lake build all

Stream: lean4

[Martin Dvořák]

I want to be able to write lake build and have my entire project checked.
In the past, was using the following configuration:
https://github.com/madvorak/lean-mam/blob/main/lakefile.lean

The new version of Lake gives me impression that globs := #[.submodules `myroot] doesn't work anymore (I may be wrong).
What can I use instead?
Basically I want the @[default_target] to be all Lean files.

[Anand Rao Tadipatri]

@Martin Dvořák On another thread, I have written a short Lake script called mkImports to automatically generate a top-level file that imports all the files in your Lean library. One possible solution is to add the script to your lakefile and run lake run mkImports && lake build next time. If your library is set as a default target, this will have the effect of checking all the files in your repository.

[Martin Dvořák]

Thanks a lot for your effort! However, I find it hard to believe that we would have to do something so complicated in order to do what leanproject build would do in Lean 3.

[Patrick Massot]

lake and leanproject have very different goals.

[Sebastian Ullrich]

I don't think any breakage in globs was intended if something changed there

[Martin Dvořák]

Maybe I'm doing it wrong.
Is there any documentation for the .submodules thing?

[Kevin Buzzard]

If it's any help, this lakefile seems to be working for that project (it uses .andSubmodules)

[Martin Dvořák]

Can @Adam Topaz comment on this commit please?
https://github.com/adamtopaz/CopenhagenMasterclass2023/commit/42af8aab39152b97b746623701ce9166bb060fef

Does the existence of the Basic.lean file (albeit empty) influence whether .addSubmodules work?

[Adam Topaz]

I learned this trick from @Alex J. Best

[Martin Dvořák]

Can you teach me the trick, senpai?

[Adam Topaz]

I think the answer is essentially yes. The gist seems to have some file Foo.lean and some folder Foo in the top-level directory of the lake project. The lean file seems to be needed for lake to compile the stuff in the Foo folder.

[Adam Topaz]

Oh actualy, Foo/Basic.lean is not needed (I think)

[Adam Topaz]

I think I only added Basic.lean so that the folder CompHaus was properly handled by git.

[Martin Dvořák]

Back then (leanprover/lean4:nightly-2023-03-07) I didn't have to perform such a hack, but I will try it now.

[Adam Topaz]

of course you can just alternatively add lean_libs to your lakefile.

[Martin Dvořák]

I want one lean_lib that will force lake to compile everything.

[Adam Topaz]

and you don't want to put everything in a single folder?

[Martin Dvořák]

I am not sure about it, but I have everything in a single folder now.

[Martin Dvořák]

Do both .submodules and .andSubmodules take the entire directory recursively (i.e., files on all levels will be compiled)?

[Adam Topaz]

I really don’t know.

[Martin Dvořák]

If I have everything in the same directory (but on multiple levels), which of .submodules or .andSubmodules should I use?

[Martin Dvořák]

Whatever I try, I obtain weird errors:

$ lake build
error: no such file or directory (error code: 2)
  file: .\.\.\Grammars\Classes.lean

Note that I have a directory Grammars inside which I have a directory Classes but no file named Classes.lean in either of them.
Is Lake suggesting that I should create an empty Lean file alongside with every directory?!

[Martin Dvořák]

If I create the "missing" file Grammars\Classes.lean it just moves one level deeper and complains again:

$ lake build
error: no such file or directory (error code: 2)
  file: .\.\.\Grammars\Classes\ContextFree.lean

As with the previous error, I have a directory ContextFree inside the directory Classes but no file ContextFree.lean and I don't know why such a file should exist.

[Mario Carneiro]

that sounds like a bug, could you minimize?

[Martin Dvořák]

I was also wondering "bug or feature?", but I concluded I would need to see a specification of what submodules and andSubmodules are supposed to do. I will try to minimize it tomorrow. In the meanwhile, if you know the intended behavior, let me know please.

[Mario Carneiro]

andSubmodules builds the specified module and all submodules, submodules only builds the submodules

[Mario Carneiro]

obviously it shouldn't attempt to build things that don't exist, except possibly in the andSubmodules case

[Mac Malone]

Martin Dvořák said:

Is Lake suggesting that I should create an empty Lean file alongside with every directory?!

Actually, yes. It is assuming a directory has a corresponding Lean file (as this is the official Lean 4 style). However, I also consider this a bug as it should verify that rather than assuming so. Will push a fix soon.

[Mac Malone]

Upon further reflection, one caveat is that, even with this check, if you do not have a Foo/Bar.lean file for every directory Foo/Bar, the behavior of import Foo.Bar is not well defined.

[Mac Malone]

@Mario Carneiro since you helped designed this feature, what behavior do think should be expected on import Foo.Bar if Foo/Bar.lean does not exist. The way globs are designed it still has to be part of the library (since that check does not have FS data available), but with the fix I am working on, :Lake can at least not attempt to compile the file on the library build.

[Mario Carneiro]

import Foo.Bar should error if Foo/Bar.lean does not exist, but submodules should not attempt to compile files that do not exist (unless they are dependencies of files that do exist)

[Mario Carneiro]

andSubmodules should only error if the module directly referenced does not exist

[Mario Carneiro]

in other words, submodules adds as "roots" all lean files which are in subdirectories of the specified module, if they exist, and andSubmodules does that as well as adding the module itself (whether it exists or not).

[Mac Malone]

That sounds good to me. :thumbs_up:

[Mario Carneiro]

Mac said:

It is assuming a directory has a corresponding Lean file (as this is the official Lean 4 style).

Mathlib significantly deviates from this, and generally avoids "default" files (now "files-named-the-same-as-a-directory") except in certain deliberately curated cases, and Mathlib.lean

[Mario Carneiro]

Std too for that matter

[Mac Malone]

Anyway, I think we have moved onto a different tangent. Have we sorted out the original point of disagreement?

[Mario Carneiro]

don't assume default.lean files exist

[Mac Malone]

Already fixed that: f6f9503.

[Notification Bot]

211 messages were moved here from #lean4 > lake build all by Martin Dvořák.

[Notification Bot]

4 messages were moved here from #lean4 > official style? by Martin Dvořák.

[Martin Dvořák]

I noticed a comment:

also tests the issue reported on this Zulip thread:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/lake.20build.20all/near/370788618

Does it mean I should create a MWE that fails with the old Lake version and then test it succeeds with the new Lake version?

[Mac Malone]

Sure, if you want to. The issue is hopefully fixed.

[Martin Dvořák]

Easier for me: I just test my (not minimal) code with the new Lake version.

How do I get the newest version? Has it become a part of the last nightly?

[Mac Malone]

Sadly, I think the lean4 Lake update was too late for that. However, it should be in the next nightly (i.e., the one for 06-31 I believe).

[Martin Dvořák]

Nevermind. I will try tomorrow!

[Mac Malone]

If you want to make sure that fix did fix it before then, you could also just clone Lake, build it (via lake build) and run the resulting executable (lake/build/bin/lake) on your project. However, I am not sure that is worth the effort.

[Martin Dvořák]

I am lazy. I'll rather wait for the next nightly.

[Mac Malone]

In this case, I think waiting is just a prudent use of time. :smile:

[Yaël Dillies]

Mac said:

Sadly, I think the lean4 Lake update was too late for that. However, it should be in the next nightly (i.e., the one for 06-31 I believe).

The 31st of June? :grinning:

[Mac Malone]

Oops! :rofl: 07-01.

[Martin Dvořák]

I wanted to try whether it works now but I didn't succeed.

I changed lean-toolchain to leanprover/lean4:nightly-2023-07-01.
I ran lake update, lake clean, lake exe cache get, and lake build.
The last one gave me some weird errors:

[236/3523] Building Std.Tactic.Congr
[237/3523] Building Std.Classes.LawfulMonad
[237/3523] Building Std.Data.PairingHeap
[237/3523] Building Std.Data.Nat.Lemmas
[237/3523] Building Std.Data.RBMap.Basic
[239/3523] Building Std.Data.Option.Basic
[239/3523] Building Std.Data.Array.Init.Lemmas
[241/3523] Building Mathlib.Init.Data.Option.Basic
[241/3523] Building Std.Data.Option.Lemmas
error: > LEAN_PATH=.\lake-packages\proofwidgets\build\lib;.\build\lib;.\lake-packages\mathlib\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\std\build\lib PATH c:\Users\mdvorak\.elan\toolchains\leanprover--lean4---nightly-2023-07-01\bin\lean.exe -Dlinter.missingDocs=true -DwarningAsError=true .\lake-packages\std\.\.\Std\Data\Array\Init\Lemmas.lean -R .\lake-packages\std\.\. -o .\lake-packages\std\build\lib\Std\Data\Array\Init\Lemmas.olean -i .\lake-packages\std\build\lib\Std\Data\Array\Init\Lemmas.ilean -c .\lake-packages\std\build\ir\Std\Data\Array\Init\Lemmas.c
error: stdout:
.\lake-packages\std\.\.\Std\Data\Array\Init\Lemmas.lean:153:31: error: invalid constructor ⟨...⟩, expected type must be an inductive type
  ?m.51990
.\lake-packages\std\.\.\Std\Data\Array\Init\Lemmas.lean:174:2: error: tactic 'apply' failed, failed to unify
  (foldl (fun bs a => push bs (f a)) #[] arr 0 (size arr)).data = ?m.54080
with
  (map f arr).data = List.map f arr.data
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
⊢ (map f arr).data = List.map f arr.data
error: external command `c:\Users\mdvorak\.elan\toolchains\leanprover--lean4---nightly-2023-07-01\bin\lean.exe` exited with code 1
[242/3523] Building Std.Data.String.Basic
[242/3523] Building Std.Data.Array.Merge
[242/3523] Building Std.Data.Nat.Gcd
[242/3523] Building Std.Data.BinomialHeap
[244/3523] Building Std.Data.RBMap.WF
[244/3523] Building Std.Data.Int.Lemmas
[246/3523] Building Mathlib.Init.Data.Option.Lemmas
[247/3523] Building Qq
[249/3523] Building Mathlib.Util.Qq
[251/3523] Building Std.Lean.Meta.DiscrTree
[256/3523] Building Mathlib.Init.Data.Int.Lemmas
[256/3523] Building Std.Data.Int.DivMod
[258/3523] Building Std.Data.RBMap
[258/3523] Building Std.Data.RBMap.Alter
[260/3523] Building Mathlib.Init.Data.Int.DivMod
[260/3523] Building Std.Data.Rat.Basic
[262/3523] Building Mathlib.Init.Data.Rat.Basic
[262/3523] Building Std.Classes.RatCast
[262/3523] Building Std.Data.Rat.Lemmas
error: > LEAN_PATH=.\lake-packages\proofwidgets\build\lib;.\build\lib;.\lake-packages\mathlib\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\std\build\lib PATH c:\Users\mdvorak\.elan\toolchains\leanprover--lean4---nightly-2023-07-01\bin\lean.exe -Dlinter.missingDocs=true -DwarningAsError=true .\lake-packages\std\.\.\Std\Data\Rat\Lemmas.lean -R .\lake-packages\std\.\. -o .\lake-packages\std\build\lib\Std\Data\Rat\Lemmas.olean -i .\lake-packages\std\build\lib\Std\Data\Rat\Lemmas.ilean -c .\lake-packages\std\build\ir\Std\Data\Rat\Lemmas.c
error: stdout:
.\lake-packages\std\.\.\Std\Data\Rat\Lemmas.lean:260:60: error: unsolved goals
a : Rat
⊢ 0.num * a.num = 0
.\lake-packages\std\.\.\Std\Data\Rat\Lemmas.lean:261:60: error: unsolved goals
a : Rat
⊢ a.num * 0.num = 0
.\lake-packages\std\.\.\Std\Data\Rat\Lemmas.lean:262:59: error: unsolved goals
a : Rat
⊢ normalize (1.num * a.num) (1.den * a.den) = a
.\lake-packages\std\.\.\Std\Data\Rat\Lemmas.lean:263:59: error: unsolved goals
a : Rat
⊢ normalize (a.num * 1.num) (a.den * 1.den) = a
error: external command `c:\Users\mdvorak\.elan\toolchains\leanprover--lean4---nightly-2023-07-01\bin\lean.exe` exited with code 1

Can these errors be caused by a mistake in my code?
I don't know where to search for problems.

[Sebastian Ullrich]

std4 doesn't seem to be compatible with that version of Lean yet

[Sebastian Ullrich]

In general, you should always use exactly the same Lean version as mathlib4, as documented at https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4

[Martin Dvořák]

PS: I get the same error when I run lake new asdf math, update lean-toolchain to leanprover/lean4:nightly-2023-07-01, put import Mathlib on the first line of Asdf.lean, and proceed the usual way.

I see now that the error was not caused by a mistake in my code.

[Martin Dvořák]

Sebastian Ullrich said:

In general, you should always use exactly the same Lean version as mathlib4,

Thanks for your answer!!

Is there anything I can do in order to test the new version of Lake and have Std4 (not necessarily the newest version) available in the project at the same time?

[Sebastian Ullrich]

You can build Lake separately as Mac suggested above. It only takes a few minutes to set up.

[Sebastian Ullrich]

There should be a way to use Lake from one toolchain with Lean from another toolchain, but I would have to try that myself first

[Martin Dvořák]

I am scared of doing these things.

[Martin Dvořák]

Mac said:

Already fixed that: f6f9503.

How long do you think we will have to wait for [Mathlib4 uses Lake that has your bugfix] ?

[Mac Malone]

@Martin Dvořák If you want to test a newer Lake with a different lean (i.e., mathlib's) you can do the following:

lake +leanprover/lean4:nightly-2023-07-01 --lean="~/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/lean" build

[Martin Dvořák]

Is it safe? Will my Lean installation stay unchanged for other projects?

[Martin Dvořák]

What should I have in lean-toolchain when running your command?
Can I do lake update, lake clean, and lake exe cache get before running the command?

[Mac Malone]

@Martin Dvořák Yes, it has no side-effects (except potentially downloaded the toolchain of the new Lake if you do not already have it).

[Martin Dvořák]

I think I already have it.

[Martin Dvořák]

If your command succeeds (i.e., my project builds in Git Bash), will it fail in VS Code afterwards?

[Mac Malone]

Martin Dvořák said:

What should I have in lean-toolchain when running your command?

Does not matter for the command. However, you should always keep the lean-toolchain of a mathlib dependent project set to mathlib's toolchain version (i.e., right now 06-20).

Martin Dvořák said:

Can I do lake update, lake clean, and lake exe cache get before running the command?

Yep and just like that (using the toolchain version lake + lean).

[Mac Malone]

Martin Dvořák said:

If your command succeeds (i.e., my project builds in Git Bash), will it fail in VS Code afterwards?

Yes, it will fail. This just tests whether this single command works. To fix it in VSCode, you would have to change your project preferences. That is, manually set your VSCode toolchainpath to that of the 07-01 nightly and add --lean="~/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/lean" to your server args.

[Martin Dvořák]

To recapitulate, I will change lean-toolchain to leanprover/lean4:nightly-2023-06-20 and then run the following commands (while in the directory of the project, i.e., where lean-toolchain is located) in the following order:

lake update
lake clean
lake exe cache get
lake +leanprover/lean4:nightly-2023-07-01 --lean="~/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/lean" build

Is it safe to do it this way?
Edit: lake exe cache get

[Mac Malone]

Yes. :thumbs_up:

[Mac Malone]

Also, it should be lake exe cache get. Right?

[Mac Malone]

@Martin Dvořák Also, you are on a Linux machine, correct?

[Martin Dvořák]

Windows 10 machine with Git GUI.

[Martin Dvořák]

*Git Bash

[Mac Malone]

Okay, since you are using Git Bash, ~/.elan should still be the correct path to the elan installation.

[Mac Malone]

You could verify by checking if ~/.elan exists (e.g., via ls ~/.elan -- if it does not error, you are good).

[Martin Dvořák]

Thank you very much! I will return to my office in the evening and try it out.

[Martin Dvořák]

mdvorak@wngrad258 MINGW64 ~/Documents/chomsky (master)
$ ls ~/.elan
bin/  settings.toml  tmp/  toolchains/  update-hashes/

mdvorak@wngrad258 MINGW64 ~/Documents/chomsky (master)
$ cat lean-toolchain
leanprover/lean4:nightly-2023-06-20

mdvorak@wngrad258 MINGW64 ~/Documents/chomsky (master)
$ lake update

mdvorak@wngrad258 MINGW64 ~/Documents/chomsky (master)
$ lake clean

mdvorak@wngrad258 MINGW64 ~/Documents/chomsky (master)
$ lake exe cache get
info: Downloading proofwidgets/v0.0.11/windows-64.tar.gz
info: Unpacking proofwidgets/v0.0.11/windows-64.tar.gz
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [6/9] Compiling Cache.Requests
info: [6/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache.exe
No files to download
Decompressing 3500 file(s)

mdvorak@wngrad258 MINGW64 ~/Documents/chomsky (master)
$ lake +leanprover/lean4:nightly-2023-07-01 --lean="~/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/lean" build
error: could not detect a Lean installation

What did I do wrong?

[Mac Malone]

@Martin Dvořák Interesting, that makes it appear as though the toolchain does not exist. Can you ls ~/.elan/toolchains/leanprover--lean4---nightly-2023-06-20?

[Mac Malone]

And if not, what does lean --print-prefix return?

[Mac Malone]

Oh, it also occurred to me that I am wrong, VSCode should not fail, because glob-based building only occurs during lake build.

[Mac Malone]

@Martin Dvořák My only other thought of what could have gone wrong here is that maybe it is the 07-01 nightly that is broken. If you want to check, what does ls ~/.elan/toolchains/leanprover--lean4---nightly-2023-07-01 produce?

[Martin Dvořák]

My previous post disappeared, so I will put both outputs here:

mdvorak@wngrad258 MINGW64 ~/Documents/chomsky (master)
$ ls ~/.elan/toolchains/leanprover--lean4---nightly-2023-06-20
LICENSE  LICENSES  bin/  include/  lib/  share/  src/

mdvorak@wngrad258 MINGW64 ~/Documents/chomsky (master)
$ ls ~/.elan/toolchains/leanprover--lean4---nightly-2023-07-01
LICENSE  LICENSES  bin/  include/  lib/  share/  src/

There doesn't seem to be a difference at this level tho.

Anyways, unless there is an easy solution to my problem, ignore it and I will just wait for mathlib4 to get a newer toolchain.

[Mac Malone]

Yeah, I think waiting is for the best. :thumbs_up:

[Martin Dvořák]

Having updated lean-toolchain to leanprover/lean4:nightly-2023-07-12 it works as it should. Thanks a lot for fixing Lake!