Create new Lean mathlib4 project with leanblueprint support

Stream: general

[Dimitar Jetchev]

I am relatively new to both of these topics but I tried to create a new Lean project with mathlib4 support and leanblueprint configured. After a brief discussion with @Kevin Buzzard and following the instructions here, I managed to install leanblueprint (in a designated python virtual environment) and managed to configure my blueprint by running leanblueprint new. I wrote some sample LaTeX and built the web and pdf for it with leanblueprint {web,pdf}. However, checking the declarations (running leanblueprint checkdeclsomehow failed with the following error messages below. I haven't changed/added any Lean code yet in the new repository (created with the very basic VSCode quickstart here). It is likely me missing some basic steps but would appreciate if anyone has an idea of how to troubleshoot this. @Kevin Buzzard @Patrick Massot

Run ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
  ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
  shell: /usr/bin/bash -e {0}
[?/?] Computing build jobs
[1/3] Building Main
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/packages/checkdecls/.lake/build/lib:././.lake/packages/CMark/.lake/build/lib:././.lake/packages/UnicodeBasic/.lake/build/lib:././.lake/packages/leanInk/.lake/build/lib:././.lake/packages/doc-gen4/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH=././.lake/packages/checkdecls/.lake/build/lib /home/runner/.elan/toolchains/leanprover--lean4---v4.8.0-rc1/bin/lean ././.lake/packages/checkdecls/././Main.lean -R ././.lake/packages/checkdecls/./. -o ././.lake/packages/checkdecls/.lake/build/lib/Main.olean -i ././.lake/packages/checkdecls/.lake/build/lib/Main.ilean -c ././.lake/packages/checkdecls/.lake/build/ir/Main.c --json
error: ././.lake/packages/checkdecls/././Main.lean:13:36-13:48: too many explicit universe levels for 'Lake.LakeOptions.mkLoadConfig'
error: ././.lake/packages/checkdecls/././Main.lean:14:11-14:73: failed to synthesize instance
  ToString Empty
error: ././.lake/packages/checkdecls/././Main.lean:15:17-15:89: invalid field 'root', the environment does not contain 'Lake.EResult.root'
  ws
has type
  EResult Nat Log Workspace
error: ././.lake/packages/checkdecls/././Main.lean:14:60-14:72: invalid dotted identifier notation, unknown identifier `Lake.Log.eio` from expected type
  Log
error: Lean exited with code 1
[2/3] Compiling Main
[3/3] Linking checkdecls
Some build steps logged failures:
- Building Main
error: build failed
Error: Process completed with exit code 1.

[Adrian Wüthrich]

I am having the exact same issue (also in a python venv).

[Patrick Massot]

This is probably a Lean version mismatch between the Lean library checkdecls and your project.

[Patrick Massot]

I confirm this is the issue. I’ll fix this very soon.

[Adrian Wüthrich]

Indeed, I have version 4.8.0-rc1 and chechdecls is on v4.6.0-rc1

[Patrick Massot]

This wouldn’t be a problem usually but the latest Lean version changed a lot of things in lake.

[Dimitar Jetchev]

Patrick Massot said:

This wouldn’t be a problem usually but the latest Lean version changed a lot of things in lake.

Sorry for the naive question but how do I compare the checkdecls versions on my system? lake --versionshowed me Lean version 4.8.0-rc1

[Patrick Massot]

And it seems the major change did not include anything like a migration guide so I guess I will need to ask @Mac Malone for help. Mac, how would you fix https://github.com/PatrickMassot/checkdecls/blob/master/Main.lean? to work with lean4.8.0?

[Patrick Massot]

Dimitar, the Lean version used by each project is recorded into a lean-toolchain file in the root folder of the project. So you can take a look at your project and then look inside the .lake folder to look at the versions used by the various Lean libraries you depend on.

[Patrick Massot]

Mac, the error messages are

invalid dotted identifier notation, unknown identifier `Lake.Log.eio` from expected type
  Log

and

invalid field 'root', the environment does not contain 'Lake.EResult.root'
  ws
has type
  EResult Nat Log Workspace

[Dimitar Jetchev]

Patrick Massot said:

Dimitar, the Lean version used by each project is recorded into a lean-toolchain file in the root folder of the project. So you can take a look at your project and then look inside the .lake folder to look at the versions used by the various Lean libraries you depend on.

Thanks, @Patrick Massot ! Looks like checkdecls is lean4:v4.6.0-rc1.

[Patrick Massot]

Yes, it is at this version for everybody. The whole library is a 16 lines long file that never needed to be updated before today.

[Dimitar Jetchev]

Thanks a lot, @Patrick Massot and @Mac Malone for your help! I assume you'll keep us updated when the issue gets fixed.

[Mac Malone]

@Patrick Massot I made a PR with the addaption.

[Patrick Massot]

Thanks a lot!

[Patrick Massot]

@Dimitar Jetchev and @Adrian Wüthrich, could you please try to run lake update checkdecls in your project and see whether it fixes your issue?

[Dimitar Jetchev]

Patrick Massot said:

Dimitar Jetchev and Adrian Wüthrich, could you please try to run lake update checkdecls in your project and see whether it fixes your issue?

@Patrick Massot @Mac Malone looks like this fixed the issue. leanblueprint all ran successfully for my repository. Thanks a lot for your quick fix!

[Patrick Massot]

@Mac Malone How do you suggest I handle this now? I have my library at https://github.com/PatrickMassot/checkdecls that has tags lean4.6.0, lean4.7.0 and lean4.8.0-rc1. Right now I hope that people who use it with an older Lean version will not update the checkdecls lib and will be fine. And people creating brand new projects will also be fine. And then people who have old project that update to the new Lean will need to run a lake update checkdecls and then should be fine. But really the ideal situation would be that when a project changes its main toolchain to 4.8.0-rc1 or above then lake somehow checks whether checkdecls has a corresponding tag and proposes to update it. How do you see this working in the future?

[Dimitar Jetchev]

@Patrick Massot I now have another issue - I get the following error: what could that mean?

Run ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
  ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
  shell: /usr/bin/bash -e {0}

[?/?] Computing build jobs
[1/3] Building Main
[2/3] Compiling Main
[3/3] Linking checkdecls
cyclotomic_units_index is missing
Error: Process completed with exit code 1.

[Dimitar Jetchev]

cyclotomic units is the number of my project

[Patrick Massot]

It says your blueprint refers to a declaration named cyclotomic_units_index that cannot be found in your Lean project. This is exactly what this lib is meant to do. The first thing to check is there is no spelling issue. Then check that your library main file indeed imports the file containing this declaration.

[Dimitar Jetchev]

Patrick Massot said:

It says your blueprint refers to a declaration named cyclotomic_units_index that cannot be found in your Lean project. This is exactly what this lib is meant to do. The first thing to check is there is no spelling issue. Then check that your library main file indeed imports the file containing this declaration.

Thanks, I managed to fix it - it was my fault! All is good new.

[Mac Malone]

@Patrick Massot The plan is to have package version with know toolchain versions and use that information to deduce what is the latest version one can update to on a given toolchain.

[Patrick Massot]

But this is all future work, right? Do you confirm there is nothing I can do at this point?

[Mac Malone]

@Patrick Massot Correct. If a repository does have such a tagging scheme, downstream packages could require a package on the tag matched on their Lean version (see this example) to avoid mismatched lake update, but there is no built-in Lake solution yet.

[Adrian Wüthrich]

Patrick Massot schrieb:

Dimitar Jetchev and Adrian Wüthrich, could you please try to run lake update checkdecls in your project and see whether it fixes your issue?

Yes that fixed the issue. Thanks a lot!

[Kevin Buzzard]

Just recording here that I needed lake update -R -Kenv=dev checkdecls and that lake update checkdecls for some reason uninstalled a bunch of other packages without warning (see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/checkdecl.20update.20surprise/near/437300239)

[Kim Morrison]

@Patrick Massot, we know this is a really big deal for the downstream ecosystem, and it's a priority! Thanks for holding our feet to the fire on this one. :-)