Zulip Chat Archive

Stream: mathlib4

Topic: New Project that uses MathLib4


Alcides Fonseca (Dec 21 2021 at 14:30):

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 (Dec 21 2021 at 14:31):

Alcides Fonseca has marked this topic as unresolved.

Sebastian Ullrich (Dec 21 2021 at 14:39):

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 (Dec 21 2021 at 15:20):

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

Sebastian Ullrich (Dec 21 2021 at 15:45):

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

Alcides Fonseca (Dec 21 2021 at 19:32):

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

Notification Bot (Jan 29 2023 at 21:20):

Patrick Massot has marked this topic as unresolved.

Patrick Massot (Jan 29 2023 at 21:21):

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 (Jan 29 2023 at 21:21):

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

Mario Carneiro (Jan 29 2023 at 21:23):

you should open an issue for that

Patrick Massot (Jan 29 2023 at 21:23):

Where?

Mario Carneiro (Jan 29 2023 at 21:23):

lake

Patrick Massot (Jan 29 2023 at 21:24):

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 (Jan 29 2023 at 21:24):

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 (Jan 29 2023 at 21:26):

I opened a lake issue.

Mario Carneiro (Jan 29 2023 at 21:27):

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 (Jan 29 2023 at 21:28):

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

Mario Carneiro (Jan 29 2023 at 21:28):

what broke?

Patrick Massot (Jan 29 2023 at 21:28):

aesop didn't build and calc failed in mathlib.

Patrick Massot (Jan 29 2023 at 21:29):

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 (Jan 29 2023 at 21:29):

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 (Jan 29 2023 at 21:32):

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 (Jan 29 2023 at 21:46):

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 (Jan 29 2023 at 21:55):

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 (Jan 29 2023 at 21:57):

Is mathlib4 meant to weight more than 850Mb already?

Patrick Massot (Jan 29 2023 at 21:58):

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

Patrick Massot (Jan 29 2023 at 22:01):

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 (Jan 29 2023 at 22:01):

Surely I have messed up something

Patrick Massot (Jan 29 2023 at 22:04):

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

Mario Carneiro (Jan 29 2023 at 22:04):

what are you measuring?

Patrick Massot (Jan 29 2023 at 22:05):

Folder size on hard drive

Mario Carneiro (Jan 29 2023 at 22:05):

after build?

Patrick Massot (Jan 29 2023 at 22:05):

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

David Renshaw (Jan 29 2023 at 22:06):

I'm seeing similar numbers

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

Henrik Böving (Jan 29 2023 at 22:06):

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 (Jan 29 2023 at 22:06):

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 (Jan 29 2023 at 22:11):

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

Henrik Böving (Jan 29 2023 at 22:15):

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

Henrik Böving (Jan 29 2023 at 22:22):

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 (Jan 29 2023 at 22:24):

You mean in every mathlib file for instance?

Henrik Böving (Jan 29 2023 at 22:25):

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 (Jan 29 2023 at 22:27):

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

Mario Carneiro (Jan 29 2023 at 22:27):

then you could set it in the lakefile

Henrik Böving (Jan 29 2023 at 22:27):

Yeah for sure it would

Henrik Böving (Jan 29 2023 at 22:30):

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 (Jan 29 2023 at 22:33):

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

Mario Carneiro (Jan 29 2023 at 23:50):

@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 (Jan 30 2023 at 07:25):

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 (Jan 30 2023 at 08:45):

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

Patrick Massot (Jan 30 2023 at 13:16):

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 (Jan 30 2023 at 13:17):

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

Shreyas Srinivas (Jan 30 2023 at 14:44):

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 (Jan 30 2023 at 14:46):

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

Shreyas Srinivas (Jan 30 2023 at 14:48):

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

Reid Barton (Jan 30 2023 at 15:01):

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 (Jan 30 2023 at 16:09):

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 (Jan 30 2023 at 16:09):

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 (Jan 30 2023 at 16:11):

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

Patrick Massot (Jan 30 2023 at 16:13):

Thanks!

Shreyas Srinivas (Jan 30 2023 at 16:17):

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 (Jan 30 2023 at 16:20):

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 (Jan 30 2023 at 16:22):

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 (Jan 30 2023 at 16:22):

and compile time

Shreyas Srinivas (Jan 30 2023 at 16:25):

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 (Jan 30 2023 at 16:29):

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 (Jan 30 2023 at 16:36):

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 (Jan 30 2023 at 16:37):

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 (Jan 30 2023 at 16:38):

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 (Jan 30 2023 at 16:39):

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 (Jan 30 2023 at 16:39):

and then storing it twice.

Shreyas Srinivas (Jan 30 2023 at 16:41):

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 (Jan 30 2023 at 16:42):

@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 (Jan 30 2023 at 16:43):

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

Shreyas Srinivas (Jan 30 2023 at 16:44):

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

Shreyas Srinivas (Jan 30 2023 at 16:46):

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

Shreyas Srinivas (Jan 30 2023 at 16:48):

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

Arthur Paulino (Jan 30 2023 at 16:57):

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 (Jan 30 2023 at 16:59):

(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 (Jan 30 2023 at 17:44):

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 (Jan 30 2023 at 18:36):

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 (Jan 30 2023 at 18:40):

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 (Jan 30 2023 at 18:45):

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 (Jan 30 2023 at 18:46):

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 (Jan 30 2023 at 18:46):

Rather than a single copy and a lot of symlinks

Eric Wieser (Jan 30 2023 at 18:46):

But symlinks are hard on windows

Arthur Paulino (Jan 30 2023 at 18:49):

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 (Jan 30 2023 at 19:36):

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

Kevin Buzzard (Jan 30 2023 at 19:39):

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

Mario Carneiro (Jan 30 2023 at 19:43):

is there an elan issue for garbage collection?

Arthur Paulino (Jan 30 2023 at 19:45):

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 (Jan 30 2023 at 19:46):

and coincidentally

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

Mario Carneiro (Jan 30 2023 at 19:48):

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 (Jan 30 2023 at 19:49):

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

Mario Carneiro (Jan 30 2023 at 19:49):

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

Mario Carneiro (Jan 30 2023 at 19:50):

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

Kevin Buzzard (Jan 30 2023 at 19:58):

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 (Jan 30 2023 at 19:59):

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

Yaël Dillies (Jan 30 2023 at 20:10):

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 (Jan 30 2023 at 20:19):

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 (Jan 30 2023 at 20:22):

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 (Jan 30 2023 at 20:32):

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 (Jan 30 2023 at 21:50):

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 (Jan 30 2023 at 21:51):

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

Arthur Paulino (Jan 30 2023 at 21:58):

Good point. I'm baking a quick fix

Arthur Paulino (Jan 30 2023 at 22:13):

!4#1956

Shreyas Srinivas (Jan 31 2023 at 09:16):

Deleted wrong message

Jannis Limperg (Jan 31 2023 at 11:29):

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 (May 29 2023 at 14:41):

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 (May 29 2023 at 14:43):

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 (May 29 2023 at 14:44):

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 (May 29 2023 at 14:51):

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

Mario Carneiro (May 29 2023 at 14:53):

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 (May 29 2023 at 14:54):

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

Mario Carneiro (May 29 2023 at 14:54):

a bunch of compile tests are timing out

Henrik Böving (May 29 2023 at 14:55):

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

Henrik Böving (May 29 2023 at 14:55):

image.png
not my fault!

Mario Carneiro (May 29 2023 at 14:55):

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

Henrik Böving (May 29 2023 at 14:56):

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

Mario Carneiro (May 29 2023 at 14:56):

bors doesn't run on lean4

Mario Carneiro (May 29 2023 at 14:57):

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

Henrik Böving (May 29 2023 at 14:58):

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 (May 29 2023 at 14:58):

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

Scott Morrison (Jun 02 2023 at 01:27):

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 (Jun 02 2023 at 06:08):

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

Scott Morrison (Jun 04 2023 at 08:31):

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

Patrick Massot (Jun 04 2023 at 08:35):

Great!

Scott Morrison (Jun 04 2023 at 09:23):

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

Scott Morrison (Jun 04 2023 at 23:29):

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


Last updated: Dec 20 2023 at 11:08 UTC