lake update fails with a huge trace

Stream: lean4

[Shreyas Srinivas]

Running lake update on a v4.12.0-rc1 project failed with a rather long trace. Running it a second time produces a more terse error message:

trace: stderr:
From https://github.com/leanprover-community/mathlib4
   77419d668a..00c6a34c09  justus/laurent_polynomials2 -> origin/justus/laurent_polynomials2
error: ././.lake/packages/proofwidgets/lakefile.lean:83:2: error: invalid field 'afterBuildCacheAsync', the environment does not contain 'Lake.Package.afterBuildCacheAsync'
  pkg
has type
  Package
error: ././.lake/packages/proofwidgets/lakefile.lean: package configuration has errors

[Shreyas Srinivas]

I know how to fix this

[Shreyas Srinivas]

But in these messages I got a long git history of pull requests

[Shreyas Srinivas]

and I am not really sure whether as an ordinary user this is of much use to me. Perhaps the stderr stuff could go to an error.log file or something similar?

[Shreyas Srinivas]

A run with lake-manifest and .lake removed produced the following :

info: TimedAutomata: no previous manifest, creating one from scratch
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '././.lake/packages/mathlib'
trace: .> git clone https://github.com/leanprover-community/mathlib4.git ././.lake/packages/mathlib
trace: stderr:
Cloning into '././.lake/packages/mathlib'...
trace: ././.lake/packages/mathlib> git checkout --detach 1109970b9069835cb9d4cd69bf196c9fff7516f4 --
trace: stderr:
HEAD is now at 1109970b90 feat: `IntermediateField.rank_sup_le` (#19527)
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
trace: .> git clone https://github.com/leanprover-community/batteries ././.lake/packages/batteries
trace: stderr:
Cloning into '././.lake/packages/batteries'...
trace: ././.lake/packages/batteries> git checkout --detach c933dd9b00271d869e22b802a015092d1e8e454a --
trace: stderr:
HEAD is now at c933dd9b feat: List.dropPrefix? / dropSuffix? / dropInfix? and specification lemmas (#1066)
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
trace: .> git clone https://github.com/leanprover-community/quote4 ././.lake/packages/Qq
trace: stderr:
Cloning into '././.lake/packages/Qq'...
trace: ././.lake/packages/Qq> git checkout --detach 303b23fbcea94ac4f96e590c1cad6618fd4f5f41 --
trace: stderr:
HEAD is now at 303b23f chore: bump toolchain to v4.14.0-rc1 (#65)
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
trace: .> git clone https://github.com/leanprover-community/aesop ././.lake/packages/aesop
trace: stderr:
Cloning into '././.lake/packages/aesop'...
trace: ././.lake/packages/aesop> git checkout --detach de91b59101763419997026c35a41432ac8691f15 --
trace: stderr:
HEAD is now at de91b59 chore: bump batteries, follow deprecations (#179)
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
trace: .> git clone https://github.com/leanprover-community/ProofWidgets4 ././.lake/packages/proofwidgets
trace: stderr:
Cloning into '././.lake/packages/proofwidgets'...
trace: ././.lake/packages/proofwidgets> git checkout --detach 1383e72b40dd62a566896a6e348ffe868801b172 --
trace: stderr:
HEAD is now at 1383e72 Update RELEASES.md
error: ././.lake/packages/proofwidgets/lakefile.lean:83:2: error: invalid field 'afterBuildCacheAsync', the environment does not contain 'Lake.Package.afterBuildCacheAsync'
  pkg
has type
  Package
error: ././.lake/packages/proofwidgets/lakefile.lean: package configuration has errors

[Shreyas Srinivas]

which seems to indicate that ProofWidgets is broken somehow

[Alex Meiburg]

I had the same issue, and the solution in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.E2.9C.94.20Fails.20to.20lake.20update/near/476747076 worked for me. It means your lean version is out of date.

[Shreyas Srinivas]

Yeah I fixed that by updating my lean-toolchain

[Alex Meiburg]

Specfically because you're on v4.12.0-rc1 and the ProofWidgets lakefile is using v4.14.0-rc1, I think

[Shreyas Srinivas]

But I am reporting it here because this shouldn't be a problem in the first place.

[Alex Meiburg]

Ah makes sense

[Shreyas Srinivas]

There are several things going wrong here.

1. Lake is not using the manifest and lakefile info to tell me in advance that it can't perform the update before giving me a long list of Mathlib PRs.
2. It is giving me this long list of Mathlib PRs.
3. There is no CLI way to tell lake to use a specific toolchain to perform the lake update. Ideally lake should be figuring this out for itself. Of course now it is not possible to patch previous toolchains with a fix.
4. The error messages are being dumped in the terminal rather than an error log file that can be more easily shared here.

[Mac Malone]

@Shreyas Srinivas trace messages should only be printed in Lake's verbose mode. Are you rinning iwth -v?

[Shreyas Srinivas]

No I didn't add extra options

[Shreyas Srinivas]

Just lake update

[Shreyas Srinivas]

Incidentally an update on a different project from v4.6.0 proceeded smoothly when I changed the lean-toolchain to v4.13.0

[Mac Malone]

Oh, perhaps I have forgotten some Lake bug or pecularity of v4.12.0 that prints trace messages for some reason. Some good news is that in v4.15.0-rc1 lake will now attempt to update the package toolchain as part of the lake update process.

[Shreyas Srinivas]

Isn't that already the default for non math projects? Or, do you mean that lake update will use toolchain version a.b.c to update the project's dependencies to a.b.c

[Shreyas Srinivas]

What would be neat is if we could say lake update va.b.c and lake would first switch to that toolchain and update the project