set up lean 4 project

Stream: general

[Thorsten Altenkirch]

I am trying to set up a lean4 project in one directory (while using lean 3 everywhere else). I have done

elan override set leanprover/lean4:stable
lake init lac

but how do I get the current version of mathlib? I say import tactic but it doesn't know it?

[Martin Dvořák]

Just 2 minutes ago I asked:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Lean.204.20first.20steps

[Alex J. Best]

You can add the line

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

in the lakefile.lean that lake init created for you, then run lake build

[Alex J. Best]

You can then import tactic with import Mathlib.Tactic.Basic, imports must be fully qualified in Lean 4, but the mathlib4 docs should be enough to tell you the names of what you need https://leanprover-community.github.io/mathlib4_docs

[Alex J. Best]

Finally I recommend using lake exec cache get to download precompiled mathlib oleans, and you should ensure that the lean-toolchain of your project matches the latest mathlib one to avoid problems.

[Alex J. Best]

You may wish to pin a specific mathlib version in the lakefile so that things don't break when mathlib moves

[Alex J. Best]

See https://github.com/leanprover/lake#syntax-of-require for how to do this

[Tomas Skrivan]

Instead of specifying exact revision in lakefile it is now done manifest.json which can be found in the directory lean_packages in your project directory.

[Alex J. Best]

I think lake-manifest.json is by default in the project root now? But that could indeed be the best practice these days

[Martin Dvořák]

Does lake fully replace the leanproject command?

[Alex J. Best]

For now yes as far as I'm aware, at least I've not needed anything leanproject for Lean 4 yet. Seeing as lake is extensible via lake exec some functionality that used to be left for leanproject rather than leanpkg before should now be implementable via a lake extension

[Matthew Ballard]

Lake also supports lake init foo math for a library only with a mathlib dependency.

[Patrick Massot]

lake is still very far away from being as convenient as leanproject unfortunately.

[Patrick Massot]

But there is no alternative.

[Patrick Massot]

See https://github.com/leanprover/lake/issues/150. Right now you cannot tell lake: "I want to create a new project depending on mathlib" and hope things will just work. There is nothing remotely analogous to leanproject new my_project that would get you the latest lean3+mathlib and the mathlib oleans.

[Sebastian Ullrich]

Realistically I think the best chance for that working out of the box is someone from the mathlib4 crowd stepping up and implementing it in Lake. It's such a surface-level that no deep knowledge of Lake should be necessary.

[Sebastian Ullrich]

Certainly I would hope that Lean people would find it easier than modifying a Python project!

[Matthew Ballard]

Forgive my ignorance but what does lake exe cache get do? I assumed it solve the oleans issue but didn't really follow.

[Thorsten Altenkirch]

Hang on, what is the relation between the file lake generates and my files? Do I just say lake init foo or maybe lake init foo math and put my proof files in the same directory?

[Matthew Ballard]

lake init foo or lake new foo generates a few files lean-toolchain lakefile.lean Foo.lean and perhaps Main.lean depending on use of the templates like math. A library author creates a folder Foo in the foo folder for the proof files (this is how std and mathlib are structured for example).

[Matthew Ballard]

Matthew Ballard said:

Forgive my ignorance but what does lake exe cache get do? I assumed it solve the oleans issue but didn't really follow.

Perhaps this only works for mathlib4?

[Thorsten Altenkirch]

I said elan override set leanprover/lean4:stable and I thought that would only apply locally but now it uses lean4 also for my lean3 files??? How do I avoid this?

[Sebastian Ullrich]

Yes, override only affects the current directory. Are they all in the same directory?

[Thorsten Altenkirch]

no I created a new directory

[Sebastian Ullrich]

Can you run elan show in the directory with the Lean 3 files?

[Thorsten Altenkirch]

installed toolchains
--------------------

stable (default)
leanprover-community/lean:3.48.0
leanprover/lean4:nightly
leanprover/lean4:stable

active toolchain
----------------

stable (default)
Lean (version 3.48.0, commit 283f6ed8083a, Release)

[Thorsten Altenkirch]

when I open with visual studio it says lean4

[Sebastian Ullrich]

In VS Code did you open the Lean 3 folder using File > Open Folder? I think it's easiest to use separate VS Code windows for each Lean version.

[Thorsten Altenkirch]

I tried this but it still uses lean4

[Thorsten Altenkirch]

Ok, I disabled lean4 in code now at least I can use my lean3 files.

[Alex J. Best]

Matthew Ballard said:

Matthew Ballard said:

Forgive my ignorance but what does lake exe cache get do? I assumed it solve the oleans issue but didn't really follow.

Perhaps this only works for mathlib4?

it only works for mathlib4 but is also very helpful for projects depending on mathlib4 also!

[Patrick Massot]

I wasn't able to use it in a project depending on mathlib4. lake kept rebuilding stuff after fetching cache. If you manage to do that then some documentation would be very nice.

[Alex J. Best]

I don't think I did anything special to get it to work, I'm using it in CI for a project depending on mathlib4, you can see the action at https://github.com/KisaraBlue/ec-tate-lean/blob/master/.github/workflows/build.yml and the lakefile in the root directory there. But I didn't have to do anything special. I'm quite sure it's working as intended as the CI runs only take 5 mins, which doesn't seem possible without the oleans. Lake will compile the executable code (but not oleans) for some files in mathlib 4, so you still see some output about compiling mathlib.blah but not building iirc

[Arthur Paulino]

If your project needs std4 and/or quote4, let mathlib4 require those for you as it pleases. I'm saying this because if you require the wrong version for those, cache will try to download files that have never been computed by mathlib4 workflow due to hash incompatibilities

[Patrick Massot]

In which folder do you run lake exe cache get? Maybe I did this wrong.

[Alex J. Best]

In the root folder of my project

[Patrick Massot]

Maybe I tried something too complicated and ran it in the lake-packages/mathlib folder.

[Arthur Paulino]

Yes, that will make cache think it's running from inside the mathlib4 repo itself and will put the olean files for std4 and quote4 in the wrong places

[Arthur Paulino]

Notice that Lake downloads std4 and quote4 to lake-packages. cache needs to know that you're not in mathlib4 itself so it can be aware that std4, quote4 and mathlib4 are in the same depth of your folder tree: they're all immediate children of lake-packages

[Patrick Massot]

Ok, I'm pretty sure I did the wrong thing here.

[Patrick Massot]

Since you understand lake, do you think you could work on preventing it to download doc-gen whenever someone one asks for mathlib?

[Arthur Paulino]

And if you did call lake exe cache get from lake-packages/mathlib, you should delete the lake-packages folder and let Lake download it again because it's full of useless/misplaced olean files

[Henrik Böving]

Patrick Massot said:

Since you understand lake, do you think you could work on preventing it to download doc-gen whenever someone one asks for mathlib?

I think that is an issue that has to be fixed from within lake, I am not sure we have people except mac who have good understanding of the lake implementation itself?

[Patrick Massot]

After trying that nothing worked so I nuked the whole lake-packages folder.

[Patrick Massot]

Henrik, don't get me wrong, I love doc-gen, but not in this place.

[Henrik Böving]

Oh I get that you don't want to download it all the time completely :D It annoys me as well.

[Sebastian Ullrich]

How big is the doc-gen source anyway compared to the big oleans downloaded from cache? Is the problem that the entire history of the repo is cloned?

[Henrik Böving]

The main issue is that it downloads Unicode.lean as a dependency which ships dozens of MB of raw unicode data.

[Arthur Paulino]

cache does not put/get doc-gen4 oleans

[Matthew Ballard]

I think I have been doing this wrong also. Would @Arthur Paulino or someone else give a bulleted list of instructions to create a new Lean 4 library with a dependency on mathlib its oleans. :pray:

[Arthur Paulino]

I will open a PR

[Arthur Paulino]

!4#1998

[Kevin Buzzard]

$ lake init MyProject math
error: toolchain 'stable' does not have the binary `/home/buzzard/.elan/toolchains/stable/bin/lake`

[Kevin Buzzard]

I'll just take this to github. Thanks a lot for the PR!

[Arthur Paulino]

That's because your default toolchain is pointing to an old version. What does elan toolchain list show for you?

[Kevin Buzzard]

buzzard@brutus:~/lean-projects$ elan toolchain list
stable (default)
leanprover-community/lean:3.35.1
leanprover-community/lean:3.44.1
leanprover-community/lean:3.45.0
leanprover-community/lean:3.48.0
leanprover-community/lean:3.49.0
leanprover-community/lean:3.49.1
leanprover-community/lean:3.5.1
leanprover-community/lean:3.50.2
leanprover-community/lean:3.50.3
leanprover/lean4:nightly
leanprover/lean4:nightly-2022-10-29
leanprover/lean4:nightly-2022-11-17
leanprover/lean4:nightly-2022-11-21
leanprover/lean4:nightly-2022-11-23
leanprover/lean4:nightly-2022-11-24
leanprover/lean4:nightly-2022-11-25
leanprover/lean4:nightly-2022-11-26
leanprover/lean4:nightly-2022-11-29
leanprover/lean4:nightly-2022-11-30
leanprover/lean4:nightly-2022-12-05
leanprover/lean4:nightly-2022-12-13
leanprover/lean4:nightly-2022-12-16
leanprover/lean4:nightly-2022-12-22
leanprover/lean4:nightly-2022-12-23
leanprover/lean4:nightly-2023-01-04
leanprover/lean4:nightly-2023-01-06
leanprover/lean4:nightly-2023-01-16
leanprover/lean4:nightly-2023-01-29
semorrison/lean4:fix-1907
buzzard@brutus:~/lean-projects$

I never think about toolchains, and my students don't either. Is this just an issue which will go away over time (e.g. when nobody's using Lean 3 any more?)

[Kevin Buzzard]

I don't even know if stable is lean 3 or lean 4!

[Arthur Paulino]

I am not sure what's the recommended way to proceed here. You already have many recent toolchains so, for you, calling elan default leanprover/lean4:nightly-2023-01-29 would do the trick. You would be able to call lake init MyProject math

[Arthur Paulino]

Okay, I've added a comment about that in the PR. The instructions recommend the users to set a more recent toolchain as default in order to be able to use the math option

[Mauricio Collares]

If you're not on Windows, you have the option of not using elan default by running elan run leanprover:lean4/nightly lake init MyProject math, which affects the current command only.

[Mauricio Collares]

Unfortunately I think elan rundoes not yet work on Windows, though, so it might be best to avoid it in general instructions

[Sebastian Ullrich]

Does lake +leanprover:lean4/nightly init MyProject math work on Windows?

[Arthur Paulino]

The PR was merged already so if someone feels confident with a better command, please open a new PR :pray:

[Eric Wieser]

Henrik Böving said:

The main issue is that it downloads Unicode.lean as a dependency which ships dozens of MB of raw unicode data.

What does it need this data for?

[Henrik Böving]

Mostly to know the name etc. of all the unicode code points afaik.

[Henrik Böving]

doc-gen4 uses it to render doc-strings to the best of its ability iirc.

[Kevin Buzzard]

Right, but a mathematician making a toy project with mathlib doesn't need doc-gen4.

[Henrik Böving]

Yeah I've never denied that, I've been in favor of not pulling doc-gen4 unless the doc feature is enabled in the entire time, it is merely a technical challenge with an issue in the lake issue tracker that needs to be implemented.

[Kevin Buzzard]

Got it. Sorry, I'm totally ignorant of all things lake! (and also all things doc-gen :-) )

[Eric Wieser]

Henrik Böving said:

Mostly to know the name etc. of all the unicode code points afaik.

Is this used at all?

[Eric Wieser]

Ah, it's used to generate header names here

[Eric Wieser]

I'd argue that if not downloading doc-gen4 at all is currently challenging in Lake, it would be better to have very slightly uglier heading links in doc-gen than to have every lean user download dozens of megabytes of unicode data

[Henrik Böving]

I'm not sure if its challenging, the issue is mostly that nobody is working on Lake right now because Mac is busy with other stuff.

[Eric Wieser]

Not all challenges are technical, it sounds like this is an availability challenge. To make my suggestion concrete: it's merge https://github.com/leanprover/doc-gen4/pull/112, and revert it once Mac or someone else has time to improve lake

[Reid Barton]

You could hard-code this list for now (I don't know what "other" means)

Prelude Data.Char> filter (\c -> isPunctuation c || isSeparator c) ['\32'..'\127']
" !\"#%&'()*,-./:;?@[\\]_{}"

[Eric Wieser]

For what it's worth, the rules for HTML ids are:

HTML 5 is even more permissive, saying only that an id must contain at least one character and may not contain any space characters.

So really just removing spaces is all that's necessary; the rest is cosmetic

[Eric Wieser]

And the place where the cosmetic choice matter is in the URL fragment, which is also only allowed to contain a hard-coded list of characters (the rest of which will be ugly %-escaped things)

[Arthur Paulino]

!4#2079 suggests a toolchain with a fix on Lake for the math template
(it's a trivial +2 −2 PR)

[Bolton Bailey]

Trying to read the instructions above but I'm afraid I missed a step: I ran lake init demo math in my empty demo directory and tried to start coding in Demo.lean, but got the error

`/Users/boltonbailey/.elan/toolchains/leanprover--lean4---stable/bin/lake print-paths Init` failed:

stderr:
Error parsing '././lakefile.lean'.  Please restart the lean server after fixing the Lake configuration file.

What did I do wrong here?

[Reid Barton]

Wild guess: somehow the version of lean/lake that made the lakefile is not the same as the one that is being used in the new project?

[Bolton Bailey]

boltonbailey@starlight demo % lake --version
Lake version 4.0.0 (Lean version 4.0.0, commit 7dbfaf9b751917a7fe020485bf57f41fdddcaafa)

[Bolton Bailey]

boltonbailey@starlight demo % lean --version
Lean (version 4.0.0, commit 7dbfaf9b7519, Release)

[Bolton Bailey]

How do I determine what version of lean is being used in the project?

[Shreyas Srinivas]

Bolton Bailey said:

boltonbailey@starlight demo % lake --version
Lake version 4.0.0 (Lean version 4.0.0, commit 7dbfaf9b751917a7fe020485bf57f41fdddcaafa)

`$ cat lean-toolchain `

[Bolton Bailey]

boltonbailey@starlight demo % cat lean-toolchain
cat: lean-toolchain: No such file or directory

[Shreyas Srinivas]

Bolton Bailey said:

boltonbailey@starlight demo % cat lean-toolchain
cat: lean-toolchain: No such file or directory

This is to get the lean toolchain used by lake in your project. So this works inside the project directory
If you want to find the lean toolchain that is your default (and therefore used to initialise projects),
$ elan toolchain list

[Shreyas Srinivas]

the version currently in use will be marked default

[Bolton Bailey]

boltonbailey@starlight demo % elan toolchain list
stable
leanprover-community/lean:3.30.0
leanprover-community/lean:3.44.1
leanprover-community/lean:3.45.0
leanprover-community/lean:3.46.0
leanprover-community/lean:3.48.0
leanprover-community/lean:3.50.3
leanprover/lean4:nightly
leanprover/lean4:nightly-2022-11-19
leanprover/lean4:nightly-2022-12-05
leanprover/lean4:nightly-2022-12-23
leanprover/lean4:stable (default)

[Bolton Bailey]

So this works inside the project directory

I ran this from the top-level of the project - lake did not create any lean-toolchain file in my directory.

[Shreyas Srinivas]

okay. Try the following and tell us if it works.

1. Leave the project directory
2. Run elan self update
3. Run elan default leanprover/lean4:nightly-2023-02-10
4. Run lake new <project_name> math
5. Run cd project_name/

[Shreyas Srinivas]

The first step is important

[Bolton Bailey]

boltonbailey@starlight mathlibcontribution % elan self update
error: self-update is disabled for this build of elan
error: you should probably use your system package manager to update elan

[Bolton Bailey]

Is this an M1 issue? I have a Mac M1.

[Kevin Buzzard]

Which version of elan do you have? Maybe you're up to date anyway

[Bolton Bailey]

boltonbailey@starlight mathlibcontribution % elan --version
elan 1.4.2 ( )

[Shreyas Srinivas]

This is fine. Skip to step 3

[Bolton Bailey]

boltonbailey@starlight mathlibcontribution % elan --version
elan 1.4.2 ( )
boltonbailey@starlight mathlibcontribution % lake new boltontest math
boltonbailey@starlight mathlibcontribution % cd boltontest
boltonbailey@starlight boltontest % ls
Boltontest.lean lakefile.lean
boltonbailey@starlight boltontest %

[Shreyas Srinivas]

run lake update inside the project folder

[Shreyas Srinivas]

wait, where is the lean-toolchain file

[Shreyas Srinivas]

Do you happen to have a lean-toolchain file inside the folder mathilbcontribution?

[Bolton Bailey]

Ok redoing it with step 2 produces the lean-toolchain file

[Bolton Bailey]

(I think you meant to say skip to step 2 above?)

[Shreyas Srinivas]

Nvm, cd into your project folder and run lake update.

[Shreyas Srinivas]

you should see mathlib being cloned. Is this happening?

[Bolton Bailey]

Yes

[Bolton Bailey]

boltonbailey@starlight boltontest % lake update
cloning https://github.com/leanprover-community/mathlib4.git to lake-packages/mathlib
cloning https://github.com/gebner/quote4 to ./lake-packages/Qq
cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop
cloning https://github.com/leanprover/std4 to ./lake-packages/std

[Bolton Bailey]

Let me try importing mathlib files now

[Shreyas Srinivas]

I would try lake exe cache first

[Shreyas Srinivas]

It should save you 20-30 minutes if it works

[Bolton Bailey]

Yeah it was taking a while

[Bolton Bailey]

Glorious, it works. Thank you @Shreyas Srinivas

[Shreyas Srinivas]

You're welcome :)

[Shreyas Srinivas]

@Arthur Paulino : This issue keeps coming up. People have some toolchain, but mathlib4 is using a different toolchain, and the build fails. Since we have a specific command just to start mathlib4 based projects, is it possible to change lake such that:

When lake new <project_name> math is called (with the math command in the end), lake changes the default toolchain to match the mathlib4 toolchain from the cloned mathlib4 repo, and calls the required elan commands?

[Arthur Paulino]

No, the default toolchain has to be chosen manually. What's happening is an old bug in the Lake math template. The solution is to set the default toolchain to a more recent one before doing lake init ... math so that command can run without the old bug

[Arthur Paulino]

Maybe it has to be better phrased in the mathlib4 readme because there I said the command first and then warned about the toolchain issue later. @Shreyas Srinivas do you want to improve those instructions?

[Shreyas Srinivas]

Sounds good. I can send a PR for this

[Arthur Paulino]

@Frédéric Dupuis Sorry I had to include another fix I just found in !4#2403

[Frédéric Dupuis]

No problem, I just reborsed it.