❌ Build Failed: puzzles
Error Summary
Project build failed
📋 View command log (YAML)
Full Build Log
✖ [4/10] Building Puzzles.Basic (566ms)
trace: .> LEAN_PATH=/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/puzzles/.lake/build/lib/lean /home/nfr/.elan/toolchains/leanprover--lean4---v4.28.0/bin/lean /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/puzzles/Puzzles/Basic.lean -o /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/puzzles/.lake/build/lib/lean/Puzzles/Basic.olean -i /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/puzzles/.lake/build/lib/lean/Puzzles/Basic.ilean -c /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/puzzles/.lake/build/ir/Puzzles/Basic.c --setup /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/puzzles/.lake/build/ir/Puzzles/Basic.setup.json --json
error: Puzzles/Basic.lean:41:20: Unknown identifier `pel55_1`
error: Puzzles/Basic.lean:41:20: Unknown identifier `pel55_1`
error: Puzzles/Basic.lean:41:7: Invalid `⟨...⟩` notation: The expected type of this term could not be determined
error: Puzzles/Basic.lean:42:2: No goals to be solved
error: Puzzles/Basic.lean:181:18: Unknown identifier `haa`
error: Puzzles/Basic.lean:175:41: unsolved goals
agatha Agatha Dreadbury : u
h₂ : ∀ (x : u), (person x ∧ ∃ e1, _live_v_1 e1 x ∧ ∃ e2, _in_p_dir e2 e1 Dreadbury) ↔ lives x
h₃ : ∀ (x y : u), (∃ e1, _kill_v_1 e1 x y) ↔ killed x y
a : u
h2 : lives a ∧ killed a Agatha
⊢ ∃ x, lives x ∧ killed x agatha
warning: Puzzles/Basic.lean:177:8: This simp argument is unused:
aux0
Hint: Omit it from the simp argument list.
simp [̵a̵u̵x̵0̵]̵ ̵at h1
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Puzzles/Basic.lean:189:8: declaration uses `sorry`
warning: Puzzles/Basic.lean:198:8: This simp argument is unused:
aux0
Hint: Omit it from the simp argument list.
simp [̵a̵u̵x̵0̵,̵a̵u̵x̵1̵,̵a̵u̵x̵2̵]̵[̲a̲u̲x̲1̲,̲ ̲a̲u̲x̲2̲]̲ at h1
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Puzzles/Basic.lean:198:13: This simp argument is unused:
aux1
Hint: Omit it from the simp argument list.
simp [̵a̵u̵x̵0̵,̵a̵u̵x̵1̵,̵a̵u̵x̵2̵]̵[̲a̲u̲x̲0̲,̲ ̲a̲u̲x̲2̲]̲ at h1
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Puzzles/Basic.lean:198:18: This simp argument is unused:
aux2
Hint: Omit it from the simp argument list.
simp [̵a̵u̵x̵0̵,̵a̵u̵x̵1̵,̵a̵u̵x̵2̵]̵[̲a̲u̲x̲0̲,̲ ̲a̲u̲x̲1̲]̲ at h1
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Puzzles/Basic.lean:205:0: (∃ e2 e22 e9 x10,
(∃ x16, pron x16 ∧ ∃ e15, poss e15 x10 x16 ∧ _victim_n_of x10) ∧
∃ x34,
pron x34 ∧
∃ x3,
_killer_n_1 x3 ∧
∃ e22_1,
_always_a_1 e9 ∧
_hate_v_1 e9 x3 x10 ∧
_and_c e2 e9 e22_1 ∧
_never_a_1 e22_1
(∃ x28,
(∃ e9_1 e9_2 e2 e33, poss e33 x28 x34 ∧ _victim_n_of x28) ∧
∃ e25 e27, _rich_a_in e25 x3 ∧ more_comp e27 e25 x28)) →
(∀ (x y : u), killed x y → hates x y) ∧ ∀ (x y : u), killed x y → ¬richer x y : Prop
warning: Puzzles/Basic.lean:205:13: unused variable `e22`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Puzzles/Basic.lean:214:29: unused variable `e9`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Puzzles/Basic.lean:214:32: unused variable `e9`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Puzzles/Basic.lean:214:35: unused variable `e2`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Puzzles/Basic.lean:218:8: declaration uses `sorry`
warning: Puzzles/Basic.lean:232:8: This simp argument is unused:
aux0
Hint: Omit it from the simp argument list.
simp [̵a̵u̵x̵0̵,̵a̵u̵x̵1̵,̵h̵₁̵]̵[̲a̲u̲x̲1̲,̲ ̲h̲₁̲]̲ at h1
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Puzzles/Basic.lean:232:13: This simp argument is unused:
aux1
Hint: Omit it from the simp argument list.
simp [̵a̵u̵x̵0̵,̵a̵u̵x̵1̵,̵h̵₁̵]̵[̲a̲u̲x̲0̲,̲ ̲h̲₁̲]̲ at h1
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Puzzles/Basic.lean:232:18: This simp argument is unused:
h₁
Hint: Omit it from the simp argument list.
simp [aux0, ̲aux1,̵h̵₁̵] at h1
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
error: Puzzles/Basic.lean:257:16: Unknown identifier `haa`
error: Puzzles/Basic.lean:244:49: unsolved goals
case a.right
agatha Agatha charles Charles : u
hh₂ : ∀ (x y : u), (∃ e1, _hate_v_1 e1 x y) ↔ hates x y
hh₃ : ∀ (x y : u), hates x y → person x ∧ person y
a : u
Haa : hates agatha a
Hca : hates charles a
a1 : u
h₂ : Agatha = a1 ∧ ∃ x3, Charles = x3 ∧ ∀ (x9 : u), (∃ e20, person x9 ∧ _hate_v_1 e20 a1 x9) → ¬∃ e2, _hate_v_1 e2 x3 x9
c : u
h₄ : Charles = c ∧ ∀ (x9 : u), (∃ e20, person x9 ∧ _hate_v_1 e20 a1 x9) → ¬∃ e2, _hate_v_1 e2 c x9
⊢ hates Agatha a
case a
agatha Agatha charles Charles : u
hh₂ : ∀ (x y : u), (∃ e1, _hate_v_1 e1 x y) ↔ hates x y
hh₃ : ∀ (x y : u), hates x y → person x ∧ person y
a : u
Haa : hates agatha a
Hca : hates charles a
a1 : u
h₂ : Agatha = a1 ∧ ∃ x3, Charles = x3 ∧ ∀ (x9 : u), (∃ e20, person x9 ∧ _hate_v_1 e20 a1 x9) → ¬∃ e2, _hate_v_1 e2 x3 x9
c : u
h₄ : Charles = c ∧ ∀ (x9 : u), (∃ e20, person x9 ∧ _hate_v_1 e20 a1 x9) → ¬∃ e2, _hate_v_1 e2 c x9
⊢ ∃ e2, _hate_v_1 e2 c a
warning: Puzzles/Basic.lean:266:8: declaration uses `sorry`
error: Puzzles/Basic.lean:318:23: Unknown identifier `haa`
error: Puzzles/Basic.lean:315:46: unsolved goals
agatha Agatha butler : u
h₁ : ∀ (x y : u), (∃ e1, _hate_v_1 e1 x y) ↔ hates x y
h₂ : ∀ (x y : u), hates x y → person x ∧ person y
h₃ : ∀ (x : u), _butler_n_1 x ↔ x = butler
a : u
h2 : hates agatha a
h3 : person a → hates Agatha a → ∃ x3, _butler_n_1 x3 ∧ hates x3 a
⊢ hates butler a
error: Puzzles/Basic.lean:358:8: Unknown identifier `haa`
error: Puzzles/Basic.lean:349:23: unsolved goals
case right
agatha Agatha butler : u
h₁ : ∀ (x : u), _butler_n_1 x ↔ x = butler
h₂ : ∀ (x y : u), (∃ e1, _be_v_id e1 x y) ↔ x = y
h1 : ¬∃ x10, _butler_n_1 x10 ∧ ∃ x3, Agatha = x3 ∧ ∃ e2, _be_v_id e2 x3 x10
h2 : agatha = butler
h3 : _butler_n_1 butler
⊢ Agatha = butler
warning: Puzzles/Basic.lean:352:8: This simp argument is unused:
aux0
Hint: Omit it from the simp argument list.
simp ̵[̵a̵u̵x̵0̵]̵
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
error: Lean exited with code 1
Some required targets logged failures:
- Puzzles.Basic
warning: failed to query latest release, using existing version 'leanprover/lean4:v4.28.0'
error: build failed
← Back to Summary