mathlib is on 3.7!

Stream: general

[Scott Morrison]

Wow, I only just noticed: mathlib is now running on Lean 3.7.

Even cooler, I barely noticed the change; after running leanproject up on a branch that I'd just merged master into, VS Code told me it was downloading Lean, and everything _just worked_.

[Scott Morrison]

Thanks everyone for coordinating this amazing infrastructure work (both 3.7, and all the tooling).

[Sebastien Gouezel]

I need some help here.

PS C:\Users\Sebastien\Desktop\mathlib> leanproject up
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/1a398a7212f9d81e33436008594727bfb5724053.tar.gz to C:\Users\Sebastien\.mathlib\1a398a7212f9d81e33436008594727bfb5724053.tar.gz
100%|█████████████████████████████████████████████████████████████████████████████| 24.0M/24.0M [01:15<00:00, 319kiB/s]
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/
PS C:\Users\Sebastien\Desktop\mathlib> lean --version
Lean (version 3.7.1, commit 4bc3b6d65ed4, Release)
PS C:\Users\Sebastien\Desktop\mathlib> lean --make src
C:\programmation\lean\lib\lean\library\init\data\list\basic.lean: parsing at line 283

I have updated my Lean to 3.7.1 (copying the release from the website), then updated my mathlib with leanproject up. But still if I start lean --make src, it starts recompiling stuff in core. Any idea of what I might be doing wrong?

[Kevin Buzzard]

Did you try leanproject check?

[Sebastien Gouezel]

Everything looks fine

[Sebastien Gouezel]

And each time I type again lean --make src, it starts recompiling the very same files from core it has just successfully compiled on the previous run.

[Kevin Buzzard]

1a398a7212f9d81e33436008594727bfb5724053 was only committed 17 minutes ago and it has an orange blob in the list of commits

[Kevin Buzzard]

so it's maybe a bit surprising that there are oleans on the azure server, but I don't really understand how this new tooling works

[Kevin Buzzard]

oh but maybe the olean files were made when the PR was made, not when it was accepted?

[Sebastien Gouezel]

I had already the same issue with the previous commit, so I don't think this is related to this specific commit, rather something with my config. Are things working smoothly with 3.7.1 for all of you, especially on windows?

[Kevin Buzzard]

oh -- it's recompiling stuff in core??

[Sebastien Gouezel]

Yes, core (just two or three files), and then from mathlib (also two or three files), and then it is done. Doing lean --make src leads to recompilation of the very same files, again and again and again.

[Kevin Buzzard]

I can't reproduce, but I will note that leanproject up for me gives me 034685b9f3e3aba7c9972162d7201ed1473213e0which is about 9 commits ago.

[Kevin Buzzard]

buzzard@bob:~/crap/test$ more leanpkg.toml
[package]
name = "test"
version = "0.1"
lean_version = "leanprover-community/lean:3.7.1"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "034685b9f3e3aba7c9972162d7201ed1473213e0"}

[Kevin Buzzard]

Is your filesystem OK? I've had weird issues like this when using some wacky encrypted filesystem which was being stored in dropbox and i had a dropbox conflict which caused the encrypted filesystem to get a bit confused

[Sebastien Gouezel]

My filesystem looks perfectly ok, from what I can tell...

[Bryan Gin-ge Chen]

I have updated my Lean to 3.7.1 (copying the release from the website)

Hmm, does this mean you are not using elan?

[Bryan Gin-ge Chen]

Actually, I think elan downloads the same files, so even if you're not using elan I don't see how that could be the issue.

I was going to say that maybe the timestamps are affected, but I think Lean 3.7.1 no longer checks timestamps.

[Kevin Buzzard]

I use elan and have the same commit hash for my 3.7.1. Isn't it a bit surprising that leanproject up does a different thing for me though? Or not?

[Bryan Gin-ge Chen]

I think the difference is that Sebastien was working on mathlib, so leanproject up gets master, whereas you were working on a project with mathlib as a dependency, so it gets the lean-3.7.1 branch.

[Kevin Buzzard]

I see. So indeed I get https://oleanstorage.azureedge.net/mathlib/1a398a7212f9d81e33436008594727bfb5724053.tar.gz if I make a new mathlib clone but nothing compiles when I make it, it's all compiled already. Maybe it's a bad local copy of lean somehow?

[Wojciech Nawrocki]

Oh dear, more 3.7 trouble! Indeed we no longer rely on timestamps, looking at the hashes of .lean sources instead, but the aim is to recompile less, not more. I looked into the issue and believe the root cause lies in a change I introduced. To my defense, my code is actually correct, it just happens to have triggered a bug in another part of the codebase. In fact, strangely while my local compiler has nothing to say about it, the windows version of that same compiler actually caught the issue in the build logs, so perhaps it highlights a need for using some stricter compilation options. In the meantime though, we'll need a 3.7.2 release which I'll PR asap.

[Sebastien Gouezel]

Thanks for investigating this!

[Sebastien Gouezel]

3.7.2 build failed on windows :(

[Gabriel Ebner]

Where do you see this? The windows build hasn't even started for the v3.7.2 tag: https://ci.appveyor.com/project/cipher1024/lean/builds/31606100
It already passed for the corresponding commit on master: https://ci.appveyor.com/project/cipher1024/lean/builds/31605182

[Gabriel Ebner]

Please stay calm. Appveyor---the windows CI solution that we use---takes a long time to run. The windows binaries should be available within the next 24 hours.

[Sebastien Gouezel]

All right, thanks. I just noticed that on the release page all builds are available but the windows one, and that the commit was marked with a red cross on https://github.com/leanprover-community/lean/commits/master, so I guessed something had gone wrong. Happy to hear this is not the case!

[Wojciech Nawrocki]

Noted the slowness of our builds in lean#156 .

[Wojciech Nawrocki]

The Windows build seems to be available now!