New Project that uses MathLib4

Stream: mathlib4

[Alcides Fonseca]

Using "leanprover/lean4:nightly-2021-12-01" and mathlib, I get this error:

./lean_packages/mathlib/././Mathlib/Data/Option/Defs.lean:54:18: error: unsolved goals
α : Type ?u.710
β : Type ?u.713
p : α → Prop
inst✝ : DecidablePred p
x✝ : Option α
⊢ α → True

which makes sense, because the project and the master don't use the same lean toolchain. (Master is using 2021-12-19 right now, and passes the tests). But when I change my project to use that toolchain, lake itself does not work (not build nor clean):

 alcides@Alcidess-MacBook-Pro  ~/Desktop/LeanGenetic   master  lake clean
./lakefile.lean:1:0: error: object file '/Users/alcides/.elan/toolchains/leanprover--lean4---nightly-2021-12-19/lib/lean/Lean/Data/Name.olean' of module Lean.Data.Name does not exist
./lakefile.lean:2:0: error: unknown namespace 'Lake'
./lakefile.lean:4:0: error: expected command
error: package configuration `./lakefile.lean` has errors

[Notification Bot]

Alcides Fonseca has marked this topic as unresolved.

[Sebastian Ullrich]

That's very odd, the file exists in the tarball

$ tar tf lean-4.0.0-nightly-2021-12-19-darwin.tar.zst | grep Data/Name.olean
lean-4.0.0-nightly-2021-12-19-darwin/lib/lean/Lean/Data/Name.olean

[Alcides Fonseca]

I went back to mathlib4 commit "559d1ea67b9ad3f18effcef642097ed0118a118c" with "leanprover/lean4:nightly-2021-12-08", and it works.

[Sebastian Ullrich]

Is the file in fact missing? Could you try removing and re-adding the toolchain?

[Alcides Fonseca]

it works by reinstaling the toolchain. I must have control+c'ed or lost internet during the instalation.

[Notification Bot]

Patrick Massot has marked this topic as unresolved.

[Patrick Massot]

It would be nice to have a reliable process to create a project that depends on mathlib4. The lake documentation says to run lake new <package-name> math but this does not work. In particular it creates a project whose lean-tool-chain is not the relevant one for mathlib.

[Patrick Massot]

And of course it doesn't include getting the cached oleans for mathlib.

[Mario Carneiro]

you should open an issue for that

[Patrick Massot]

Where?

[Mario Carneiro]

lake

[Patrick Massot]

Is there any hope to get a version of mathlib4 using a Lean4 that includes https://github.com/leanprover/lean4/commit/18297d8d918cc808c37c23ad497bca7f98dbe973 before Tuesday?

[Patrick Massot]

I need to give a short Lean demo on Tuesday and I was about to decide to show Lean 4 when I remembered this fix didn't reach mathlib yet.

[Patrick Massot]

I opened a lake issue.

[Mario Carneiro]

have you tried just bumping the lean-toolchain of your project depending on mathlib? I guess you won't get caches that way though

[Patrick Massot]

This is what I involuntarily tried when I tried to follow the lake README and nothing worked.

[Mario Carneiro]

what broke?

[Patrick Massot]

aesop didn't build and calc failed in mathlib.

[Patrick Massot]

Building Aesop.Tree.Check
error: > LEAN_PATH=./lake-packages/mathlib/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./build/lib:./lake-packages/std/build/lib LD_LIBRARY_PATH=/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2023-01-29/lib:./lake-packages/aesop/build/lib /home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2023-01-29/bin/lean ./lake-packages/aesop/././Aesop/Tree/ExtractProof.lean -R ./lake-packages/aesop/./. -o ./lake-packages/aesop/build/lib/Aesop/Tree/ExtractProof.olean -i ./lake-packages/aesop/build/lib/Aesop/Tree/ExtractProof.ilean -c ./lake-packages/aesop/build/ir/Aesop/Tree/ExtractProof.c
error: stderr:
failed to write './lake-packages/aesop/build/lib/Aesop/Tree/ExtractProof.olean': 2 No such file or directory
error: external command `/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2023-01-29/bin/lean` exited with code 1

[Patrick Massot]

error: > LEAN_PATH=./lake-packages/mathlib/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./build/lib:./lake-packages/std/build/lib LD_LIBRARY_PATH=/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2023-01-29/lib:./lake-packages/mathlib/build/lib /home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2023-01-29/bin/lean -DwarningAsError=true -Dpp.unicode.fun=true ./lake-packages/mathlib/././Mathlib/Algebra/Group/Semiconj.lean -R ./lake-packages/mathlib/./. -o ./lake-packages/mathlib/build/lib/Mathlib/Algebra/Group/Semiconj.olean -i ./lake-packages/mathlib/build/lib/Mathlib/Algebra/Group/Semiconj.ilean -c ./lake-packages/mathlib/build/ir/Mathlib/Algebra/Group/Semiconj.c
error: stdout:
./lake-packages/mathlib/././Mathlib/Algebra/Group/Semiconj.lean:124:4: error: invalid 'calc' step, left-hand-side is
  a * ↑x⁻¹ : M
expected
  ↑x⁻¹ : M
./lake-packages/mathlib/././Mathlib/Algebra/Group/Semiconj.lean:140:4: error: invalid 'calc' step, left-hand-side is
  ↑a⁻¹ * y : M
expected
  y : M
error: external command `/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2023-01-29/bin/lean` exited with code 1

[Patrick Massot]

I guess I could use the stopgap from https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unexpander.20for.20function.20composition and show Lean 4 anyway.

[Patrick Massot]

I'm playing the human-mathport game on a Lean 3 tutorial. The really nice part is deleting all those commas. The really really sad one is adding all those square brackets for single rewrites. This super painful and hurts the eye so much...

[Mario Carneiro]

by the way you can define your own rw as a macro for the normal one if you want to get rid of the brackets

[Patrick Massot]

Is mathlib4 meant to weight more than 850Mb already?

[Patrick Massot]

I guess this ends the idea of using it for my interactive demo. Participants will have machines with limited storage.

[Patrick Massot]

In Lean 3 I could distribute a demo package including lean itself and enough mathlib to get data.real.basic in 133Mb. It seems the price in Lean 4 without including Lean 4 itself is 1.2Gb.

[Patrick Massot]

Surely I have messed up something

[Patrick Massot]

Is https://github.com/xubaiw/Unicode.lean really needed? This alone is already 102Mb

[Mario Carneiro]

what are you measuring?

[Patrick Massot]

Folder size on hard drive

[Mario Carneiro]

after build?

[Patrick Massot]

After enough build so that you can use it, yes.

[David Renshaw]

I'm seeing similar numbers

dwrensha@hafnium:~/src/mathlib4$ du -hs .
865M    .

[Henrik Böving]

Patrick Massot said:

Is https://github.com/xubaiw/Unicode.lean really needed? This alone is already 102Mb

This is only downloaded as part of the doc-gen4 dependency...It would be cool if lake had a feature to only download dependencies that are actually required with the current configuration (i.e. if -Kdoc=on is false it doesn't download) but sadly that's not the case yet.

Quite a few of the files are also unnecessarily big due to our compiler efforts...we are storing basically unused compilation output in the .olean files so the new compiler can alreayd run on all files in hopes that we might catch errors before making it the new default after its development is done.

So overall yes there is definitely quite a lot of stuff that does not have to be in there.

[Patrick Massot]

That demo project is basically the first half of https://github.com/leanprover-community/tutorials. In Lean 3, you can download 133Mb, including lean itself, and do the exercices. In Lean 4 it seems to be 1.2Gb.

[Patrick Massot]

Is it possible to turn off the new compiler output stuff?

[Henrik Böving]

Not directly but I might have an idea for a hack :tm: ...

[Henrik Böving]

So in theory with this:

import Lean.Compiler.LCNF.Main

@[cpass]
def stop : Lean.Compiler.LCNF.PassInstaller where
  install := fun _ => return #[]

you can tell the new compiler that it should just drop its list of pre-configured compiler passes and do nothing. And this does actually work...the only issue is that this does of course need to run before we process the files so it would need to be an extra import everywhere which I didn't think about before :(

[Patrick Massot]

You mean in every mathlib file for instance?

[Henrik Böving]

Yes...unless there is another way to run this piece of code before the compiler is run on each file. I unfortunately don't know much about how the new compiler hooks into the elaborator, Leo just did that at some point.

[Mario Carneiro]

I think a better approach would be an option to disable the old and/or new compiler

[Mario Carneiro]

then you could set it in the lakefile

[Henrik Böving]

Yeah for sure it would

[Henrik Böving]

You could hook either into the calls that are made to this function: https://github.com/leanprover/lean4/blob/5349a089e5bb6905eaca1a09e2b587488f8e4715/src/Lean/CoreM.lean#L299-L299 or directly into https://github.com/leanprover/lean4/blob/5349a089e5bb6905eaca1a09e2b587488f8e4715/src/Lean/Compiler/LCNF/Main.lean#L87-L88 this function. I'm afraid I need to go to bed now though since I have to get up early and won't be able to make a PR for this until tomorrow evening/night so if you want this quickly someone else will have to insert the option. I don't think it should be too hard though.

[Patrick Massot]

Thank you very much for having spent time to think about this!

[Mario Carneiro]

@Patrick Massot said:

Is there any hope to get a version of mathlib4 using a Lean4 that includes https://github.com/leanprover/lean4/commit/18297d8d918cc808c37c23ad497bca7f98dbe973 before Tuesday?

not sure if you talked yourself out of it anyway, but mathlib + deps are now on 01-29.

[Patrick Massot]

Thank you very much Mario! I still don't know whether I'll use Lean 4 tomorrow. I'm waiting to hear about how much storage space is available. Initially I announced that I would need about 200Mb and now I need at least 850Mb (I managed to save 400Mb by removing doc-gen that lake thought was useful for anyone relying on mathlib).

[Sebastian Ullrich]

That one is https://github.com/leanprover/lake/issues/149 fwiw

[Patrick Massot]

Patrick Massot said:

Thank you very much Mario! I still don't know whether I'll use Lean 4 tomorrow. I'm waiting to hear about how much storage space is available. Initially I announced that I would need about 200Mb and now I need at least 850Mb (I managed to save 400Mb by removing doc-gen that lake thought was useful for anyone relying on mathlib).

Actually that estimate was completely wrong, I forgot to look at my .elan folder. Lean alone is 875Mb per toolchain. So being able to check a Lean 4 file containing

import Mathlib.Data.Real.Basic

seems to require at least 1.6 Gb of disk space after optimizing mathlib4 but without trying to optimize the toolchain folder. I guess there is no hope to bring this below 500Mb, so I'll give up the idea to organize a "let's try Lean 4 session" until this massive duplication issue is fixed.

[Patrick Massot]

I'm writing this for future reference if someone else is tempted, I do not mean to complain.

[Shreyas Srinivas]

adding to this thread: I notice that every time I start a new project with mathlib, (and run lake update), mathlib is built from scratch. This takes a solid 20 minutes, and my laptop fans cry for dear life. Is it possible to get the precached oleans when lake clones mathlib and avoid this build somehow?

[Shreyas Srinivas]

It makes no sense to rebuild mathlib when one is not even editing it. Just using it.

[Shreyas Srinivas]

especially when one already needs to match the lean toolchain version with mathlib

[Reid Barton]

Based on an extremely unscientific sample (one file) the mathlib 4 oleans seem to be about 5-6 times as large as the corresponding mathlib 3 oleans

[Henrik Böving]

https://github.com/leanprover/lean4/pull/2075 for enabling/disabling the new compiler.

The effects seem to be certainly significant:

# array_test.lean with new compiler
λ du out.olean
332     out.olean
# array_test.lean without new compiler
λ du out.olean
200     out.olean

[Eric Wieser]

That sounds like it might be a problem for our Azure costs in the long run, althoughlake exe cache is arguably better at reducing duplication than leanproject get-cache was

[Henrik Böving]

CC: @Mario Carneiro @Patrick Massot if you can still be fancied :P

[Patrick Massot]

Thanks!

[Shreyas Srinivas]

Eric Wieser said:

That sounds like it might be a problem for our Azure costs in the long run, althoughlake exe cache is arguably better at reducing duplication than leanproject get-cache was

How about local caches? The same version of mathlib might be used in many projects. So why not download a given version of mathlib and compile it the first time, and store them alongwith the object files in some central place, like toolchains are at the moment. Then a new version is downloaded and compiled only if required.

[Kevin Buzzard]

I have about 50 Lean 3 projects on the computer I'm writing this on and I am highly confident that they will use 50 different versions of mathlib 3 (most of which are costing me 700MB of storage). The issue is that mathlib3 updates about 10 times a day!

[Shreyas Srinivas]

Kevin Buzzard said:

I have about 50 Lean 3 projects on the computer I'm writing this on and I am highly confident that they will use 50 different versions of mathlib 3 (most of which are costing me 700MB of storage). The issue is that mathlib3 updates about 10 times a day!

But you would still save space if they were stored centrally even if in the future, two projects used each version.

[Shreyas Srinivas]

and compile time

[Shreyas Srinivas]

The only upside I can see for downloading a local copy for each project is getting reproducible builds for your project. But this might not be a requirement for most use cases. I am not sure it is necessary for even that on second thought.

[Kevin Buzzard]

All I'm saying is "the same version of mathlib might be used in many projects" is an extremely optimistic hope, given that when you make a new project you just clone mathlib master which is different to mathlib master from 2 hours ago.

[Shreyas Srinivas]

Hmm... makes sense if that is your use case. Does it make sense for everyone to use the latest version that is released every two hours? Not all changes might be bug fixes, so if someone is using mathlib for some part of it that has been stable for some time, does it make sense for them to recompile it for some additional results, that are extraneous to their needs?

[Eric Wieser]

Kevin, note that caches are now per-file rather than global; so it's likely that your two projects on mathlib versions a few weeks apart can use the same cache for Logic.Basic even if they can't use the same cache for downstream files

[Eric Wieser]

Shreyas Srinivas said:

Does it make sense for everyone to use the latest version that is released every two hours? Not all changes might be bug fixes, so if someone is using mathlib for some part of it that has been stable for some time, does it make sense for them to recompile it for some additional results, that are extraneous to their needs?

We're not talking about users upgrading every two hours, we're talking about two users starting their own projects two hours apart from each other.

[Shreyas Srinivas]

My original issue was about one user (in this case me), having to recompile mathlib because of either 1. no changes or 2. some changes that are not relevant to me).

[Shreyas Srinivas]

and then storing it twice.

[Shreyas Srinivas]

Maybe in the future these issues are resolved when there are stable releases and each mathlib user has a central folder containing the versions they need with the respective caches after first compile.

[Eric Wieser]

@Shreyas Srinivas, if you're working on a downstream project you should never have to "recompile mathlib", and should be running lake exe cache. Are you talking about working on mathlib itself?

[Eric Wieser]

(or did we never implement lake exe cache for downstream projects?)

[Shreyas Srinivas]

I recall that discussion: it was suggested that we need something that just works for mathlib4 for the moment.

[Shreyas Srinivas]

I can't use it anyway because my curl version is too low or something

[Shreyas Srinivas]

Even if lake exe cache works, that only solves the compile issue, not the massive storage issue.

[Arthur Paulino]

lake exe cache works for downstream projects if you set the dependency properly. And it uses an unified cache folder for multiple projects in your computer

[Arthur Paulino]

(it wasn't originally implemented like that, but Johan asked for this change because he had multiple copies of mathlib4 on his machine and he was doing too many downloads of the same files to different folders)

[Sebastian Ullrich]

Arthur Paulino said:

lake exe cache works for downstream projects if you set the dependency properly. And it uses an unified cache folder for multiple projects in your computer

But that's just the tarballs, no? Since this discussion was mainly about storage size, we would have to store the .oleans there as well and hard- or symlink them into the projects. At which point there would be no need for keeping around the tarballs anymore.

[Shreyas Srinivas]

Is it possible, if either curl doesn't work (version issues), or if there is no internet, to locally build the required version of mathlib once and store the locally built files in the cache with lake exe cache?

[Arthur Paulino]

Yes, that's lake exe cache mk. Then you can unpack with lake exe cache unpack. Try lake exe cache for more options

[Arthur Paulino]

Sebastian Ullrich said:

Arthur Paulino said:

lake exe cache works for downstream projects if you set the dependency properly. And it uses an unified cache folder for multiple projects in your computer

But that's just the tarballs, no? Since this discussion was mainly about storage size, we would have to store the .oleans there as well and hard- or symlink them into the projects. At which point there would be no need for keeping around the tarballs anymore.

Sorry, I don't understand your point. the compressid olean files are in the tarbals. So is two projects need the same olean, lake exe cache makes use of the same tar file

[Eric Wieser]

I think the point is that there are n+1 copies of the olean; one in each project and one in the original tarball

[Eric Wieser]

Rather than a single copy and a lot of symlinks

[Eric Wieser]

But symlinks are hard on windows

[Arthur Paulino]

Ah, I get it now. I've thought of an unified folder for oleans in the past, instead of putting built files inside a build folder for each project. But that's in the scope of Lake, of course.

I mean, Lake could implement something similar to what cache is doing: have a target lake_store folder and put everything there, named by hash. But then a better hash would be even more advised.

As a bonus, that would make the implementation of lake exe cache simpler because the target folder of cached files would be trivial

[Reid Barton]

Thanks for the tip btw, I just deleted 8 gigs of lean4 toolchains from 2022

[Kevin Buzzard]

buzzard@buster:~/.elan$ du -sh
26G .

[Mario Carneiro]

is there an elan issue for garbage collection?

[Arthur Paulino]

I know Jannis has implemented an independent script that does that. I usually just do it by hand via the elan toolchain CLI

[Kevin Buzzard]

and coincidentally

buzzard@buster:~/lean-projects$ du -sh
26G .

[Mario Carneiro]

I would like to have elan do garbage collection automatically given some user-configurable caching policy (even if the default is to keep everything). It is very easy not to realize that your elan folder is ballooning, so a manually triggered script doesn't really solve the problem

[Mario Carneiro]

not to mention that it can't help all the people who don't know how to work a console

[Mario Carneiro]

last I recall just deleting folders in the elan directory puts it in a weird state

[Mario Carneiro]

and that's the most obvious thing to do in response to giant folders on your HD

[Kevin Buzzard]

yeah, just deleting directories in .elan/toolchains messes things up (you can't use the toolchain again IIRC); you also have to delete the corresponding 87-or-so byte file in .elan/update-hashes.

[Mario Carneiro]

I wonder whether we can put that file in the directory as well so that one folder deletion just works

[Yaël Dillies]

Eric Wieser said:

Kevin, note that caches are now per-file rather than global; so it's likely that your two projects on mathlib versions a few weeks apart can use the same cache for Logic.Basic even if they can't use the same cache for downstream files

Can we gather data about how often a file had its cache invalidated over, say, the past year? My guess is "often", because files have many imports and even basic files change regularly.

[Arthur Paulino]

That's a tricky query but can be done by navigating the commit history, computing the hashes and counting the number of hashes each file has had

[Arthur Paulino]

But each toolchain bump is a guaranteed invalidation of the entire cache folder. So while the toolchain isn't stable enough, we should expect 1 or two complete wipes every week I think. So, again, remember to lake exe cache clean once in a while

[Arthur Paulino]

Idea: make any call to lake exe cache print a suggestion to lake exe cache clean once the number of cached files reaches, say, 4 times the number of files that are actually relevant at the moment

[Shreyas Srinivas]

Arthur Paulino said:

Yes, that's lake exe cache mk. Then you can unpack with lake exe cache unpack. Try lake exe cache for more options

lake exe cache mk fails if I have the wrong version of curl.

[Shreyas Srinivas]

is curl necessary if I don't want the remotely cached oleans?

[Arthur Paulino]

Good point. I'm baking a quick fix

[Arthur Paulino]

!4#1956

[Shreyas Srinivas]

Deleted wrong message

[Jannis Limperg]

Arthur Paulino said:

I know Jannis has implemented an independent script that does that. I usually just do it by hand via the elan toolchain CLI

This one: https://github.com/JLimperg/elan-cleanup

[Henrik Böving]

Henrik Böving said:

https://github.com/leanprover/lean4/pull/2075 for enabling/disabling the new compiler.

The effects seem to be certainly significant:

# array_test.lean with new compiler
λ du out.olean
332     out.olean
# array_test.lean without new compiler
λ du out.olean
200     out.olean

https://github.com/leanprover/lean4/pull/2075 is merged now, so mathlib4 could in theory decide to disable the new code generator, most likely saving quite a bit of space if you want to.

[Patrick Massot]

I'm tempted to say we should be doing this for now, especially since we have several summer schools coming up where we'll ask participants to install Lean+mathlib4.

[Mario Carneiro]

Yes, I think there is not much point keeping the new compiler enabled in std or mathlib, at least while development is on hiatus, and even once it starts up again we can have a custom testing build of the new compiler + other projects

[Sebastian Ullrich]

I'm assuming any downstream projects would have to disable the option as well?

[Mario Carneiro]

yeah it would be nice if the option could be set in a "sticky" way since it will almost certainly be useless to run the new compiler on projects downstream of std/mathlib if they disable it

[Mario Carneiro]

also @Henrik Böving I hope lean4#2075 isn't the source of the test failures that are currently breaking lean4 master...

[Mario Carneiro]

a bunch of compile tests are timing out

[Henrik Böving]

I mean the tests on the PR itself did pass, but maybe something changed in the mean time...

[Henrik Böving]

image.png
not my fault!

[Mario Carneiro]

6 PRs and a fix from leo were merged at the same time, it's not clear which was the cause

[Henrik Böving]

But don't we run tests for each of them? Or are all those runs at the same time?

[Mario Carneiro]

bors doesn't run on lean4

[Mario Carneiro]

6 of the red X's are just "this run was cancelled because of the following commit"

[Henrik Böving]

I see. But my PR does keep the state from before, previously new code generation was on by default and now it is still on by default, so it should be a no-op to our tests :tm:

[Mario Carneiro]

I don't see anything from any of the PRs that would reasonably cause the timeouts

[Scott Morrison]

Patrick Massot said:

I'm tempted to say we should be doing this for now, especially since we have several summer schools coming up where we'll ask participants to install Lean+mathlib4.

!4#4573

[Patrick Massot]

I forgot about that, thanks @Scott Morrison! Unfortunately it doesn't build.

[Scott Morrison]

@Patrick Massot, now building locally for me, hopefully CI agrees soon. :-)

[Patrick Massot]

Great!

[Scott Morrison]

It actually only makes a small difference (-5%) to the size of the build directory.

[Scott Morrison]

!4#4573 is compiling now. !bench concurs that it's only a 5% reduction in olean size.