Mathlib doesn't build

Stream: mathlib4

[Stepan Nesterov]

If I try to simply clone and run mathlib in VSCode right now, I get the following error:
PastedText.txt
How do I deal with this?

[James E Hanson]

Did you try running lake exe cache get like the middle of the log suggested?

[Stepan Nesterov]

Ok I have tried to run lake exe cache get on my fork on Mathlib, which is identical to current Mathlib, and after just a few hours of build I get this:
PastedText.txt

[Stepan Nesterov]

Basically it seems like this random chunk of Mathlib suddenly contains a wrong proof:

/-- The group morphism from `fixingSubgroup` of a union to the iterated `fixingSubgroup`. -/
@[to_additive
/-- The additive group morphism from `fixingAddSubgroup` of a union
to the iterated `fixingAddSubgroup`. -/]
def fixingSubgroup_union_to_fixingSubgroup_of_fixingSubgroup :
    fixingSubgroup M (s ∪ t) →*
      fixingSubgroup (fixingSubgroup M s) (Subtype.val ⁻¹' t : Set (ofFixingSubgroup M s)) where
  toFun m := ⟨⟨m, (mem_fixingSubgroup_union_iff.mp m.prop).1⟩, by
      rintro ⟨⟨x, hx⟩, hx'⟩
      simp only [Set.mem_preimage] at hx'
      simp only [← SetLike.coe_eq_coe, SubMulAction.val_smul_of_tower]
      exact (mem_fixingSubgroup_union_iff.mp m.prop).2 ⟨x, hx'⟩⟩
  map_one' := by simp
  map_mul' _ _ := by simp

The last simp does not finish the job

[Stepan Nesterov]

Which I can fix with simp; rfl and proceed to do what I wanted to do but obviously I feel very suspicious of the fact that I need to actually fix a part of mathlib before it compiles, and it's more likely that I did something wrong

[Ruben Van de Velde]

You should never have a few hours of build for mathlib

[Ruben Van de Velde]

The cache command should download the compiled version of mathlib

[Stepan Nesterov]

Ruben Van de Velde said:

The cache command should download the compiled version of mathlib

Is it lake exe cache get or a separate command?

[Ruben Van de Velde]

That one, yeah

[Stepan Nesterov]

Well I did run lake exe cache get

[Stepan Nesterov]

Another interesting fact is that it only works if you don't try to lake update, otherwise
stepannesterov@DN0a1e875b Stepan-s-mathlib4-fork % lake update
info: leanprover-community/plausible: checking out revision '7311586e1a56af887b1081d05e80c11b6c41d212'
info: leanprover-community/importGraph: checking out revision '875ad9d88ed684e39c16bdea260e6ecfa15afd60'
info: leanprover-community/aesop: checking out revision 'f08e838d4f9aea519f3cde06260cfb686fd4bab0'
info: leanprover-community/Qq: checking out revision '23324752757bf28124a518ec284044c8db79fee5'
info: leanprover-community/batteries: checking out revision 'a7ab123915d17f92587c2b1ec7218db7db7856e1'
info: updating toolchain to 'leanprover/lean4:v4.28.0-rc1'
info: restarting Lake via Elan
info: toolchain not updated; already up-to-date
info: Cli: checking out revision '28e0856d4424863a85b18f38868c5420c55f9bae'
info: mathlib: running post-update hooks
(base) stepannesterov@DN0a1e875b Stepan-s-mathlib4-fork % lake exe cache get
✖ [13/21] Building Batteries.Data.Array.Match
trace: .> LEAN_PATH=/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Cli/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Qq/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/aesop/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/importGraph/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/plausible/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/build/lib/lean /Users/stepannesterov/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lean /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/Batteries/Data/Array/Match.lean -o /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.olean -i /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.ilean -c /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.c --setup /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.setup.json --json
error: Batteries/Data/Array/Match.lean:138:2: Rel is not a field of structure FinitenessRelation
error: Batteries/Data/Array/Match.lean:137:44: Fields missing: rel

Field rel must be explicitly provided; its synthesized value is
InvImage IterM.IsPlausibleSuccessorOf ?m.18
error: Batteries/Data/Array/Match.lean:146:6: failed to synthesize
Iterator ?m.19 ?m.20 ?m.21

Hint: Additional diagnostic information may be available using the set_option diagnostics true command.
error: Batteries/Data/Array/Match.lean:154:10: failed to synthesize
Iterator ?m.19 ?m.20 ?m.21

Hint: Additional diagnostic information may be available using the set_option diagnostics true command.
error: Batteries/Data/Array/Match.lean:162:10: failed to synthesize
Iterator ?m.19 ?m.20 ?m.21

Hint: Additional diagnostic information may be available using the set_option diagnostics true command.
error: Lean exited with code 1
Some required targets logged failures:

• Batteries.Data.Array.Match
  error: build failed

[Ruben Van de Velde]

That makes sense, you should not run lake update within mathlib

[Stepan Nesterov]

So potentially maybe my mathlib doesn't work because I can't lake update, but I really cant lake update, because then everything is on fire

[Ruben Van de Velde]

After you revert all local chances and run lake exe cache get, what's the output?

[Stepan Nesterov]

I don't know how to revert lake exe cache get, but when I executed it for the first time, it was
stepannesterov@DN0a1e875b Stepan-s-mathlib4-fork % git switch semisimple-branch
branch 'semisimple-branch' set up to track 'origin/semisimple-branch'.
Switched to a new branch 'semisimple-branch'
(base) stepannesterov@DN0a1e875b Stepan-s-mathlib4-fork % lake exe cache get
info: proofwidgets: checking out revision 'c04225ee7c0585effbd933662b3151f01b600e40'
info: aesop: checking out revision 'cb837cc26236ada03c81837bebe0acd9c70ced7d'
info: Qq: checking out revision 'bd58c9efe2086d56ca361807014141a860ddbf8c'
info: batteries: checking out revision '4ca6ac27b5b03d9554013a85343f75f43501175a'
info: Cli: checking out revision '55c37290ff6186e2e965d68cf853a57c0702db82'
Fetching ProofWidgets cloud release... done!
Current branch: semisimple-branch
Using cache (Azure) from origin: stepan2698-cpu/Stepan-s-mathlib4-fork
No files to download
No files to download
Decompressing 7874 file(s)
Unpacked in 11594 ms
Completed successfully!

[Stepan Nesterov]

But of course mathlib.lean still was complaining that imports are out of date, so I pressed 'Restart File' and waited for a couple hours

[Stepan Nesterov]

Stepan Nesterov said:

Ok I have tried to run lake exe cache get on my fork on Mathlib, which is identical to current Mathlib, and after just a few hours of build I get this:
PastedText.txt

And then this happened

[Damiano Testa]

Sometimes, I need to restart the server in VSCode, to make it aware that the cache is available.

[Kevin Buzzard]

Just to emphasize a couple of things: (1) an end user should never have to type lake update in mathlib (2) waiting more than a few minutes for anything almost certainly means something has gone wrong (in particular essentially the only reason you should be watching a machine slowly counting to 7000 is if you've changed a file which is imported early and have decided to compile the resulting mathlib on your own computer rather than getting one of github's computers to do this for you).

[Junyan Xu]

What does lake setup-file do? lake help says nothing about it. Did you run it yourself? I checked that lake update doesn't call it.

[Aaron Liu]

I think it's called by VSCode when it sets up the file

[Junyan Xu]

I don't recall ever seeing lake setup-file being called; do they appear in the infoview?

[Stepan Nesterov]

What if I cannot get cache because of the following:
(base) stepannesterov@DNa221b1b Stepan-s-mathlib4-fork % lake exe cache get
✖ [9/22] Building Batteries.Data.Array.Match
trace: .> LEAN_PATH=/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Cli/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Qq/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/aesop/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/importGraph/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/plausible/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/build/lib/lean /Users/stepannesterov/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lean /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/Batteries/Data/Array/Match.lean -o /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.olean -i /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.ilean -c /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.c --setup /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.setup.json --json
error: Batteries/Data/Array/Match.lean:138:2: Rel is not a field of structure FinitenessRelation
error: Batteries/Data/Array/Match.lean:137:44: Fields missing: rel

Field rel must be explicitly provided; its synthesized value is
InvImage IterM.IsPlausibleSuccessorOf ?m.18
error: Batteries/Data/Array/Match.lean:146:6: failed to synthesize
Iterator ?m.19 ?m.20 ?m.21

Hint: Additional diagnostic information may be available using the set_option diagnostics true command.
error: Batteries/Data/Array/Match.lean:154:10: failed to synthesize
Iterator ?m.19 ?m.20 ?m.21

Hint: Additional diagnostic information may be available using the set_option diagnostics true command.
error: Batteries/Data/Array/Match.lean:162:10: failed to synthesize
Iterator ?m.19 ?m.20 ?m.21

Hint: Additional diagnostic information may be available using the set_option diagnostics true command.
error: Lean exited with code 1
Some required targets logged failures:

• Batteries.Data.Array.Match
  error: build failed

[Kevin Buzzard]

Did you try switching it off and on again with rm -rf .lake (aka delete the directory .lake) then lake exe cache get again?

[Stepan Nesterov]

I tried creating a new branch for a new PR, running rm -rf .lake, lake exe cache get, but this still happens:
PastedText.txt

[Sébastien Gouëzel]

Could you start a new clone of Mathlib and see what happens? Copy-pasting all the commands you type and their outputs would hopefully help.

[Stepan Nesterov]

Well I guess this happens when I restart the file. When I lake exe cache get, I get
PastedText.txt

[Sébastien Gouëzel]

I mean, from a fresh directory, start with

git clone https://github.com/leanprover-community/mathlib4.git
cd Mathlib
lake exe cache get
lake build

[Stepan Nesterov]

Well it works on mathlib itself, but not on my fork whose master branch is supposed to be identical to mathlib
Full log:
PastedText.txt

[Stepan Nesterov]

That said, I've already made one PR by working inside mathlib in VSCode, and then just copypasting my code into the broken fork and commiting it. Github couldn't tell the difference c;

[Ruben Van de Velde]

Okay, that's because you're running lake inside your Lean folder rather than Lean/Stepan-s-mathlib4-fork

[Stepan Nesterov]

Oh yeah I did that by mistake at first. But the same thing happens when I run it from VSCode

[Stepan Nesterov]

Or in the right directory which I did afterwards

[Ruben Van de Velde]

It looks like you're building with lean 4.27 but your repository is on 4.28

[Ruben Van de Velde]

Did you ever set up a version override in lake?

[Stepan Nesterov]

I might have written some bespoke commands which chatGPT told me to do...

[Stepan Nesterov]

When I tried to fix it by myself I mean

[Ruben Van de Velde]

That's always risky

[Ruben Van de Velde]

I don't recall the command to check, but look at lake --help for something related to version overrides

[Sébastien Gouëzel]

You could start from a fresh directory but cloning your fork instead of the main mathlib. Hopefully the override shouldn't be set up there.

[Stepan Nesterov]

That's exactly what I did

[Stepan Nesterov]

Could the version override somehow have propagated into github?

[Ruben Van de Velde]

What does elan override list say?

[Stepan Nesterov]

(base) stepannesterov@DN0a221534 Stepan-s-mathlib4-fork % elan override list
/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork leanprover/lean4:v4.27.0-rc1

[Ruben Van de Velde]

That's your issue

[Ruben Van de Velde]

Run elan override unset /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork

[Stepan Nesterov]

(base) stepannesterov@DN0a221534 Stepan-s-mathlib4-fork % elan override unset /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork
error: Found argument '/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork' which wasn't expected, or isn't valid in this context

USAGE:
elan override unset [FLAGS] [OPTIONS]

[Riccardo Brasca]

I saw the same today on two student's computer. mathlib was just cloned (and Lean just installed). I thinking something strange was going on, but maybe there is actually a problem somewhere.

[Riccardo Brasca]

@Filippo A. E. Nuccio it was the same error, right?

[Ruben Van de Velde]

Sorry, elan override unset --path /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork

[Stepan Nesterov]

It works!! :tada:

[Stepan Nesterov]

Thank you so much for the quick reaction

[Ruben Van de Velde]

I still believe elan should print a warning on every command when an override is in place

[Kim Morrison]

Issue posted as https://github.com/leanprover/elan/issues/189

[Kim Morrison :bot:]

PR: elan#190