Mathlib install memory usage

Stream: new members

[Brendan Seamas Murphy]

I'm having trouble installing mathlib on a new laptop. It spends half an hour or so (maybe a little more?) chugging along, steadily increases to just over 6 GB of ram used, and then my laptop chokes because it doesn't have any more memory. Is there any way to download a pre-built version or have it decrease memory usage?

[Kevin Buzzard]

What does "installing mathlib" even mean? Do you know about leanproject?

[Brendan Seamas Murphy]

I mean running "leanpkg install <insert github url>" in a terminal

[Kevin Buzzard]

$ leanproject get mathlib
Cloning from git@github.com:leanprover-community/mathlib.git
configuring mathlib 0.1
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/df34ee20df5f60e92116b5af0b3e0f78c7ad1648.tar.xz to /home/buzzard/.mathlib/df34ee20df5f60e92116b5af0b3e0f78c7ad1648.tar.xz
100%|████████████████████████████████████████████████████████████████████████████████████████████| 22.6M/22.6M [00:04<00:00, 5.40MiB/s]
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/
$

20 seconds and barely any memory usage

[Brendan Seamas Murphy]

Ahh it was building it locally for me. I'll check out leanproject

[Kevin Buzzard]

Yeah, I just downloaded compiled olean files automatically.

[Kevin Buzzard]

Look at the leanprover-community web pages, they explain the modern way of doing things.