Zulip Chat Archive

Stream: general

Topic: build mathlib

Matthew Ballard (Feb 04 2022 at 17:07):

How long should leanproject build take on a cloned copy of mathlib?

Alex J. Best (Feb 04 2022 at 17:08):

Depends on your machine/number of threads, currently CI takes > 3hrs

Matthew Ballard (Feb 04 2022 at 17:08):

Memory?

Alex J. Best (Feb 04 2022 at 17:09):

Probably around 20gb?

Matthew Ballard (Feb 04 2022 at 17:11):

Adam suggested I benchmark my laptop using this:

leanproject build  41572.15s user 82.95s system 913% cpu 1:16:02.15 total

and I wanted to see how this compared.

Alex J. Best (Feb 04 2022 at 17:11):

Once again it depends how many threads you are using

Alex J. Best (Feb 04 2022 at 17:12):

Yeah that seems fairly reasonable at a glance. There is a reason most of us try to use pre-compiled oleans files as much as possible and never build mathlib ourselves any more!

Matthew Ballard (Feb 04 2022 at 17:13):

I tried it on the old laptop for comparison and it is still going...

Arthur Paulino (Feb 04 2022 at 17:19):

This gave me an idea: lake build or lake build --pretty would show a completion bar from 0 to 100%, an ETA and the current file being built

Matthew Ballard (Feb 07 2022 at 15:30):

I left my old computer running for the weekend compiling mathlib. I was hoping to to have an amusing comparison with new one. Perhaps it is still amusing

Process: lean [36557]
Path: /Users/USER/*/lean
Identifier: lean
Version: ???
Code Type: X86-64 (Translated)
Parent Process: node [36548]
User ID: 502

Date/Time: 2022-02-01 19:21:44.7102 -0500
OS Version: macOS 12.1 (21C52)
Report Version: 12
Anonymous UUID: BF09A2FC-EBDF-0218-4FD6-F5D2B942D66E

Sleep/Wake UUID: 77DBCD8F-8CAF-4F28-9EFB-2E5711ACFA68

Time Awake Since Boot: 400000 seconds
Time Since Wake: 37626 seconds

System Integrity Protection: enabled

Crashed Thread: 10

Exception Type: EXC_BAD_ACCESS (SIGSEGV)
Exception Codes: KERN_INVALID_ADDRESS at 0x000000000000000c
Exception Codes: 0x0000000000000001, 0x000000000000000c
Exception Note: EXC_CORPSE_NOTIFY

Termination Reason: Namespace SIGNAL, Code 11 Segmentation fault: 11

Matthew Ballard (Feb 07 2022 at 15:30):

TLDR: building mathlib?

M1 Max with 64 gb: ~75 minutes
M1 with 8 gb: $\infty$

Arthur Paulino (Feb 07 2022 at 15:34):

8gb? Then it was just drowning with swap memory I guess?

Matthew Ballard (Feb 07 2022 at 15:35):

My guess also. I didn't copy over the full log entry from the other machine. I would be great in DevOps.

Miguel Marco (Feb 07 2022 at 21:17):

Alex J. Best said:

Yeah that seems fairly reasonable at a glance. There is a reason most of us try to use pre-compiled oleans files as much as possible and never build mathlib ourselves any more!

Is that what you get with leanproject --get-cache? I usually do that but still need to spend quite a while coimpiling before i can work interactively.

Patrick Massot (Feb 07 2022 at 21:20):

Miguel, we would need more information about your workflow to help you.

Miguel Marco (Feb 07 2022 at 21:27):

I basically run leanproject new and start editing a file in src (I use mostly emacs with lean mode).

Just typing import tactic triggers a loooong process until i can interactively prove something seeing the goal in tactic mode and so on.

Patrick Massot (Feb 07 2022 at 21:29):

I don't know anything about Lean in emacs, but that doesn't sound right

Miguel Marco (Feb 07 2022 at 21:31):

I don't think emacs is relevant here. Didn't notice anything different one I tried vscode.

Which should be the correct workflow?

Alex J. Best (Feb 07 2022 at 21:54):

If you are working on a project that depends on mathlib (via leanproject new) the right command would be leanproject --get-mathlib-cache (though get-cache might do this automatically, I'm not sure) when you run this what does the output look like?

Patrick Massot (Feb 07 2022 at 21:57):

leanproject new should do that automatically

Miguel Marco (Feb 07 2022 at 22:01):

I get this

mmarco@neumann ~/lean/pr $ leanproject new
Move existing .lean files into the 'src' folder.
> git init -q
> git checkout -b lean-3.35.1
Cambiado a nueva rama 'lean-3.35.1'
configuring pr 0.1
Adding mathlib
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Clonando en '_target/deps/mathlib'...
remote: Enumerating objects: 241581, done.
remote: Counting objects: 100% (376/376), done.
remote: Compressing objects: 100% (52/52), done.
remote: Total 241581 (delta 360), reused 332 (delta 324), pack-reused 241205
Recibiendo objetos: 100% (241581/241581), 121.90 MiB | 15.05 MiB/s, listo.
Resolviendo deltas: 100% (192813/192813), listo.
> git checkout --detach dd1242d2aec84561c8f8651721ea1c1d8d25007a    # in directory _target/deps/mathlib
HEAD está ahora en dd1242d2a feat(algebra/associated): generalize nat.prime.pow_dvd_of_dvd_mul_{left,right} (#11301)

WARNING: Lean version mismatch: installed version is leanprover-community/lean:3.35.1, but package requires leanprover-community/lean:3.39.0


WARNING: Lean version mismatch: installed version is leanprover-community/lean:3.35.1, but package requires leanprover-community/lean:3.39.0

configuring pr 0.1
mathlib: trying to update _target/deps/mathlib to revision dd1242d2aec84561c8f8651721ea1c1d8d25007a
> git checkout --detach dd1242d2aec84561c8f8651721ea1c1d8d25007a    # in directory _target/deps/mathlib
HEAD está ahora en dd1242d2a feat(algebra/associated): generalize nat.prime.pow_dvd_of_dvd_mul_{left,right} (#11301)
Looking for pr oleans for dd1242d2a
  locally...
  Found local pr oleans
Located matching cache
Applying cache
  files extracted: 2063 [00:07, 277.28/s]
mmarco@neumann ~/lean/pr $ leanproject --get-mathlib-cache
Usage: leanproject [OPTIONS] COMMAND [ARGS]...
Try 'leanproject -h' for help.

Error: No such option: --get-mathlib-cache
mmarco@neumann ~/lean/pr $ leanproject get-mathlib-cache
Looking for pr oleans for dd1242d2a
  locally...
  Found local pr oleans
Located matching cache
Applying cache
  files extracted: 2063 [00:07, 273.11/s]

And still the long computation (and memory consuming) before being able to interactively prove anything.

If I just create a file with the imports, and then run leanproject build, I still get the long computation, but after that, I don't have to wait for it every time i open the files from the beginning.

Maybe I have something not well configured?

Julian Berman (Feb 07 2022 at 22:04):

Did you run that from a directory that already has lean files? It seems like possibly?

Miguel Marco (Feb 07 2022 at 22:06):

No, It was a freshly created directory. It is located inside a general directory where i store all my lean projects though.

Patrick Massot (Feb 07 2022 at 22:06):

Please try to run this command in /tmp

Miguel Marco (Feb 07 2022 at 22:07):

Which command do you mean?

Patrick Massot (Feb 07 2022 at 22:09):

leanprojet new pr

Miguel Marco (Feb 07 2022 at 22:12):

It doesn't make a difference

Patrick Massot (Feb 07 2022 at 22:18):

Do you have elan installed?

Patrick Massot (Feb 07 2022 at 22:18):

The Lean mismatch error is really weird

Mauricio Collares (Feb 07 2022 at 22:18):

As Patrick said, you probably installed lean directly from your package manager instead of using the preferred method, which is to install elan and let it download/manage lean versions. The olean cache only works for the exact version it was built with. Are you on Linux? How did you install lean?

Miguel Marco (Feb 07 2022 at 22:20):

Yes, I installed it with the gentoo package manger. Didn't use elan.

Patrick Massot (Feb 07 2022 at 22:23):

That's the explanation

Miguel Marco (Feb 07 2022 at 22:23):

I see, having the right version should solve it? Or Do I need to specifically use elan?

Mauricio Collares (Feb 07 2022 at 22:25):

Having the right version should solve it, where "the right version" is the one specified in leanpkg.toml for the mathlib commit you're using. It will change when new versions are released and mathlib is updated.

Mauricio Collares (Feb 07 2022 at 22:25):

But using elan is more convenient, since different projects can specify different lean versions and elan handles that seamlessly.

Patrick Massot (Feb 07 2022 at 22:26):

Not using elan is pure masochism.

Patrick Massot (Feb 07 2022 at 22:26):

And you just proved it once more.

Mauricio Collares (Feb 07 2022 at 22:27):

The problem here is that Gentoo doesn't package elan, I think

Mauricio Collares (Feb 07 2022 at 22:28):

The correct answer is to contact the maintainer and ask for an elan package

Riccardo Brasca (Feb 07 2022 at 22:29):

It's probably a bad idea to use the package manager if you want a working installation.

Riccardo Brasca (Feb 07 2022 at 22:30):

We have instructions for Linux

Miguel Marco (Feb 07 2022 at 22:32):

Thanks

Patrick Massot (Feb 07 2022 at 22:43):

Is there a Lean package in Gentoo? We should really try to kill all those fake Lean packages from distributions

Patrick Massot (Feb 07 2022 at 22:43):

Nobody is keeping them up to date. Linux distributions simply can't keep up with software that moves so fast.

Kevin Buzzard (Feb 07 2022 at 23:10):

Lean updates once a month or so, mathlib updates 10 times a day. Package managers can't handle it; you just have to pull today's set-up directly from the web, which is what elan is doing.

Matthew Ballard (Feb 07 2022 at 23:14):

https://packages.gentoo.org/packages/sci-mathematics/lean - Gentoo Mathematics Project

Arthur Paulino (Feb 08 2022 at 00:03):

I think having elan itself in package managers would be great though

Mauricio Collares (Feb 08 2022 at 00:05):

Elan is in most package managers, I think (I know of Arch, Debian and Nix). Gentoo seems to be an exception.

Arthur Paulino (Feb 08 2022 at 00:11):

I see. I meant that it would be nice to be able to do sudo apt install elan. I just tested it and it didn't work. Or am I misunderstanding something?

Mauricio Collares (Feb 08 2022 at 00:17):

Oh, sorry! For Debian-based systems, elan is only packaged on Debian Testing and on Ubuntu 22.04.

Mauricio Collares (Feb 08 2022 at 00:20):

At least I think that's what https://launchpad.net/ubuntu/jammy/+source/elan means for Ubuntu

Kevin Buzzard (Feb 08 2022 at 06:54):

How does this all work? I don't remember anyone showing up and saying "hello I'm from Gentoo/Ubuntu and we propose doing this, is it a good idea?".

On the other hand I do remember me saying "wouldn't it be a good idea" back in 2018 and various people not being optimistic, for reasons like this

Sebastian Ullrich (Feb 08 2022 at 08:37):

I don't remember anyone showing up and saying "hello I'm from Gentoo/Ubuntu and we propose doing this, is it a good idea?".

That would be entirely too convenient

Martin Dvořák (Jun 22 2023 at 14:28):

Arthur Paulino said:

I see. I meant that it would be nice to be able to do sudo apt install elan. I just tested it and it didn't work. Or am I misunderstanding something?

I just did this on WSL Ubuntu and I have no idea what I actually installed (but lake doesn't work).

Mauricio Collares (Jun 22 2023 at 16:08):

Yes, unfortunately the Debian/Ubuntu elan couldn't unpack zstd archives for a while, and this format is used by Lean 4.

Mauricio Collares (Jun 22 2023 at 16:09):

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.22binary.20package.20was.20not.20provided.20for.20'linux'.22.20on.20Ubuntu/near/313434078

Mauricio Collares (Jun 22 2023 at 16:10):

But you can install Elan "the manual way": https://github.com/leanprover/elan#manual-installation

Mauricio Collares (Jun 22 2023 at 16:12):

And there's a PPA in the other thread with an updated elan version if you prefer to use apt and Ubuntu 22.04

Last updated: Dec 20 2023 at 11:08 UTC