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-toolchains 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, 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.

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