instructions for new project

Stream: mathlib4

[Antoine Chambert-Loir]

I tried to follow the instructions for Using mathlib4 as a dependency and something didn't happen as indicated.
After the initial lake +leanprover… new … math command, the lake exe cache get command gave me an error message, and I had to go straight away to the next phase, starting with lake update.
Is this normal?

[Patrick Massot]

No, this isn't normal, you shouldn't see any error message. Could you tell us more about that error message?

[Antoine Chambert-Loir]

info: cloning https://github.com/leanprover-community/mathlib4.git to ./lean_packages/mathlib
error: ./lean_packages/mathlib/lakefile.lean:18:2: error: unknown attribute [def
ault_target]
error: ./lean_packages/mathlib/lakefile.lean:22:2: error: unknown attribute [default_target]
error: ./lean_packages/mathlib/lakefile.lean: package configuration has errors

[Sebastian Ullrich]

What does elan show say?

[Antoine Chambert-Loir]

(10:54) pro-acl > elan show
installed toolchains
--------------------

stable
nightly
leanprover-community/lean:3.44.1
leanprover-community/lean:3.48.0
leanprover-community/lean:3.49.0
leanprover-community/lean:3.49.1
leanprover-community/lean:3.50.2
leanprover-community/lean:3.50.3
leanprover-community/lean:3.51.1
leanprover/lean4:nightly
leanprover/lean4:nightly-2022-12-13
leanprover/lean4:nightly-2022-12-16
leanprover/lean4:nightly-2023-02-04
leanprover/lean4:nightly-2023-05-16
leanprover/lean4:nightly-2023-05-31
leanprover/lean4:nightly-2023-06-07
leanprover/lean4:nightly-2023-06-10
leanprover/lean4:nightly-2023-06-20
leanprover/lean4:nightly-2023-07-12
leanprover/lean4:stable (default)

active toolchain
----------------

leanprover/lean4:nightly-2023-07-12 (overridden by '/Users/chambert/Documents/Lean4/Jordan/lean-toolchain')
Lean (version 4.0.0-nightly-2023-07-12, commit 6e904421304c, Release)

[Antoine Chambert-Loir]

(I'd be glad to be taught how to delete obsolete toolchains…)

[Sebastian Ullrich]

Curious. Old Lakes don't understand [default_target], but apparently your Lake should not be old at all. What does lake --version say?

[Kevin Buzzard]

I never know whether having stable as default is a bad idea. Isn't stable very old now?

[Antoine Chambert-Loir]

(11:28) pro-acl > lake --version
Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2023-07-12)

[Scott Morrison]

When you are outside of that directory (e.g. in the parent directory) so lake --version say something else?

[Scott Morrison]

(I'm imagining that an old lake was used to create the project, and so made a lakefile.lean with old syntax, but then once you're inside the project this is obscured because the lean-toolchain causes a newer lake to be used.)

[Antoine Chambert-Loir]

(12:59) pro-acl > pwd
/Users/chambert/Documents
(13:00) pro-acl > lake --version
Lake version 4.0.0 (Lean version 4.0.0, commit 7dbfaf9b751917a7fe020485bf57f41fdddcaafa)
(13:00) pro-acl > cd Lean4
(13:00) pro-acl > lake --version
Lake version 4.0.0 (Lean version 4.0.0, commit 7dbfaf9b751917a7fe020485bf57f41fdddcaafa)
(13:00) pro-acl > cd Jordan
(13:00) pro-acl > lake --version
Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2023-07-12)

[Antoine Chambert-Loir]

On the other hand :

(13:00) pro-acl > cd
(13:01) pro-acl > which lake
/Users/chambert/.elan/bin/lake
(13:01) pro-acl > cd Documents/Lean4/Jordan
(13:01) pro-acl > which lake
/Users/chambert/.elan/bin/lake

[Scott Morrison]

@Antoine Chambert-Loir, replying to something above, you can clean up your toolchains by deleting some or all of .elan/toolchain.

[Scott Morrison]

That commit is from a year ago, so perhaps this is the problem. I would at this point just recommend deleting ~/.elan, reinstalling elan, and hoping that you can no longer reproduce the problem. :-)

[Sebastian Ullrich]

The core issue seems to be that the default toolchain somehow is used inside the project directory... sometimes. Updating or removing the default toolchain should not really solve the issue.

[Sebastian Ullrich]

@Antoine Chambert-Loir I'm assuming lake build fails the same way? But update didn't? And all these were run from the same directory?

[Antoine Chambert-Loir]

I deleted my .elan directory, ran brew upgrade elan (because elan self update apparently does not work when elanhas been installed by brew), and now everything works as indicated.

[Michael Stoll]

Reviving this thread to report my experience with trying to follow https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency: After

> elan self update
info: checking for self-updates
info: downloading self-update
info: elan updated successfully to 2.0.1
> lake +leanprover-community/mathlib4:lean-toolchain new seminar2023 math
info: downloading component 'lean'
178.9 MiB / 178.9 MiB (100 %)   3.0 MiB/s ETA:   0 s
info: installing component 'lean'
> cd seminar2023/
seminar2023> lake exe cache get

I got the message

error: dependency mathlib of seminar2023 not in manifest, use `lake update` to update

Then

seminar2023> lake update
cloning https://github.com/leanprover-community/mathlib4.git to lake-packages/mathlib
error: ./lake-packages/mathlib/lakefile.lean:30:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: ./lake-packages/mathlib/lakefile.lean:53:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: ./lake-packages/mathlib/lakefile.lean: package configuration has errors

So I tried the next item on the list, which finally did work:

seminar2023> 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    28  100    28    0     0    300      0 --:--:-- --:--:-- --:--:--   304
seminar2023> lake update
mathlib: URL has changed; deleting './lake-packages/mathlib' and cloning again
cloning https://github.com/leanprover-community/mathlib4.git to ./lake-packages/mathlib
cloning https://github.com/EdAyers/ProofWidgets4 to ./lake-packages/proofwidgets
cloning https://github.com/mhuisi/lean4-cli.git to ./lake-packages/Cli
cloning https://github.com/gebner/quote4 to ./lake-packages/Qq
cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop
cloning https://github.com/leanprover/std4 to ./lake-packages/std
seminar2023> lake exe cache get
info: Downloading proofwidgets/v0.0.13/linux-64.tar.gz
info: Unpacking proofwidgets/v0.0.13/linux-64.tar.gz
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache
leantar is too old; downloading more recent version
Attempting to download 3683 file(s)
Downloaded: 3683 file(s) [attempted 3683/3683 = 100%] (100% success)
Decompressing 3683 file(s)
unpacked in 10652 ms

Is this normal (this is on Linux OpenSuSE Tumbleweed)? If so, it would help to modify the instructions accordingly.

[Scott Morrison]

I see slightly different results (on macos):

% elan --version
elan 2.0.1 ( )
% lake +leanprover-community/mathlib4:lean-toolchain new seminar2023 math
% cd seminar2023
% lake exe cache get
error: no default toolchain configured. run `elan default nightly` to install & configure the latest Lean 4 nightly release.
% elan default nightly
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2023-08-28
info: downloading component 'lean'
Total: 174.4 MiB Speed:  10.7 MiB/s
info: installing component 'lean'
info: default toolchain set to 'nightly'

  nightly installed - Lean (version 4.0.0-nightly-2023-08-28, commit 7ee7595637dc, Release)

% lake exe cache get
error: dependency 'mathlib' of 'seminar2023' not in manifest, use `lake update` to update
% lake update
cloning https://github.com/leanprover-community/mathlib4.git to ./lake-packages/mathlib
cloning https://github.com/EdAyers/ProofWidgets4 to ./lake-packages/proofwidgets
cloning https://github.com/mhuisi/lean4-cli.git to ./lake-packages/Cli
cloning https://github.com/gebner/quote4 to ./lake-packages/Qq
cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop
cloning https://github.com/leanprover/std4 to ./lake-packages/std

[Scott Morrison]

I would have hoped that lake +leanprover-community/mathlib4:lean-toolchain new seminar2023 math would create a directory containing a lean-toolchain, but apparently it doesn't.

[Scott Morrison]

@Mac Malone do you have a suggestion here? Clearly something, instructions or otherwise, needs fixing here.

[Mac Malone]

@Scott Morrison I have not been able to get lake +leanprover-community/mathlib4:lean-toolchain working on my system -- even in WSL -- despite elan claiming to be on version 2.0.1, so I can't test this at the moment. However, the only reason Lake should skip creating a lean-toolchain toolchain is if the Lean.toolchain of the Lean Lake was built with was not set to anything.

[Mac Malone]

One thing to check is what does echo "#eval Lean.toolchain" | lean +leanprover-community/mathlib4:lean-toolchain --stdin give?

[Scott Morrison]

Indeed:

% echo "#eval Lean.toolchain" | lean +leanprover-community/mathlib4:lean-toolchain --stdin
""

[Scott Morrison]

% lean --version
Lean (version 4.0.0-nightly-2023-08-28, commit 7ee7595637dc, Release)

[Scott Morrison]

So a problem in how we release nightlies?

[Mac Malone]

what does lean +leanprover-community/mathlib4:lean-toolchain --version give?

[Scott Morrison]

% lean +leanprover-community/mathlib4:lean-toolchain --version
Lean (version 4.0.0, commit 216d2460e0ad, Release)

[Mac Malone]

And what does echo "#eval Lean.toolchain" | lean --stdin give.

[Scott Morrison]

% echo "#eval Lean.toolchain" | lean --stdin
"leanprover/lean4:nightly-2023-08-28"

[Mac Malone]

Ok, so your system Lean is fine. The mathlib4:lean-toolchain Lean is not properly versioned however.

[Mac Malone]

It could be because it is uses rc? and that did not get versioned correctly when built.

[Scott Morrison]

Last night I moved Mathlib's lean-toolchain to

% cat lean-toolchain
leanprover/lean4:v4.0.0-rc2

[Mac Malone]

Yeah, it seems that the rc2 release tag was not built with proper version information. How was it built?

[Scott Morrison]

The "usual" way: I just pushed a tag to leanprover/lean and waited for CI.

[Mac Malone]

Oh, yeah, that will not work. That will create a source build.

[Mac Malone]

Note the LEAN_VERSION_STRING=... in the CI for nightly builds.

[Scott Morrison]

I think it is

if [[ -n '${{ matrix.release }}' && -n '${{ needs.set-nightly.outputs.nightly }}' ]]; then
  OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.set-nightly.outputs.nightly }})
fi

where it actually happens.

[Mac Malone]

Interesting, looking back, some the old milestone releases also don't have proper version info (e.g., m4).

[Mac Malone]

If we want tags to work, the CI will need to parse the tag and set the relevant version definitions accordingly.

[Scott Morrison]

Yes. I think I want this to be driven by pushing a tag. So the CI needs some work today. :-)

[Scott Morrison]

Okay, I've written said CI in lean4#2472.

[Scott Morrison]

@Michael Stoll, thank you very much for your bug report (even if we are actually solving a different problem by now!), and sorry for hijacking your thread.

[Michael Stoll]

@Scott Morrison No problem; it wasn't my thread to begin with...