Zulip Chat Archive
Stream: lean4
Topic: Invalid lake configuration
Bolton Bailey (Dec 03 2023 at 08:10):
I am getting the following error
`/Users/boltonbailey/.elan/toolchains/leanprover--lean4---v4.3.0/bin/lake print-paths Init FormalSnarksProject.Models.AGMProofSystemInstantiation Mathlib.Data.Polynomial.Div --no-build` failed:
stderr:
error: compiled configuration is invalid; run with `-R` to reconfigure
Invalid Lake configuration. Please restart the server after fixing the Lake configuration file.
My lakefile.lean looks like
import Lake
open Lake DSL
package «formalSnarksProject» {
-- add any package configuration options here
}
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
@[default_target]
lean_lib «FormalSnarksProject» {
-- add any library configuration options here
}
Bolton Bailey (Dec 03 2023 at 08:11):
Which seems the same as what I get from lake new test math
. What is going on?
Bolton Bailey (Dec 03 2023 at 08:13):
Furthermore, if I look in the lake --help, I see there is an -R option, but then it tells me it's missing the command?
boltonbailey@eduroamprvnat-172-16-41-159 FormalSnarksProject % lake --help
Lake version 5.0.0-8e5cf64 (Lean version 4.3.0)
USAGE:
lake [OPTIONS] <COMMAND>
COMMANDS:
new <name> <temp> create a Lean package in a new directory
init <name> <temp> create a Lean package in the current directory
build <targets>... build targets
exe <exe> <args>... build an exe and run it in Lake's environment
clean remove build outputs
env <cmd> <args>... execute a command in Lake's environment
update update dependencies and save them to the manifest
upload <tag> upload build artifacts to a GitHub release
script manage and run workspace scripts
scripts shorthand for `lake script list`
run <script> shorthand for `lake script run`
serve start the Lean language server
OPTIONS:
--version print version and exit
--help, -h print help of the program or a command and exit
--dir, -d=file use the package configuration in a specific directory
--file, -f=file use a specific file for the package configuration
--quiet, -q hide progress messages
--verbose, -v show verbose information (command invocations)
--lean=cmd specify the `lean` command used by Lake
-K key[=value] set the configuration file option named key
--old only rebuild modified modules (ignore transitive deps)
--rehash, -H hash all files for traces (do not trust `.hash` files)
--update, -U update manifest before building
--reconfigure, -R elaborate configuration files instead of using OLeans
See `lake help <command>` for more information on a specific command.
boltonbailey@eduroamprvnat-172-16-41-159 FormalSnarksProject % lake -R
error: missing command
Bolton Bailey (Dec 03 2023 at 08:21):
Screenshot-2023-12-03-at-2.20.51-AM.png
Why are there two mathlibs?
Bolton Bailey (Dec 03 2023 at 08:21):
Is it safe to just delete the .lean
folder and start again?
Utensil Song (Dec 03 2023 at 08:26):
If you were running lake build
, you'll need to run lake -R build
, the same applies to other commands
Bolton Bailey (Dec 03 2023 at 08:27):
Ok like this?
boltonbailey@eduroamprvnat-172-16-41-159 FormalSnarksProject % lake clean -R
boltonbailey@eduroamprvnat-172-16-41-159 FormalSnarksProject % lake update
mathlib: updating repository './.lake/packages/mathlib' to revision 'b1cd52acffa53bca04a33ddc14a40b2a62ed4308'
error: ./.lake/packages/mathlib/lakefile.lean:6:2: error: 'leanOptions' is not a field of structure 'Lake.PackageConfig'
error: ./.lake/packages/mathlib/lakefile.lean: package configuration has errors
boltonbailey@eduroamprvnat-172-16-41-159 FormalSnarksProject % lake update -R
error: ./.lake/packages/mathlib/lakefile.lean:6:2: error: 'leanOptions' is not a field of structure 'Lake.PackageConfig'
error: ./.lake/packages/mathlib/lakefile.lean: package configuration has errors
boltonbailey@eduroamprvnat-172-16-41-159 FormalSnarksProject %
Utensil Song (Dec 03 2023 at 08:33):
Seems to be still having incompatible lake versions, possibly related to lean4#2858
Utensil Song (Dec 03 2023 at 08:35):
I'm on my phone and can't debug or properly search for now, but removing .lake and start from scratch is safe.
Utensil Song (Dec 03 2023 at 08:37):
And maybe try to update to lean 4.4.0-rc1 as Mathlib master is using it already
Utensil Song (Dec 03 2023 at 08:40):
Bolton Bailey said:
Screenshot-2023-12-03-at-2.20.51-AM.png
Why are there two mathlibs?
The 2nd mathlib looks like a manual copy by accident, removing it should also help. As it's redundant and would be kept incompatible hower you update with command line
Mario Carneiro (Dec 03 2023 at 09:43):
I also hit this issue in mathport. @Mac Malone This seems to be a drawback of moving the lean-toolchain
copy into lake update
: When the lakefile syntax changes, old lake can't process the new lakefile in the updated dependency, so it can't run the update script that says to copy the lean-toolchain
and try again
Mario Carneiro (Dec 03 2023 at 09:44):
This is going to hit every project that depends on mathlib and uses lake update
Mario Carneiro (Dec 03 2023 at 09:46):
and it will happen again every time mathlib's lakefile uses a new lake feature
Mario Carneiro (Dec 03 2023 at 09:53):
The options for mitigating this on mathlib's side seem very limited. In lake, one way to address this would be to show an additional error message if there is a problem processing the lakefile of a dependency and the lean-toolchain
s don't match, suggesting either a direct cp
invocation or some new lake
option like lake update --toolchain
which copies the toolchain of failing dependencies.
Also, the require mathlib
could have a trackToolchain := true
option which would allow you to know to do this in advance of processing the dependency's lakefile. This seems like a better long-term solution.
Mario Carneiro (Dec 03 2023 at 09:59):
To people stumbling on this issue: If you get an error like this:
$ lake update
mathlib: updating repository './.lake/packages/mathlib' to revision 'b1cd52acffa53bca04a33ddc14a40b2a62ed4308'
error: ./.lake/packages/mathlib/lakefile.lean:6:2: error: 'leanOptions' is not a field of structure 'Lake.PackageConfig'
error: ./.lake/packages/mathlib/lakefile.lean: package configuration has errors
the fix is
cp .lake/packages/mathlib/lean-toolchain .
lake update -R
Patrick Massot (Dec 04 2023 at 15:06):
Except of course it could be cp lake-packages/mathlib/lean-toolchain .
depending on how much your project is synchronized with random lake changes.
Shreyas Srinivas (Dec 04 2023 at 15:21):
One weird trick that worked for me twice last week is to use lake update
twice.
Patrick Massot (Dec 04 2023 at 15:22):
Only twice? You are really lucky!
Shreyas Srinivas (Dec 04 2023 at 15:28):
Mario Carneiro said:
.
Also, therequire mathlib
could have atrackToolchain := true
option which would allow you to know to do this in advance of processing the dependency's lakefile. This seems like a better long-term solution.
Isn't this toolchain matching requirement coming from cache? We don't have to match toolchains with Std or Qq. Only mathlib. Will this change as cache is generalised? NVM: just learnt that this is a lake versioning issue.
Shreyas Srinivas (Dec 04 2023 at 15:31):
Would it help if elan managed lake installations separately like rustup does with cargo, and lake warns you that the next version of <insert package> requires you to update lake through elan first?
Shreyas Srinivas (Dec 04 2023 at 15:32):
Or does lake remove support for old syntax and make it impossible to compile older Lakefiles from newer versions?
Mac Malone (Dec 04 2023 at 18:03):
Shreyas Srinivas said:
Or does lake remove support for old syntax and make it impossible to compile older Lakefiles from newer versions?
Eventually, yes, deprecated syntax is removed. But the aim is for each stable release to be backwards compatible with at least the prior stable.
Mac Malone (Dec 04 2023 at 18:06):
Notably, the fact that a package in general is neither necessarily forward- or backwards-compatible with other Lean toolchains is what makes an principled, automated solution to lean4#2582 complex.
Shreyas Srinivas (Dec 04 2023 at 18:19):
Then maybe a stepped update could be applied in the suggestion I describe above?
Mario Carneiro (Dec 08 2023 at 09:09):
Shreyas Srinivas said:
One weird trick that worked for me twice last week is to use
lake update
twice.
I recently confirmed with @Mac Malone that there is indeed a second bug and lake update
may not work after the toolchain copy, and using lake update
twice in a row will sometimes work but lake update -R
seems to be the most reliable way to fix this. I have updated the instructions above.
Mario Carneiro (Feb 02 2024 at 14:00):
This issue is back again for the 4.6.0 release, because we still haven't fixed the issue of lakefile additions being breaking changes.
Mario Carneiro (Feb 02 2024 at 14:01):
To people stumbling on this issue: If you get an error like this:
$ lake update
error: ./.lake/packages/proofwidgets/lakefile.lean:6:2: error: 'buildArchive' is not a field of structure 'Lake.PackageConfig'
error: ./.lake/packages/proofwidgets/lakefile.lean: package configuration has errors
the fix is
cp .lake/packages/mathlib/lean-toolchain .
lake update -R
Mac Malone (Feb 02 2024 at 19:21):
@Mario Carneiro Oops! I forgot that this was a problem (moe specifically, I forgot the problem was adding options -- I misremebered and thought it was only removing). Looking, the old field name still exists. So ProofWdigets can change to use buildArchive?
rather than buildArchive
to be backwards-compatible.
Michael Stoll (Feb 03 2024 at 10:36):
I still get an error on proofwidgets
:
~/lean4/EulerProducts> cp .lake/packages/mathlib/lean-toolchain .
~/lean4/EulerProducts> lake update -R
mathlib: updating repository './.lake/packages/mathlib' to revision '4d359a9bdcc3dabec793c88ec4b342a1b13b465b'
std: updating repository './.lake/packages/std' to revision '276953b13323ca151939eafaaec9129bf7970306'
aesop: updating repository './.lake/packages/aesop' to revision '6beed82dcfbb7731d173cd517675df27d62ad0f4'
proofwidgets: updating repository './.lake/packages/proofwidgets' to revision 'af1e86cf7a37389632a02f4a111e6b501b2b818f'
error: ./.lake/packages/proofwidgets/lakefile.lean:6:2: error: 'buildArchive' is not a field of structure 'Lake.PackageConfig'
error: ./.lake/packages/proofwidgets/lakefile.lean: package configuration has errors
Mario Carneiro (Feb 03 2024 at 10:45):
you have to run that after running it the normal way and getting the error
Mario Carneiro (Feb 03 2024 at 10:46):
or else do it twice in a row
Mario Carneiro (Feb 03 2024 at 10:46):
because the cp
line doesn't work until after the mathlib: updating repository
line
Kevin Buzzard (Feb 03 2024 at 10:50):
I had extra fun doing this yesterday because I upgraded a several-months-old project yesterday and things were still being put into lake-packages
:-) Fortunately my minimal understanding of what was going on, plus this thread, got me through (and indeed I needed to do something twice)
Michael Stoll (Feb 03 2024 at 13:27):
Mario Carneiro said:
you have to run that after running it the normal way and getting the error
I did that after the update via VSCode had failed, but maybe that attempt did not get the new toolchain file into the mathlib directory. Doing it again seems to be working.
Kim Morrison (Feb 08 2024 at 22:39):
Okay, this problem should go away after #10364 lands.
Last updated: May 02 2025 at 03:31 UTC