Updating to 4.15.0

Stream: general

[Yaël Dillies]

I am trying to update CamCombi to 4.15.0 and I get a lot of error lines of the form

warning: ././.lake/packages/MD4Lean/lakefile.lean:13:61: warning: `Lake.BuildJob` has been deprecated: use `Lake.Job` instead

warning: ././.lake/packages/MD4Lean/lakefile.lean:26:45: warning: `Lake.BuildJob` has been deprecated: use `Lake.Job` instead

info: plausible: checking out revision '2c57364ef83406ea86d0f78ce3e342079a2fece5'
info: importGraph: checking out revision '9a0b533c2fbd6195df067630be18e11e4349051c'
warning: ././.lake/packages/proofwidgets/lakefile.lean:28:63: warning: `Lake.BuildJob` has been deprecated: use `Lake.Job` instead

warning: ././.lake/packages/proofwidgets/lakefile.lean:40:13: warning: `Lake.BuildJob.collectArray` has been deprecated: use `Lake.Job.collectArray` instead

warning: ././.lake/packages/proofwidgets/lakefile.lean:46:29: warning: `Lake.BuildJob.bindSync` has been deprecated: use `Lake.Job.mapM` instead

info: aesop: checking out revision '2689851f387bb2cef351e6825fe94a56a304ca13'
info: Qq: checking out revision 'f0c584bcb14c5adfb53079781eeea75b26ebbd32'
info: batteries: checking out revision 'e8dc5fc16c625fc4fe08f42d625523275ddbbb4b'
info: mathlib: running post-update hooks
error: ././.lake/packages/doc-gen4/lakefile.lean:134:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:135:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:138:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:139:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:142:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:144:2: error: invalid field 'mapM', the environment does not contain 'Lake.BuildJob.mapM'
  exeJob
has type
  BuildJob FilePath

error: ././.lake/packages/doc-gen4/lakefile.lean:144:2: error: invalid field 'mapM', the environment does not contain 'Lake.Job.mapM'
  exeJob
has type
  Job (FilePath × BuildTrace)

[Yaël Dillies]

cc @Kim Morrison since I see you literally just bumped mathlib to 4.15.0

[Kevin Buzzard]

I tried bumping mathlib on FLT and got similar errors. Here is the full output:

buzzard@brutus:~/lean-projects/FLT$ ./scripts/update_mathlib.sh
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100    25  100    25    0     0    106      0 --:--:-- --:--:-- --:--:--   106
info: downloading component 'lean'
252.6 MiB / 252.6 MiB (100 %)   1.9 MiB/s ETA:   0 s
info: installing component 'lean'
info: doc-gen4: checking out revision '9d993b252964a394dc4beb84f2a2a210de5f5936'
info: mathlib: checking out revision 'a97b21ff86ea58a827f0d95be7ff3d799647b417'
info: updating toolchain to 'leanprover/lean4:v4.16.0-rc1'
info: restarting Lake via Elan
info: downloading component 'lean'
261.1 MiB / 261.1 MiB (100 %) 248.0 KiB/s ETA:   0 s
info: installing component 'lean'
info: toolchain not updated; already up-to-date
info: UnicodeBasic: checking out revision '470c41643209208d325a5a7315116f293c7443fb'
info: BibtexQuery: checking out revision '46376bc3c8f46ac1a1fd7712856b0f7bd6166098'
info: MD4Lean: checking out revision 'f8ed91f3a9d806648ae6a03ab98c8b87e8bedc7e'
warning: ././.lake/packages/MD4Lean/lakefile.lean:13:61: warning: `Lake.BuildJob` has been deprecated: use `Lake.Job` instead

warning: ././.lake/packages/MD4Lean/lakefile.lean:26:45: warning: `Lake.BuildJob` has been deprecated: use `Lake.Job` instead

info: plausible: checking out revision '2c57364ef83406ea86d0f78ce3e342079a2fece5'
info: importGraph: checking out revision '9a0b533c2fbd6195df067630be18e11e4349051c'
warning: ././.lake/packages/proofwidgets/lakefile.lean:28:63: warning: `Lake.BuildJob` has been deprecated: use `Lake.Job` instead

warning: ././.lake/packages/proofwidgets/lakefile.lean:40:13: warning: `Lake.BuildJob.collectArray` has been deprecated: use `Lake.Job.collectArray` instead

warning: ././.lake/packages/proofwidgets/lakefile.lean:46:29: warning: `Lake.BuildJob.bindSync` has been deprecated: use `Lake.Job.mapM` instead

info: aesop: checking out revision '2689851f387bb2cef351e6825fe94a56a304ca13'
info: Qq: checking out revision 'f0c584bcb14c5adfb53079781eeea75b26ebbd32'
info: batteries: checking out revision 'e8dc5fc16c625fc4fe08f42d625523275ddbbb4b'
info: mathlib: running post-update hooks
error: ././.lake/packages/doc-gen4/lakefile.lean:134:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:135:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:138:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:139:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:142:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:144:2: error: invalid field 'mapM', the environment does not contain 'Lake.BuildJob.mapM'
  exeJob
has type
  BuildJob FilePath

error: ././.lake/packages/doc-gen4/lakefile.lean:144:2: error: invalid field 'mapM', the environment does not contain 'Lake.Job.mapM'
  exeJob
has type
  Job (FilePath × BuildTrace)

error: ././.lake/packages/doc-gen4/lakefile.lean:144:2: error: invalid field 'mapM', the environment does not contain 'Lake.JobCore.mapM'
  exeJob
has type
  JobCore (JobTask (FilePath × BuildTrace))

error: ././.lake/packages/doc-gen4/lakefile.lean:156:22: error: failed to synthesize
  FamilyOut CustomData (bibPrepass.pkg, bibPrepass.name) ?m.7376
Additional diagnostic information may be available using the `set_option diagnostics true` command.

error: ././.lake/packages/doc-gen4/lakefile.lean:160:20: error: unknown constant 'Lake.Job.mixArray'

error: ././.lake/packages/doc-gen4/lakefile.lean:164:2: error: invalid field notation, type is not of the form (C ...) where C is a constant
  depDocJobs
has type
  ?m.9091 mod exeJob bibPrepassJob modJob imports __do_lift✝¹

error: ././.lake/packages/doc-gen4/lakefile.lean:179:22: error: failed to synthesize
  FamilyOut CustomData (bibPrepass.pkg, bibPrepass.name) ?m.9229
Additional diagnostic information may be available using the `set_option diagnostics true` command.

error: ././.lake/packages/doc-gen4/lakefile.lean:183:2: error: invalid field notation, type is not of the form (C ...) where C is a constant
  bibPrepassJob
has type
  ?m.10597 exeJob

error: ././.lake/packages/doc-gen4/lakefile.lean:195:9: error: unknown constant 'Lake.Job.mixArray'

error: ././.lake/packages/doc-gen4/lakefile.lean:199:20: error: unknown constant 'Lake.Job.mixArray'

error: ././.lake/packages/doc-gen4/lakefile.lean:226:2: error: invalid field 'bindM', the environment does not contain 'Lake.BuildJob.bindM'
  exeJob
has type
  BuildJob FilePath

error: ././.lake/packages/doc-gen4/lakefile.lean:226:2: error: invalid field 'bindM', the environment does not contain 'Lake.Job.bindM'
  exeJob
has type
  Job (FilePath × BuildTrace)

error: ././.lake/packages/doc-gen4/lakefile.lean:226:2: error: invalid field 'bindM', the environment does not contain 'Lake.JobCore.bindM'
  exeJob
has type
  JobCore (JobTask (FilePath × BuildTrace))

error: ././.lake/packages/doc-gen4/lakefile.lean:241:20: error: unknown constant 'Lake.Job.mixArray'

error: ././.lake/packages/doc-gen4/lakefile.lean:248:2: error: invalid field 'bindM', the environment does not contain 'Lake.BuildJob.bindM'
  exeJob
has type
  BuildJob FilePath

error: ././.lake/packages/doc-gen4/lakefile.lean:248:2: error: invalid field 'bindM', the environment does not contain 'Lake.Job.bindM'
  exeJob
has type
  Job (FilePath × BuildTrace)

error: ././.lake/packages/doc-gen4/lakefile.lean:248:2: error: invalid field 'bindM', the environment does not contain 'Lake.JobCore.bindM'
  exeJob
has type
  JobCore (JobTask (FilePath × BuildTrace))

error: ././.lake/packages/doc-gen4/lakefile.lean: package configuration has errors
error: mathlib: failed to fetch cache
buzzard@brutus:~/lean-projects/FLT$

I was surprised to see lake downloading not one but two versions of Lean during the process but I must confess I don't pay much attention to the process usually.

[Yaël Dillies]

It changed the toolchain first to 4.16.0-rc1, then to 4.15.0

[Kevin Buzzard]

Indeed I started on leanprover/lean4:v4.15.0-rc1 (I assume I am usually on an rc because I work with mathlib master) and finished on leanprover/lean4:v4.15.0 according to lean-toolchain. (Just to add: I bumped mathlib yesterday and it worked fine, and I'm in no hurry to bump it again, I'm not trying to put pressure on here, I know it's the weekend, I'm just trying to be helpful)

[Pietro Monticone]

Same for #Equational by the way.

[Patrick Massot]

@Kim Morrison and @Mac Malone could we get some help here? It seems all projects using Mathlib are stuck in their upgrading.

[Sébastien Gouëzel]

FWIW, I had no problem upgrading Carleson in https://github.com/fpvandoorn/carleson/pull/202. Could it be related to the way the project is set up?

[Pietro Monticone]

The problem might arise when push.yml in the master branch (not push_pr.yml in the related PR branch) runs.

See https://leanprover.zulipchat.com/#narrow/stream/442935-Carleson/topic/.5BDOCS.5D.20New.20setup.20for.20doc-gen4

[Yaël Dillies]

How could this have anything to do with the project's CI? The failure occurs locally

[Pietro Monticone]

Because we use the docbuild thing in Carleson which means that we have separate “channels” to update Mathlib and Doc-Gen.

[Pietro Monticone]

I guess that the reason why it’s not failing locally for Carleson might be that it’s not updating doc-gen.

[Pietro Monticone]

Yep, now I am at home and can confirm:

docbuild % lake update carleson
info: docbuild: no previous manifest, creating one from scratch
info: leanprover/doc-gen4: cloning https://github.com/leanprover/doc-gen4
info: leanprover/doc-gen4: checking out revision '535c69d52d2359e7973c9c7bdc4041845dfab27e'
info: updating toolchain to 'leanprover/lean4:v4.16.0-rc1'
info: restarting Lake via Elan
info: docbuild: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
info: UnicodeBasic: cloning https://github.com/fgdorais/lean4-unicode-basic
info: UnicodeBasic: checking out revision '470c41643209208d325a5a7315116f293c7443fb'
info: BibtexQuery: cloning https://github.com/dupuisf/BibtexQuery
info: BibtexQuery: checking out revision '46376bc3c8f46ac1a1fd7712856b0f7bd6166098'
info: MD4Lean: cloning https://github.com/acmepjz/md4lean
info: MD4Lean: checking out revision 'f8ed91f3a9d806648ae6a03ab98c8b87e8bedc7e'
warning: ././.lake/packages/MD4Lean/lakefile.lean:13:61: warning: `Lake.BuildJob` has been deprecated: use `Lake.Job` instead

warning: ././.lake/packages/MD4Lean/lakefile.lean:26:45: warning: `Lake.BuildJob` has been deprecated: use `Lake.Job` instead

warning: ././.lake/packages/proofwidgets/lakefile.lean:28:63: warning: `Lake.BuildJob` has been deprecated: use `Lake.Job` instead

warning: ././.lake/packages/proofwidgets/lakefile.lean:40:13: warning: `Lake.BuildJob.collectArray` has been deprecated: use `Lake.Job.collectArray` instead

warning: ././.lake/packages/proofwidgets/lakefile.lean:46:29: warning: `Lake.BuildJob.bindSync` has been deprecated: use `Lake.Job.mapM` instead

info: mathlib: running post-update hooks
error: ././.lake/packages/doc-gen4/lakefile.lean:134:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:135:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:138:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:139:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:142:4: error: unknown identifier 'addTrace'

error: ././.lake/packages/doc-gen4/lakefile.lean:144:2: error: invalid field 'mapM', the environment does not contain 'Lake.BuildJob.mapM'
  exeJob
has type
  BuildJob FilePath

error: ././.lake/packages/doc-gen4/lakefile.lean:144:2: error: invalid field 'mapM', the environment does not contain 'Lake.Job.mapM'
  exeJob
has type
  Job (FilePath × BuildTrace)

error: ././.lake/packages/doc-gen4/lakefile.lean:144:2: error: invalid field 'mapM', the environment does not contain 'Lake.JobCore.mapM'
  exeJob
has type
  JobCore (JobTask (FilePath × BuildTrace))

error: ././.lake/packages/doc-gen4/lakefile.lean:156:22: error: failed to synthesize
  FamilyOut CustomData (bibPrepass.pkg, bibPrepass.name) ?m.7376
Additional diagnostic information may be available using the `set_option diagnostics true` command.

error: ././.lake/packages/doc-gen4/lakefile.lean:160:20: error: unknown constant 'Lake.Job.mixArray'

error: ././.lake/packages/doc-gen4/lakefile.lean:164:2: error: invalid field notation, type is not of the form (C ...) where C is a constant
  depDocJobs
has type
  ?m.9091 mod exeJob bibPrepassJob modJob imports __do_lift✝¹

error: ././.lake/packages/doc-gen4/lakefile.lean:179:22: error: failed to synthesize
  FamilyOut CustomData (bibPrepass.pkg, bibPrepass.name) ?m.9229
Additional diagnostic information may be available using the `set_option diagnostics true` command.

error: ././.lake/packages/doc-gen4/lakefile.lean:183:2: error: invalid field notation, type is not of the form (C ...) where C is a constant
  bibPrepassJob
has type
  ?m.10597 exeJob

error: ././.lake/packages/doc-gen4/lakefile.lean:195:9: error: unknown constant 'Lake.Job.mixArray'

error: ././.lake/packages/doc-gen4/lakefile.lean:199:20: error: unknown constant 'Lake.Job.mixArray'

error: ././.lake/packages/doc-gen4/lakefile.lean:226:2: error: invalid field 'bindM', the environment does not contain 'Lake.BuildJob.bindM'
  exeJob
has type
  BuildJob FilePath

error: ././.lake/packages/doc-gen4/lakefile.lean:226:2: error: invalid field 'bindM', the environment does not contain 'Lake.Job.bindM'
  exeJob
has type
  Job (FilePath × BuildTrace)

error: ././.lake/packages/doc-gen4/lakefile.lean:226:2: error: invalid field 'bindM', the environment does not contain 'Lake.JobCore.bindM'
  exeJob
has type
  JobCore (JobTask (FilePath × BuildTrace))

error: ././.lake/packages/doc-gen4/lakefile.lean:241:20: error: unknown constant 'Lake.Job.mixArray'

error: ././.lake/packages/doc-gen4/lakefile.lean:248:2: error: invalid field 'bindM', the environment does not contain 'Lake.BuildJob.bindM'
  exeJob
has type
  BuildJob FilePath

error: ././.lake/packages/doc-gen4/lakefile.lean:248:2: error: invalid field 'bindM', the environment does not contain 'Lake.Job.bindM'
  exeJob
has type
  Job (FilePath × BuildTrace)

error: ././.lake/packages/doc-gen4/lakefile.lean:248:2: error: invalid field 'bindM', the environment does not contain 'Lake.JobCore.bindM'
  exeJob
has type
  JobCore (JobTask (FilePath × BuildTrace))

error: ././.lake/packages/doc-gen4/lakefile.lean: package configuration has errors
error: mathlib: failed to fetch cache

[Kim Morrison]

The title of this thread is wrong, I think. No one is experiencing problems with v4.15.0, it's only v4.16.0-rc1 from what I can see above?

[Kim Morrison]

I think what has gone wrong is that we prematurely merged https://github.com/leanprover/doc-gen4/pull/255, the PR bumping doc-gen4 to v4.16.0-rc1, because doc-gen4 CI isn't set up to fail on warnings.

[Kim Morrison]

See https://github.com/leanprover/doc-gen4/actions/runs/12607913996/job/35139815612#step:3:79

[Kim Morrison]

https://github.com/leanprover/doc-gen4/issues/256

[Kim Morrison]

@Henrik Böving, would you be able to update the CI so this doesn't happen?

[Kim Morrison]

Actually, maybe this is really a question for @Austin Letson --- could we change the default for lean-action to fail if there are warning during the build?

[Kim Morrison]

Okay, https://github.com/acmepjz/md4lean/pull/4 is the (trivial) fix required for md4lean. We're now blocked on merging this. I've asked @Jz Pan for write access to this repository so that I can make fixes like this directly during future releases.

[Kim Morrison]

Looking further at the messages above, I suspect people are using mismatched versions of things. If you want to be on toolchain v4.16.0-rc1, you need to be using ProofWidgets at v0.0.50, and I don't think you should be seeing the errors messages that @Pietro Monticone saw above!

[Henrik Böving]

Kim Morrison said:

Actually, maybe this is really a question for Austin Letson --- could we change the default for lean-action to fail if there are warning during the build?

I made the change to doc-gen in https://github.com/leanprover/doc-gen4/pull/257, unfortunately, unlike it should, the CI does not error on building doc-gen itself as it recovers the build from a cache, this seems to be an indicator to me that the cache key used to compute build results is not taking into accounts things like change of arguments etc. This should probably also be addressed @Austin Letson. Alternatively maybe this is not an issue with lean-action itself but with lake, I can't quite tell.

[Kim Morrison]

@Yaël Dillies or @Pietro Monticone, could you please post instructions to reproduce your problems? (starting with a git clone)

[Yaël Dillies]

1. Open LeanCamCombi in gitpod
2. Run scripts/update_mathlib.sh

[Kim Morrison]

I suspect what is going on is that you are running lake update, that is seeing that Batteries doc-gen4 is already at v4.16.0-rc1, so it is moving the toolchain to that, but then you are still using v0.0.48 or v0.0.49 of ProofWidgets, which is not compatible with v4.16.0-rc1

[Yaël Dillies]

Yes, that sounds plausible, since I see the toolchain jump back and forth when I run lake update

[Patrick Massot]

Kim, thanks a lot for investigating this :pray:

[Kim Morrison]

Yaël Dillies said:

1. Open LeanCamCombi in gitpod
2. Run scripts/update_mathlib.sh

@Yaël Dillies two suggestions:

1. It is more helpful if you give a URL, rather than asking people to google for the repo.
2. Specifying a commit is helpful for reproducibility.

[Kim Morrison]

@Mac Malone, I think this comes down to unfortunate behaviour of lake's new ability to update the toolchain automatically.

To reproduce:

git clone git@github.com:YaelDillies/LeanCamCombi.git
cd LeanCamCombi
git checkout 6a6a670f324b2af82ae17f21f9d51ac0bc859f6f
lake -R -Kenv=dev update

this then prints:

info: updating toolchain to 'leanprover/lean4:v4.16.0-rc1'
info: restarting Lake via Elan
info: toolchain not updated; already up-to-date
warning: ././.lake/packages/proofwidgets/lakefile.lean:28:63: warning: `Lake.BuildJob` has been deprecated: use `Lake.Job` instead

followed by many more warnings and errors.

What is going on here?

• lake looks at the two declarated dependencies, Mathlib and doc-gen4
• sees that they respectively ask for the toolchains v4.15.0 and v4.16.0-rc1
• correctly decides that v4.16.0-rc1 is "the latest"
• and tries to switch the toolchain to that

which then breaks everything, because Mathlib master can't cope with v4.16.0-rc1. (In particular, Mathlib master is using ProofWidgets v0.0.48, resulting in the first warning above.)

[Kim Morrison]

What we need here is support from lake for specifying in the lakefile which dependency to track for the purposes of the toolchain. In this situation, we really want to stay on v4.15.0, because Mathlib being on the right toolchain is more critical than doc-gen4 being on the right toolchain.

[Kim Morrison]

(In practice, even that is not going to work, and running lake update is simply doomed when Mathlib master and doc-gen4 main rely on different toolchains, as they do today.)

[Kim Morrison]

Intermediate solutions:

1. we can just go ahead and merge #20464, getting Mathlib onto v4.16.0-rc1, so everything is available at the same toolchain
2. we can please stop adding doc-gen4 as a dependency to development projects, and instead generate docs in a supplementary project, as discussed previously, until such time as we can drop/replace doc-gen4.

[Yaël Dillies]

Last time I tried (a month and a half ago), I failed to understand how to get the new setup working. It's been on my todo list but hasn't bubbled up to the top yet

[Yaël Dillies]

Sorry, I would have given you the link but it's really hard to get it right from a phone

[Pietro Monticone]

I run the following once again and it worked:

git clone https://github.com/sgouezel/carleson.git
cd carleson
git fetch origin SG_bump_415
git checkout SG_bump_415
lake exe cache get
lake build
cd docbuild
../scripts/setup_lake_package_symlinks.sh
lake update carleson

Now both projects (carleson and docbuild) live on lean4:v4.15.0 and everything works fine.

Please note that the Carleson's setup is not yet aligned with the latest recommendations outlined in the doc-gen4 README.

Thank you so much Kim for your help!

[Eric Wieser]

Kim Morrison said:

1. we can just go ahead and merge #20464, getting Mathlib onto v4.16.0-rc1, so everything is available at the same toolchain

This will not help projects who want to produce a commit at v4.15.0, which I believe is the recommended thing to do if they want others to be able to depend on them. For projects in this situation that are struggling with point 2, is the second best choice for them to pin doc-gen in their lakefile to the same lean version as mathlib?

[François G. Dorais]

For scripts, I think it's useful to run lake with --keep-toolchain unless the script wants to use lake to figure out the correct toolchain.

[Jz Pan]

Kim Morrison said:

Okay, https://github.com/acmepjz/md4lean/pull/4 is the (trivial) fix required for md4lean. We're now blocked on merging this. I've asked Jz Pan for write access to this repository so that I can make fixes like this directly during future releases.

Merged.

[Kim Morrison]

Yes, pinning doc-gen4 seems to be a reasonable option.

[Yaël Dillies]

@Kim Morrison, here's my attempt to get this new setup working:

1. Open https://gitpod.io/#https://github.com/YaelDillies/LeanCamCombi
2. git checkout 6a6a670f324b2af82ae17f21f9d51ac0bc859f6f
3. Follow the instructions over at https://github.com/leanprover/doc-gen4/blob/main/README.md

[Yaël Dillies]

lake update doc-gen4 within step 3 fails with the same errors as at the start of this topic

[Yaël Dillies]

I am giving up for now, but feel free to ping me whenever the new instructions work

[Henrik Böving]

Yaël Dillies said:

lake update doc-gen4 within step 3 fails with the same errors as at the start of this topic

It works without the above error for me, did you follow the advice to pin doc-gen to a certain tag if you are developing against a certain revision, so in your case v4.15.0-rc1?

[Yaël Dillies]

Ah no, I did not. How does one do that with lakefile.toml?

[Henrik Böving]

It says in the template

name = "docbuild"
reservoir = false
version = "0.1.0"
packagesDir = "../.lake/packages"

[[require]]
name = "Your Library Name"
path = "../"

[[require]]
scope = "leanprover"
name = "doc-gen4"
# Use revision v4.x if you are developing against a stable Lean version.
rev = "main"

just put the tag at rev instead of "main"

[Yaël Dillies]

Aaah, okay. It wasn't clear this was meant literally. Lean releases are referred to differently in other parts of the ecosystem

[Henrik Böving]

What would you expect the sentence to be to make sense for the more casual user?

[Yaël Dillies]

# If you are developing against a stable Lean version `v4.x`, replace `main` below by `v4.x`

[Yaël Dillies]

Doesn't work still, I now get

gitpod /workspace/LeanCamCombi/docbuild ((6a6a670...)) $ lake update doc-gen4
info: docbuild: no previous manifest, creating one from scratch
info: leanprover/doc-gen4: checking out revision '099b90e374ba73983c3fda87595be625f1931669'
info: updating toolchain to 'leanprover/lean4:v4.15.0-rc1'
info: restarting Lake via Elan
info: docbuild: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
info: UnicodeBasic: checking out revision 'd55279d2ff01759fa75752fcf1a93d1db8db18ff'
info: BibtexQuery: checking out revision '982700bcf78b93166e5b1af0b4b756b8acfdb54b'
info: MD4Lean: URL has changed; deleting '././../.lake/packages/MD4Lean' and cloning again
info: MD4Lean: cloning https://github.com/acmepjz/md4lean
info: MD4Lean: checking out revision 'fe8e6e649ac8251f43c6f6f934f095ebebce7e7c'
info: mathlib: running post-update hooks
uncaught exception: no such file or directory (error code: 2)
  file: .lake/packages/mathlib/lakefile.lean
error: mathlib: failed to fetch cache

[Yaël Dillies]

My lakefile.toml is

name = "docbuild"
reservoir = false
version = "0.1.0"
packagesDir = "../.lake/packages"

[[require]]
name = "LeanCamCombi"
path = "../"

[[require]]
scope = "leanprover"
name = "doc-gen4"
# Use revision v4.x if you are developing against a stable Lean version.
rev = "v4.15.0-rc1"

[Henrik Böving]

Yaël Dillies said:

Doesn't work still, I now get

gitpod /workspace/LeanCamCombi/docbuild ((6a6a670...)) $ lake update doc-gen4
info: docbuild: no previous manifest, creating one from scratch
info: leanprover/doc-gen4: checking out revision '099b90e374ba73983c3fda87595be625f1931669'
info: updating toolchain to 'leanprover/lean4:v4.15.0-rc1'
info: restarting Lake via Elan
info: docbuild: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
info: UnicodeBasic: checking out revision 'd55279d2ff01759fa75752fcf1a93d1db8db18ff'
info: BibtexQuery: checking out revision '982700bcf78b93166e5b1af0b4b756b8acfdb54b'
info: MD4Lean: URL has changed; deleting '././../.lake/packages/MD4Lean' and cloning again
info: MD4Lean: cloning https://github.com/acmepjz/md4lean
info: MD4Lean: checking out revision 'fe8e6e649ac8251f43c6f6f934f095ebebce7e7c'
info: mathlib: running post-update hooks
uncaught exception: no such file or directory (error code: 2)
  file: .lake/packages/mathlib/lakefile.lean
error: mathlib: failed to fetch cache

Yes this is unfortunately a known mathlib issue and just a bug in Cache, you can in fact just ignore it and continue on with your life.

[Henrik Böving]

I was hoping that someone :tm: would just get to fixing it but I guess I'll put a note in doc-gen specifically for mathlib

[Edward van de Meent]

Henrik Böving said:

[...]

Yes this is unfortunately a known mathlib issue and just a bug in Cache, you can in fact just ignore it and continue on with your life.

in the sense that the error is a lie and it does work? or in the sense that running lake exe cache get is only a QOL thing and you can just build the project yourself?

[Henrik Böving]

Cache currently doesn't respect the packagesDir flag of lakefile.toml so it just looks in the wrong directory for a mathlib checkout and then throws this error. If you run lake exe cache get from your actual project directory everything just works.

[Henrik Böving]

Okay I put out an update to the setup instructions to account for the mathlib error and the unclear instructions with respect to the revision.

[Yaël Dillies]

Btw in "against a stable Lean version", we can actually use non-stable versions (aka release candidates), right?

[Henrik Böving]

Right, it's more of a "not against nightly", not quite sure how to describe the sets of versions that contain rcs and full releases but not nightlies

[Yaël Dillies]

"a release candidate or a stable version"?

[Henrik Böving]

Updated again

[Yaël Dillies]

Okay so I pinned the rev to v4.15.0-rc1. Then I thought I would try updating mathlib. So I did

1. In docbuild, pin the rev to v4.16.0-rc1
2. lake update in the root folder
3. cd docbuild
4. lake update LeanCamCombi
5. cd ../
6. lake exe cache get
7. lake build

[Yaël Dillies]

But then the cache doesn't work and lake build starts rebuilding all of mathlib

[Henrik Böving]

Yes, due to the bug in the Cache you need to build from the root directory of your project, there Cache is going to work, then you can go back to your docbuild directory and work there.

[Yaël Dillies]

Ah sorry, I missed a step. Edited

[Yaël Dillies]

lake build is failing in the root directory

[Henrik Böving]

And a manual lake exe cache get also doesn't help that?

[Yaël Dillies]

Nope

[Henrik Böving]

Then I also don't know what's wrong with Cache, I would suspect that just hard removing .lake and running lake exe cache get is going to fix it but that's not a very nice solution of course.

[Henrik Böving]

I mean, evidently we are messing with what the people that put Cache in place intended when we set the above environment variable. So maybe just fixing that bug would already get us some of the way there.

[Frédéric Dupuis]

I'm also having problems upgrading a local project that depends on mathlib to v4.16.0-rc1. If I delete the .lake folder and run lake exe cache get, everything seems to work fine, but then if I run lake build on the project, it starts to compile everything.

[Frédéric Dupuis]

Could it have anything to do with the fact that Qq is still on v4.15.0?

[Kevin Buzzard]

@Pietro Monticone bumped FLT to current mathlib master and I merged, but I can also confirm that lake exe cache get no longer works for me (even after rm -rf .lake and lake exe cache get!); mathlib starts building from source even though 5000+ files were downloaded without error. So I've reverted the commit and I'm still unable to get FLT working on current mathlib (at least without building mathlib from source)

[Joachim Breitner]

I also observe lake build rebuilding everything despite cache downloading lots of files, on live.lean-lang.org. Clean checkout, latest elan. Does not happen with mathlib stable.

[Julian Berman]

The same thing happened yesterday to @Aaron Hill -- it might be a different issue but just to be sure, what fixed it for him was deleting the mathlib cache. Have folks confirmed whether that works for you too?

[Julian Berman]

I.e. rm -f of ~/.cache/mathlib or wherever your MATHLIB_CACHE_DIR is, followed by lake exe cache get again, and then lake build to check whether things are now happy.

[Joachim Breitner]

Heh, just deleting that directory on live.lean-lang.org takes a lot of time :-) (and removes >100GB of data)

[Joachim Breitner]

Nope, does not help here.

[Julian Berman]

Unfortunate. But ok, early spring cleaning sounds like :)

[Eric Wieser]

Yaël Dillies said:

Okay so I pinned the rev to v4.15.0-rc1

Isn't 4.15.0rc1 from long ago?

[Mauricio Collares]

Kevin Buzzard said:

Pietro Monticone bumped FLT to current mathlib master and I merged, but I can also confirm that lake exe cache get no longer works for me (even after rm -rf .lake and lake exe cache get!); mathlib starts building from source even though 5000+ files were downloaded without error. So I've reverted the commit and I'm still unable to get FLT working on current mathlib (at least without building mathlib from source)

In your v4.16.0-rc1 update I see this behaviour:

$ lake exe cache get
[...snip...]
$ cat ./.lake/packages/mathlib/.lake/build/lib/Mathlib/Tactic/Linter/Header.trace
{"log":[],"depHash":"16549332353800634075"}
$ lake build --no-ansi
⚠ [317/5889] Replayed FLT.Junk.Algebra
warning: ././././FLT/Junk/Algebra.lean:1:0: using 'exit' to interrupt Lean
⚠ [318/5889] Replayed FLT.Junk.Algebra2
warning: ././././FLT/Junk/Algebra2.lean:1:0: using 'exit' to interrupt Lean
✔ [320/5889] Built Mathlib.Tactic.Linter.Header
[...]
$ cat ./.lake/packages/mathlib/.lake/build/lib/Mathlib/Tactic/Linter/Header.trace
{"log":
 [{"message": "...snip...",
   "level": "trace"}],
 "depHash": "1306935599467847507"}

But the only files Mathlib/Tactic/Linter/Header.lean imports are core Lean files. The oleans/ileans for this file are the same before and after lake build, only the trace changes.

[Eric Wieser]

I think everyone should avoid updating to 4.16.0rc1 until they have updated to 4.15.0, otherwise it is very hard for someone to use multiple projects together

[Eric Wieser]

But we can't update to 4.15.0 without first declaring one of these commits to be 4.15.0, as the v4.15.0 tag as of writing does not exist

[Eric Wieser]

@Kim Morrison, did you already create this tag and forget to push?

[Eric Wieser]

I think the two clear choices for the tag are 29f9a66d622d9bab7f419120e22bb0d2598676ab (the very first commit at 4.15.0) or 9837ca9d65d9de6fad1ef4381750ca688774e608(the very last commit at 4.15.0). I think we should take the latter to get slightly more mathlib in that release, unless there are reasons to prefer the former.

[Paige Thomas]

(deleted)

[Mauricio Collares]

If I build Mathlib itself at b552a67b9245b0012c186a4a06f519600b151e28, then I get:

$ lake build Mathlib.Tactic.Linter.Header
Build completed successfully.

$ cat .lake/build/lib/Mathlib/Tactic/Linter/Header.trace
{"log":
 [{"message": "...snip...",
   "level": "trace"}],
 "depHash": "16549332353800634075"}

But if I build https://github.com/ImperialCollegeLondon/FLT at commit 3fbdf303085b8bbf890d4f9dd13caa227ccffbfa, which imports mathlib at b552a67b9245b0012c186a4a06f519600b151e28, I get:

$ lake build Mathlib.Tactic.Linter.Header
Build completed successfully.

$ cat .lake/packages/mathlib/.lake/build/lib/Mathlib/Tactic/Linter/Header.trace
{"log":
 [{"message": "...snip...",
   "level": "trace"}],
 "depHash": "1306935599467847507"}

@Mac Malone this seems like a regression in v4.16.0-rc1, maybe fallout from lean4#6388? The oleans/ileans are identical, only the trace changes. This is the "first" file for which the trace changes in this way.

[Mauricio Collares]

Mauricio Collares said:

This is the "first" file for which the trace changes in this way.

This is probably just because it's the first file to be built in Mathlib (i.e. doesn't come from batteries or another dep)

[Kim Morrison]

Thanks, I had indeed forgotten to tag v4.15.0, and I've done so now (at 9837ca9d65d9de6fad1ef4381750ca688774e608).

[Eric Wieser]

Thanks!

[Eric Wieser]

(I'm a little surprised no one else in this thread noticed!)

[Kim Morrison]

I've been meaning to write a "toolchain release dashboard" that would display the status of all the steps, but so far can't justify the time investment for something that will only be used twice a month... But it hopefully would save a lot of these manual catches!!

[Kim Morrison]

Still slightly buggy, but 15 minutes with Claude gives:

% ./release_checklist.py v4.15.0

Repository: Batteries
  ✅ On compatible toolchain (>= v4.15.0)
  ✅ Toolchain tag exists
  ❌ Toolchain tag is not merged into the stable branch

Repository: lean4checker
  ✅ On compatible toolchain (>= v4.15.0)
  ✅ Toolchain tag exists
  ✅ Toolchain tag is merged into the stable branch

Repository: doc-gen4
  ✅ On compatible toolchain (>= v4.15.0)
  ✅ Toolchain tag exists

Repository: Verso
  ✅ On compatible toolchain (>= v4.15.0)
  ✅ Toolchain tag exists

Repository: ProofWidgets4
  ✅ On compatible toolchain (>= v4.15.0)

Repository: Aesop
  ✅ On compatible toolchain (>= v4.15.0)
  ✅ Toolchain tag exists
  ✅ Toolchain tag is merged into the stable branch

Repository: import-graph
  ✅ On compatible toolchain (>= v4.15.0)
  ✅ Toolchain tag exists

Repository: plausible
  ❌ Not on target toolchain (needs >= v4.15.0)

Repository: Mathlib
  ❌ Not on target toolchain (needs >= v4.15.0)

Repository: REPL
  ❌ Not on target toolchain (needs >= v4.15.0)

[Kim Morrison]

As usual, bug fixing takes twice as long as initial implementation, but it is looking pretty good now. I've run it over v4.14.0, v4.15.0-rc1, v4.15.0, and v4.16.0-rc1 and fixed a few problems!

[Kim Morrison]

lean#6542

[Eric Wieser]

Nice! To be clear, my comment was not a complaint that this slipped through, but a complaint that in a thread titled "updating to 4.15.0", seemingly not one person was actually performing an update to 4.15.0.

[Kim Morrison]

I think my current advice is to not attempt to update downstream projects to v4.16.0-rc1 yet. It will likely take us a week until we're ready to release rc2 (people are still on holidays!).

In the meantime though, as far as I'm aware there is no obstacle to updating all downstream projects to v4.15.0 (possibly needing to manually pin your doc-gen4 requires to the v4.15.0 tag of doc-gen4, and possibly using lake update --keep-toolchain instead of lake update).

[Kim Morrison]

If @Yaël Dillies / @Pietro Monticone / anyone else attempting bumps could try the v4.15.0 bump with those caveats and report back, that would be great. :-)

[Frédéric Dupuis]

Going to v4.15.0 works fine for my project (but I'm not using doc-gen, it's just a regular project).

[Paige Thomas]

If I'm creating a new project should I run something like lake +leanprover/lean4:v4.15.0 new my_project math and then lake update --keep-toolchain?

[Paige Thomas]

That seems to create more files in the generated project than lake +leanprover/lean4:nightly-2024-04-24 new my_project math? Should I have been doing that all along?

[Paige Thomas]

For some reason it also set the toolchain to leanprover/lean4:v4.16.0-rc1?

[François G. Dorais]

In the current settings, you need to invoke lake --keep-toolchain (almost) every time.

[Paige Thomas]

Do you mean I should run lake +leanprover/lean4:v4.15.0 new my_project math --keep-toolchain?

[Paige Thomas]

It seems no matter how I create a new project it sets the toolchain to leanprover/lean4:v4.16.0-rc1.

[Ruben Van de Velde]

I think that's expected, yeah. For now you'll need to manually change the toolchain

[Kim Morrison]

https://github.com/ImperialCollegeLondon/FLT/pull/305 I think successfully updates FLT to v4.15.0

[Kim Morrison]

and
https://github.com/ImperialCollegeLondon/FLT/pull/306, which we can't merge yet, is a reproducible example of the cache failing in all projects downstream of Mathlib on v4.16.0-rc1.

[Yaël Dillies]

Eric Wieser said:

in a thread titled "updating to 4.15.0", seemingly not one person was actually performing an update to 4.15.0.

At the start of this thread I was updating to the latest mathlib, which for a few hours meant 4.15.0

[Mauricio Collares]

@Kim Morrison I didn't check if the trace for a given mathlib file is the same for all downstream projects. If it is, there is a hack one can do to make cache work without a new Lean release: just push two sets of cache files, one valid for mathlib itself and one valid for downstream projects.

[Mauricio Collares]

But this depends on whether leangz stores the trace file or recomputes it

[Mauricio Collares]

Just checked that Mathlib/Tactic/Linter/Header.trace in FLT is the same as in a brand-new project created with lake new math (pinned to the same mathlib commit, of course). Unfortunately the above hack is not a viable solution because (even with the modified trace) the compiled files for Mathlib/Tactic/Linter/Header.lean get packed as 084e8150a7e80f16.ltar. The ltar changes when the trace changes (you can see the changed trace starting at byte 0x42, but you have to be careful to delete the appropriate files in ~/.cache/mathlib because otherwise it doesn't get overwritten), but the filename itself is the same.

[David Loeffler]

I think my current advice is to not attempt to update downstream projects to v4.16.0-rc1 yet. It will likely take us a week until we're ready to release rc2 (people are still on holidays!).

Just coming over to this thread from another one I started here. If this is unlikely to be resolved in a week, then I am going to need a work-around for the course I am teaching which starts next Monday. So, what steps should I follow (more accurately: advise students to follow) in order to create a new Lean project that imports a reasonably recent version of mathlib, without recompiling mathlib it from scratch?

[Eric Wieser]

Pinning to 4.15.0 should work for you, though I don't remember the lake new invocation to do that

[Yaël Dillies]

You can change the require line to say

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0"

[Mauricio Collares]

Or, if your project uses lakefile.toml (this is the default for lake new PROJECT_NAME math, so it's likely), you should add a rev = "v4.15.0" line like this:

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

If any lake command is run inside the project (for example, if the project was created using the VS Code extension, which should call lake exe cache get) before you did the change, you probably need to run lake update after this change.

[Mauricio Collares]

Both options are really not ideal if you're not creating the project yourself, but I can't think of anything better. I guess you can supply a correct lake-manifest.json (and perhaps a lakefile.toml as well) and ask students to just overwrite their copy with yours.

Eric Wieser said:

Pinning to 4.15.0 should work for you, though I don't remember the lake new invocation to do that

There is none, I just checked.

[Yaël Dillies]

Kim Morrison said:

If Yaël Dillies / Pietro Monticone / anyone else attempting bumps could try the v4.15.0 bump with those caveats and report back, that would be great. :-)

It works :tada:

[Jz Pan]

Kevin Buzzard said:

Pietro Monticone bumped FLT to current mathlib master and I merged, but I can also confirm that lake exe cache get no longer works for me (even after rm -rf .lake and lake exe cache get!); mathlib starts building from source even though 5000+ files were downloaded without error. So I've reverted the commit and I'm still unable to get FLT working on current mathlib (at least without building mathlib from source)

Same problem here. I'm giving a talk of Lean today and distributed pre-packaged Lean4 Windows version to students. Suddenly I found that the downloaded mathlib cache doesn't work as expected :(

[Mauricio Collares]

Mauricio Collares said:

Kim Morrison I didn't check if the trace for a given mathlib file is the same for all downstream projects. If it is, there is a hack one can do to make cache work without a new Lean release: just push two sets of cache files, one valid for mathlib itself and one valid for downstream projects.

Ah, the filename is not generated by leangz but by the cache script. So in principle this hack can work, and it only requires changes to mathlib. It would require generating a different filename for each .ltar file when the dephash in the trace file changes (but changes to the rest of the trace file shouldn't affect it). That's just reading a value from a JSON file, so it shouldn't be too bad to implement, but there's the question of whether uploading duplicated cache files in CI for downstream projects (as a temporary workaround) is a good idea.

[Jz Pan]

Mauricio Collares said:

Or, if your project uses lakefile.toml (this is the default for lake new PROJECT_NAME math, so it's likely), you should add a rev = "v4.15.0" line like this:

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

If any lake command is run inside the project (for example, if the project was created using the VS Code extension, which should call lake exe cache get) before you did the change, you probably need to run lake update after this change.

Thank you! Seems that this solution works.

[Pietro Monticone]

Kim Morrison said:

If Yaël Dillies / Pietro Monticone / anyone else attempting bumps could try the v4.15.0 bump with those caveats and report back, that would be great. :-)

• Worked for Carleson (see here).
• Worked for FLT (see here).

[David Loeffler]

Thanks @Mauricio Collares, your solution worked for me as well!

[Violeta Hernández]

I have a lakefile.lean instead of a lakefile.toml, is that what I should be using or should I somehow convert my file into a TOML?

[Pietro Monticone]

You can run lake translate-config toml in your repo to get the toml version.

[Mauricio Collares]

Yaël Dillies said:

You can change the require line to say

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0"

This is the lakefile.lean version

[Violeta Hernández]

Pietro Monticone said:

lake translate-config toml

Thanks! Is this the preferred version moving forwards?

[Mauricio Collares]

Yes, provided your configuration is not complicated

[Kevin Buzzard]

Do you happen to know whether the FLT configuration is "complicated"? https://github.com/ImperialCollegeLondon/FLT/blob/main/lakefile.lean (it's certainly complicated from where I'm sitting...)

[Mauricio Collares]

I don't know off the top of my head if the globs = part is supported in the toml configuration. Setting up doc-gen in a subdirectory can be done with a separate toml file (see the doc-gen README), and leanOptions are supported.

[Kim Morrison]

globs is supported in toml, c.f. the Aesop lakefile.toml

[Kim Morrison]

meta if is not supported in toml, and as Mauricio suggests the preferred solution is to run doc-gen in a subdirectory with it's own lakefile.toml.

[Kim Morrison]

feat: test the cache as if in a downstream project #20532

can't be merged as is, because v4.16.0-rc1 is broken, but having this in place would have alerted us to the problems in v4.16.0-rc1 when it was still in the nightly-testing process.

[Paige Thomas]

Mauricio Collares said:

Or, if your project uses lakefile.toml (this is the default for lake new PROJECT_NAME math, so it's likely), you should add a rev = "v4.15.0" line like this:

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

If any lake command is run inside the project (for example, if the project was created using the VS Code extension, which should call lake exe cache get) before you did the change, you probably need to run lake update after this change.

Is lake new PROJECT_NAME math preferred over lake +leanprover/lean4:nightly-2024-04-24 new PROJECT_NAME math? I've been following the instructions at https://leanprover-community.github.io/install/project.html#creating-a-lean-project.

[Eric Wieser]

The problem with bare lake new is that it could be any version of lake, depending on your setup

[Eric Wieser]

So it's terrible to include in instructions, as the reader might be using an ancient prerelease of lake

[Eric Wieser]

It surprises me that the instructions tell you to use a nightly and not stable though

[Paige Thomas]

Is this expected?

pthomas@HP-Laptop:~/Desktop/github/lean$ elan show
installed toolchains
--------------------

stable (default)
leanprover/lean4:nightly-2024-04-24
leanprover/lean4:v4.15.0

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

stable (default)
Lean (version 4.15.0, x86_64-unknown-linux-gnu, commit 11651562caae, Release)

pthomas@HP-Laptop:~/Desktop/github/lean$ lake new my_project math
info: downloading mathlib `lean-toolchain` file
pthomas@HP-Laptop:~/Desktop/github/lean$ cat my_project/
.git/           .gitignore      lean-toolchain  MyProject.lean
.github/        lakefile.toml   MyProject/      README.md
pthomas@HP-Laptop:~/Desktop/github/lean$ cat my_project/lean-toolchain
leanprover/lean4:v4.16.0-rc1
pthomas@HP-Laptop:~/Desktop/github/lean$ elan show
installed toolchains
--------------------

stable (default)
leanprover/lean4:nightly-2024-04-24
leanprover/lean4:v4.15.0

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

stable (default)
Lean (version 4.15.0, x86_64-unknown-linux-gnu, commit 11651562caae, Release)

[Paige Thomas]

I was expecting it to give me v4.15.0, since that is the latest that elan show gave.

[Paige Thomas]

Is elan saying here that the active toolchain is both stable and 4.15.0, ie, that they are one and the same?

[Paige Thomas]

What does the + do? I'm not sure I see it in the documentation?

[Paige Thomas]

What it does that is.

[Ruben Van de Velde]

Eric Wieser said:

It surprises me that the instructions tell you to use a nightly and not stable though

Doesn't that have the same issue?