std fails to build after lake update

Stream: mathlib4

[Joachim Breitner]

Coming back to a mathlib4-using project of mine that I haven't touched in a few month, I ran lake update and cp lake-packages/mathlib/lean-toolchain ., but if I now run lake build I get build errors when building std:

./lake-packages/std/././Std/Tactic/HaveI.lean:47:16: error: application type mismatch
  TSyntax.getId x
argument
  x
has type
  TSyntax [`ident, `Lean.Parser.Term.hole] : Type
but is expected to have type
  Ident : Type
error: external command `/home/jojo/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/lean` exited with code 1

I checked: The same revision of std is mentioned in lake-manifest.json and lake-packages/mathlib/lake-manifest.json. What could this mean?
(I am using elan 1.4.5 if that matters.)

[Alex J. Best]

Did you try lake clean first?

[Joachim Breitner]

Not sure, but it doesn't help :-)

[Jannis Limperg]

Maybe a stray elan override.

[Joachim Breitner]

Good idea, but

$ elan override list
no overrides

[Alex J. Best]

Also probably worth doing elan self update not that its likely to make too much of a difference here

[Joachim Breitner]

(The project is https://github.com/nomeata/rerolling-sixes if someone wants to help by trying it; clone it and run lake update; cp lake-packages/mathlib/lean-toolchain .; lake build)

[Joachim Breitner]

I’m using elan from nix, which doesn't like elan self update, but as you say, it’s unlikely the issue.
Now upgraded to elan-2.0.0, still via nix, deleted ~/.elan, still fails. Very odd.

[Joachim Breitner]

Ah, found it. Somehow the lake update didn't work, at least after I ran it again it switched more versions, and now cache get actually hits… not sure what went wrong initially.
Sorry for the noise

[Joachim Breitner]

Scrolling back I got

~/projekte/rerolling-sixes $ lake update
updating lake-packages/mathlib to revision 8fe2ce366cdcf5d06ea7d8de708d81e7d4df8873
error: ./lake-packages/mathlib/lakefile.lean:29:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: ./lake-packages/mathlib/lakefile.lean:47:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: ./lake-packages/mathlib/lakefile.lean: package configuration has errors

and I saw the error messages, but didn’t realize that the update was partial this way.

[Notification Bot]

Joachim Breitner has marked this topic as resolved.

[Notification Bot]

Kevin Buzzard has marked this topic as unresolved.

[Kevin Buzzard]

I have a student with the same error and it was very confusing fixing it. Maybe quitting VS Code and using a terminal helps? Some combination of lake clean and lake update got us through in the end but I'm unclear about how we did it.

[Kevin Buzzard]

Update: we haven't fixed it and I have no idea how to fix it.

[Sebastian Ullrich]

In a project depending on mathlib4? Did you follow https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4?

[Kevin Buzzard]

Oh! No, I thought it was just lake update then lake exe cache get. Let's see if this gets us out of the hole!

[Kevin Buzzard]

Why is it more complicated? All experiments are slow because we're on a mac with a non-parallel curl :-/

[Ruben Van de Velde]

Because your dependent project needs to ask for the version of lean that mathlib used to create the cached oleans

[Kevin Buzzard]

but that was also true in lean 3 and I didn't have to type any random extra curl line

[Julian Berman]

All experiments are slow because we're on a mac with a non-parallel curl :-/

(if it helps, newer curl is in homebrew of course. brew install curl followed by PATH=$(brew --prefix curl)/bin:$PATH should get you whatever version it's expecting that has parallelism).

[Kevin Buzzard]

oh nice! OK so we have a new curl and so far we're on uncaught exception; leantar failed with error code 101

[Ruben Van de Velde]

Lean 3 solved that by having a mathlib-specific command in leanproject. I wonder if lake could do that by default or at least print a prompt to do it after it's updated the dependency

[Julian Berman]

I don't know much about leantar but if you run export RUST_BACKTRACE=1 and then try again do you get anything more interesting looking Kevin? That error message doesn't have much in it.

[Kevin Buzzard]

looks like it's working now; that wasn't much fun. I have no idea what we did to get into that state.

[Julian Berman]

https://en.wikipedia.org/wiki/Heisenbug

[Mario Carneiro]

Kevin Buzzard said:

oh nice! OK so we have a new curl and so far we're on uncaught exception; leantar failed with error code 101

This error code looks to be the result of a rust panic inside leantar, so hopefully it printed something else before that, unless lake exe cache is swallowing the error message

[Mario Carneiro]

My guess is that either a file was not found or something was not writable

[Mario Carneiro]

or you ran out of disk space

[Kevin Buzzard]

A combination of lake clean, lake exe cache clean!, lake update, and copying the thing which Sebastian linked to ultimately got it working.

[Kevin Buzzard]

OK so I'm back, updating another project with mathlib as a dependency, same error. This time I (believe I) am following the instructions to the letter. Right now the project works fine with the last commit in the mathlib in lake-packages being

commit f3e62849a4e599fd45fd6a0b43ee383789d52780 (HEAD)
Author: Alex Keizer <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Mon Jul 3 07:59:33 2023 +0000

I now try to update the dependencies of the project to today's mathlib following the instructions here and I get

buzzard@brutus:~/lean-projects/M1F-explained$ lake build
buzzard@brutus:~/lean-projects/M1F-explained$ lean --version
Lean (version 4.0.0-nightly-2023-06-20, commit a44dd71ad62a, Release)
buzzard@brutus:~/lean-projects/M1F-explained$ more lean-toolchain
leanprover/lean4:nightly-2023-06-20
buzzard@brutus:~/lean-projects/M1F-explained$ ## following https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4
buzzard@brutus:~/lean-projects/M1F-explained$ lake update
updating lake-packages/mathlib to revision 35ae770835c2770643ccc5a57910828ba9885e23
error: ./lake-packages/mathlib/lakefile.lean:29:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: ./lake-packages/mathlib/lakefile.lean:52:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: ./lake-packages/mathlib/lakefile.lean: package configuration has errors
buzzard@brutus:~/lean-projects/M1F-explained$ curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100    36  100    36    0     0    107      0 --:--:-- --:--:-- --:--:--   108
buzzard@brutus:~/lean-projects/M1F-explained$ lake exe cache get
info: updating ./lake-packages/mathlib to revision f3e62849a4e599fd45fd6a0b43ee383789d52780
error: ./lake-packages/proofwidgets/lakefile.lean:29:5: error: invalid binder annotation, type is not a class instance
  ?m.6585
use the command `set_option checkBinderAnnotations false` to disable the check
error: ./lake-packages/proofwidgets/lakefile.lean:48:39: error: invalid binder annotation, type is not a class instance
  ?m.6595
use the command `set_option checkBinderAnnotations false` to disable the check
error: ./lake-packages/proofwidgets/lakefile.lean:59:2: error: unknown identifier 'widgetJsAllTarget'
error: ./lake-packages/proofwidgets/lakefile.lean:62:2: error: unknown identifier 'widgetJsAllTarget'
error: ./lake-packages/proofwidgets/lakefile.lean:69:10: error: invalid field 'await', the environment does not contain 'Lake.CustomData.await'
  job₁
has type
  CustomData (Package.name pkg, `widgetJsAll)
error: ./lake-packages/proofwidgets/lakefile.lean: package configuration has errors
buzzard@brutus:~/lean-projects/M1F-explained$ git status
On branch main
Your branch is up-to-date with 'origin/main'.

Changes not staged for commit:
  (use "git add <file>..." to update what will be committed)
  (use "git restore <file>..." to discard changes in working directory)
    modified:   lean-toolchain

no changes added to commit (use "git add" and/or "git commit -a")
buzzard@brutus:~/lean-projects/M1F-explained$

The project whose mathlib I want to update is on github here.

What am I doing wrong?

[Mauricio Collares]

lake update does not update lean-toolchain. Try copying it from mathlib.

[Kevin Buzzard]

Is that not what the line curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain does?

I should make it clearer what I ran:

lake update
curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake exe cache get

[Arend Mellendijk]

Try running the curl first. That worked for me.

[Mauricio Collares]

Sorry Kevin, my bad! But I agree with Arend's suggestion. From the logs, the initial lake update in your run fetched the new mathlib commits, then failed because of the Lake version mismatch and didn't touch the lockfile. Then lake exe cache get checked out the mathlib commit in the lockfile (that is, the old f3e628 revision), which does not compile with the newer toolchain.

[Scott Morrison]

I permuted those lines on the wiki page!

[Kevin Buzzard]

Progress: The project was in a borked state -- the copy of mathlib in lake-packages was on a July commit but it's claiming to use a version of Lean from August.

I can confirm that running curl first, and then lake update, has updated the project correctly (i.e. Scott's fix seems to be good).

Reverting back to the July state of the project, it seems that the following instructions

lake update ## errors as above
curl -L ... ## works fine as above
lake exe cache get ## errors as above
lake update ## seems to work fine

bork your project. After those commands I now have a mathlib dependency on a July 3rd commit and on an August toolchain. So this is a pretty horrible gotcha.