Zulip Chat Archive

Stream: new members

Topic: Mathlib install memory usage


view this post on Zulip Brendan Seamas Murphy (Jun 09 2020 at 21:04):

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?

view this post on Zulip Kevin Buzzard (Jun 09 2020 at 21:05):

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

view this post on Zulip Brendan Seamas Murphy (Jun 09 2020 at 21:06):

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

view this post on Zulip Kevin Buzzard (Jun 09 2020 at 21:06):

$ 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

view this post on Zulip Brendan Seamas Murphy (Jun 09 2020 at 21:06):

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

view this post on Zulip Kevin Buzzard (Jun 09 2020 at 21:07):

Yeah, I just downloaded compiled olean files automatically.

view this post on Zulip Kevin Buzzard (Jun 09 2020 at 21:07):

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


Last updated: May 13 2021 at 06:15 UTC