Invalid lake configuration

Stream: lean4

[Bolton Bailey]

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]

Which seems the same as what I get from lake new test math. What is going on?

[Bolton Bailey]

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]

Screenshot-2023-12-03-at-2.20.51-AM.png
Why are there two mathlibs?

[Bolton Bailey]

Is it safe to just delete the .lean folder and start again?

[Utensil Song]

If you were running lake build, you'll need to run lake -R build, the same applies to other commands

[Bolton Bailey]

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]

Seems to be still having incompatible lake versions, possibly related to lean4#2858

[Utensil Song]

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]

And maybe try to update to lean 4.4.0-rc1 as Mathlib master is using it already

[Utensil Song]

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]

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]

This is going to hit every project that depends on mathlib and uses lake update

[Mario Carneiro]

and it will happen again every time mathlib's lakefile uses a new lake feature

[Mario Carneiro]

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]

---

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]

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]

One weird trick that worked for me twice last week is to use lake update twice.

[Patrick Massot]

Only twice? You are really lucky!

[Shreyas Srinivas]

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]

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]

Or does lake remove support for old syntax and make it impossible to compile older Lakefiles from newer versions?

[Mac Malone]

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]

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]

Then maybe a stepped update could be applied in the suggestion I describe above?

[Mario Carneiro]

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.