Bug: lake update making unwanted toolchain update

Stream: lean4

[Shreyas Srinivas]

The following happened:

1. I setup a v4.13.0 project . I made elan pin the toolchain to v4.13.0 as default. This is the latest toolchain on Duper.
2. I added the Duper dependency.
3. lake complained that there was no manifest entry for Duper and asked me to run lake update Duper.
4. Now I find that lake has updated my toolchain to 4.15.0-rc1. Naturally it can't build duper.

[Shreyas Srinivas]

CC : @Mac Malone

[Shreyas Srinivas]

more:

5. I tried changing the toolchain file back to v4.13.0. Now suddenly proofwidgets has an issue

[Shreyas Srinivas]

Essentially it seems impossible to get a working project with duper and auto

[Shreyas Srinivas]

Additional point: I would love to not have to deal with ProofWidget issues on math projects, since I don't use it at all. Adjusting v4.14.0 and higher projects to v4.13.0 (to use Duper and lean-auto) seems impossible because of ProofWidgets. This happened when I started the project without forcing elan to default to v4.13.0

[Chris Bailey]

Pinning the version to 4.13.0, putting this in the lakefile.toml, and running lake build worked for me:

[[require]]
name = "Duper"
git = "https://github.com/leanprover-community/duper"
rev = "b9a630ad3bf65b01cba95fa19ce1bdb5d71a6c99"

[Shreyas Srinivas]

How did you get duper added to the lake-manifest file?

[Shreyas Srinivas]

Also, the duper project instructions specifically suggest using "v0.0.20"

[Shreyas Srinivas]

Running cache on a fresh project with your config, I get

error: ././.lake/packages/proofwidgets/lakefile.lean:20:20: error: invalid argument name 'text' for function 'Lake.buildFileAfterDep'
error: ././.lake/packages/proofwidgets/lakefile.lean: package configuration has errors

[Shreyas Srinivas]

the lean-toolchain file is says leanprover/lean4:v4.13.0

[Chris Bailey]

I guess just change it to rev = "v0.0.20" then. I don't know what cache is for in this case; the lake-manifest was generated for me the first time I ran lake build. I have found that I sometimes need to remove and remake the manifest, I would try removing lake-manifest and .lake and just rebuilding.

[Shreyas Srinivas]

The cache is for mathlib

[Shreyas Srinivas]

running lake build produces stranger errors:

lake build
info: EFXExperiments: no previous manifest, creating one from scratch
trace: ././.lake/packages/Duper> git fetch --tags --force origin
trace: ././.lake/packages/mathlib> git fetch --tags --force origin
trace: stderr:
From https://github.com/leanprover-community/mathlib4
   eba2d3f58a..a54394de02  arend/card_pair_lcm  -> origin/arend/card_pair_lcm
 + ea6e38a0c2...3561e76bb0 emultiplicity-of-nat -> origin/emultiplicity-of-nat  (forced update)
 * [new branch]            j-loreaux/ring-error-msg -> origin/j-loreaux/ring-error-msg
   6581d46be3..1957fef0f0  master               -> origin/master
   e4b9c103a7..2da14b7cdf  nightly-testing      -> origin/nightly-testing
   6581d46be3..1957fef0f0  staging              -> origin/staging
info: leanprover-community/mathlib: updating repository '././.lake/packages/mathlib' to revision '1957fef0f098a197410617514519012cccddd207'
trace: ././.lake/packages/mathlib> git checkout --detach 1957fef0f098a197410617514519012cccddd207 --
trace: stderr:
Previous HEAD position was 6581d46be3 chore: eliminate `multiplicity` namespace (#19623)
HEAD is now at 1957fef0f0 feat(CategoryTheory): expand the API for AB axioms (#19200)
error: ././.lake/packages/proofwidgets/lakefile.lean:20:20: error: invalid argument name 'text' for function 'Lake.buildFileAfterDep'
error: ././.lake/packages/proofwidgets/lakefile.lean: package configuration has errors

[Shreyas Srinivas]

This is funny because the project is fresh and none of the dependencies have even been imported

[Chris Bailey]

Oh right, I guess your project can be mathlib + duper in which case you'd still want to use the cache. I'm not sure of the extent to which you would need to manually ensure compatible versions for everything at this point.

[Shreyas Srinivas]

but lake should be fetching the cache for v4.13.0

[Chris Bailey]

I don't think it does that automatically, or at least it's not in this case. 1957fef0f098a197410617514519012cccddd207 is the current head. Does your lakefile pin the version?

[Shreyas Srinivas]

I'll try pinning mathlib

[Shreyas Srinivas]

Although I have never needed to do this on any other math project which I don't update

[Shreyas Srinivas]

That proved even worse. Here's my lakefile.toml:

name = "EFXExperiments"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["EFXExperiments"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`

[[require]]
name = "Duper"
git = "https://github.com/leanprover-community/duper"
rev = "b9a630ad3bf65b01cba95fa19ce1bdb5d71a6c99"

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.13.0"

[[lean_lib]]
name = "EFXExperiments"

[Shreyas Srinivas]

Here's the lean-toolchain file : leanprover/lean4:v4.13.0

[Shreyas Srinivas]

The error message is super long with a number of errors about Std. which indicates toolchain incompatibility

[Shreyas Srinivas]

Here's stderr dumped in a textfile if it helps:
errorfile.txt

[Chris Bailey]

Here's my lakefile, I was able to open and use the Auto example from the readme. I would make sure adjust the toml file, then manually remove the lake-manifest AND the .lake directory, then run lake exe cache get. Also I just picked a dumb faceroll name for the test project, probably shouldn't have picked something so close to duper.

name = "dup"
version = "0.1.0"
defaultTargets = ["dup"]

[[require]]
name = "Duper"
git = "https://github.com/leanprover-community/duper"
rev = "v0.0.20"

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4"
rev = "v4.13.0"

[[lean_lib]]
name = "Dup"

[[lean_exe]]
name = "dup"
root = "Main"

[Shreyas Srinivas]

I did that and this time it worked. Thanks :)

However cache downloaded the files twice:

lake exe cache get!
Attempting to download 5370 file(s)
Downloaded: 5370 file(s) [attempted 5370/5370 = 100%] (100% success)
Decompressing 5370 file(s)
Unpacked in 4315 ms
Completed successfully!
info: EFXExperiments: no previous manifest, creating one from scratch
info: Duper: cloning https://github.com/leanprover-community/duper to '././.lake/packages/Duper'
info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4 to '././.lake/packages/mathlib'
info: auto: cloning https://github.com/leanprover-community/lean-auto.git to '././.lake/packages/auto'
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
info: importGraph: cloning https://github.com/leanprover-community/import-graph to '././.lake/packages/importGraph'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient to '././.lake/packages/LeanSearchClient'
info: plausible: cloning https://github.com/leanprover-community/plausible to '././.lake/packages/plausible'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
info: mathlib: running post-update hooks
Attempting to download 5370 file(s)
Downloaded: 5370 file(s) [attempted 5370/5370 = 100%] (100% success)
Decompressing 5370 file(s)
Unpacked in 5083 ms
Completed successfully!