failure in test/ValuedCSP.lean

Stream: nightly-testing

[Kim Morrison]

@Martin Dvořák, are you available to fix the failure in test/ValuedCSP.lean in on branch#nightly-testing?

For now I am just commenting the failing test out. You can just push directly to that branch if you're able to help.

[Martin Dvořák]

I will have a look; thanks for letting me know.

[Martin Dvořák]

I cannot build the file locally at all:

stderr:
✖ [290/907] Building Batteries.Data.List.Lemmas
trace: .> LEAN_PATH=.\.\.lake/packages\batteries\.lake\build\lib;.\.\.lake/packages\Qq\.lake\build\lib;.\.\.lake/packages\aesop\.lake\build\lib;.\.\.lake/packages\proofwidgets\.lake\build\lib;.\.\.lake/packages\Cli\.lake\build\lib;.\.\.lake/packages\importGraph\.lake\build\lib;.\.\.lake\build\lib PATH c:\Users\mdvorak\.elan\toolchains\leanprover--lean4---nightly-2024-09-05\bin\lean.exe -Dlinter.missingDocs=true .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean -R .\.\.lake/packages\batteries\.\. -o .\.\.lake/packages\batteries\.lake\build\lib\Batteries\Data\List\Lemmas.olean -i .\.\.lake/packages\batteries\.lake\build\lib\Batteries\Data\List\Lemmas.ilean -c .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\List\Lemmas.c --json
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:163:31: unknown identifier 'getElem?_set_eq''
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:164:2: The rfl tactic failed. Possible reasons:
- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
- The arguments of the relation are not equal.
Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
`exact HEq.rfl` etc.
α : Type u_1
a : α
n : Nat
l : List α
⊢ (l.set n a)[n]? = Option.map (fun x => a) l[n]?
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:161:13: unknown constant 'getElem?_set_eq''
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:167:39: unknown identifier 'getElem?_set_eq''
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:167:39: tactic 'rewrite' failed, equality or iff proof expected
  ?m.17713
α : Type u_1
a : α
n : Nat
l : List α
h : n < l.length
⊢ (l.set n a)[n]? = some a
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:172:24: unknown identifier 'getElem?_set_eq''
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:172:24: tactic 'rewrite' failed, equality or iff proof expected
  ?m.17774
α : Type u_1
a : α
n : Nat
l : List α
h : n < l.length
⊢ (l.set n a)[n]? = some a
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:180:82: unsolved goals
α : Type u_1
a : α
m n : Nat
l : List α
⊢ (if m = n then Option.map (Function.const α a) l[n]? else l[n]?) =
    if m = n then Option.map (fun x => a) l[n]? else l[n]?
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:330:66: ambiguous, possible interpretations
  _root_.or_assoc : (?m.35214 ∨ ?m.35215) ∨ ?m.35216 ↔ ?m.35214 ∨ ?m.35215 ∨ ?m.35216

  Nat.or_assoc : ∀ (x y z : Nat), x ||| y ||| z = x ||| (y ||| z)
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:330:66: ambiguous, possible interpretations
  _root_.or_assoc : (?m.35298 ∨ ?m.35299) ∨ ?m.35300 ↔ ?m.35298 ∨ ?m.35299 ∨ ?m.35300

  Nat.or_assoc : ∀ (x y z : Nat), x ||| y ||| z = x ||| (y ||| z)
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:330:37: unsolved goals
case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : x ∈ tail✝ ∪ l₂ ↔ x ∈ tail✝ ∨ x ∈ l₂
⊢ x = head✝ ∨ x ∈ tail✝ ∨ x ∈ l₂ ↔ (x = head✝ ∨ x ∈ tail✝) ∨ x ∈ l₂
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:442:31: ambiguous, possible interpretations
  _root_.and_self : ∀ (p : Prop), (p ∧ p) = p

  Nat.and_self : ∀ (x : Nat), x &&& x = x
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:442:31: ambiguous, possible interpretations
  _root_.and_self : ∀ (p : Prop), (p ∧ p) = p

  Nat.and_self : ∀ (x : Nat), x &&& x = x
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:442:31: ambiguous, possible interpretations
  _root_.and_self : ∀ (p : Prop), (p ∧ p) = p

  Nat.and_self : ∀ (x : Nat), x &&& x = x
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Lemmas.lean:442:31: ambiguous, possible interpretations
  _root_.and_self : ∀ (p : Prop), (p ∧ p) = p

  Nat.and_self : ∀ (x : Nat), x &&& x = x
error: Lean exited with code 1
✖ [393/907] Building Mathlib.Logic.Basic
trace: .> LEAN_PATH=.\.\.lake/packages\batteries\.lake\build\lib;.\.\.lake/packages\Qq\.lake\build\lib;.\.\.lake/packages\aesop\.lake\build\lib;.\.\.lake/packages\proofwidgets\.lake\build\lib;.\.\.lake/packages\Cli\.lake\build\lib;.\.\.lake/packages\importGraph\.lake\build\lib;.\.\.lake\build\lib PATH c:\Users\mdvorak\.elan\toolchains\leanprover--lean4---nightly-2024-09-05\bin\lean.exe -Dpp.unicode.fun=true -DautoImplicit=false -Dweak.linter.hashCommand=true -Dweak.linter.oldObtain=true -Dweak.linter.refine=true -Dweak.linter.style.cdot=true -Dweak.linter.style.dollarSyntax=true -Dweak.linter.style.lambdaSyntax=true -Dweak.linter.style.longLine=true -Dweak.linter.style.longFile=1500 -Dweak.linter.style.missingEnd=true -Dweak.linter.style.setOption=true .\.\.\.\Mathlib\Logic\Basic.lean -R .\.\.\. -o .\.\.lake\build\lib\Mathlib\Logic\Basic.olean -i .\.\.lake\build\lib\Mathlib\Logic\Basic.ilean -c .\.\.lake\build\ir\Mathlib\Logic\Basic.c --json
error: .\.\.\.\Mathlib\Logic\Basic.lean:901:3: function expected at
  dite_eq_left_iff
term has type
  (if h : ?m.27904 then ?m.27906 else ?m.27907 h) = ?m.27906 ↔ ∀ (h : ¬?m.27904), ?m.27907 h = ?m.27906
error: .\.\.\.\Mathlib\Logic\Basic.lean:904:3: function expected at
  dite_eq_right_iff
term has type
  (if h : ?m.28257 then ?m.28259 h else ?m.28260) = ?m.28260 ↔ ∀ (h : ?m.28257), ?m.28259 h = ?m.28260
error: .\.\.\.\Mathlib\Logic\Basic.lean:998:8: function expected at
  beq_iff_eq
term has type
  (?m.32294 == ?m.32295) = true ↔ ?m.32294 = ?m.32295
error: .\.\.\.\Mathlib\Logic\Basic.lean:998:6: tactic 'rewrite' failed, equality or iff proof expected
  ?m.32329
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = decide (a = b)
error: Lean exited with code 1
Some required builds logged failures:
- Batteries.Data.List.Lemmas
- Mathlib.Logic.Basic
error: build failed

What can I do so that I can debug it on my machine?

[Kim Morrison]

Sorry, I should have pointed you to a particular commit that would keep working.

[Kim Morrison]

@Martin Dvořák, could you checkout b5a83ea0c40bb96f710a523dbf14796352c8ce31, where lake exe cache get succeeds, see if you can work out a fix there, but then commit the fix to the head of nightly-testing?