Zulip Chat Archive

Stream: new members

Topic: building mathlib


view this post on Zulip Iocta (Apr 06 2020 at 20:45):

The normal workflow with elan and leanproject works for me but I am curious about what's involved in building mathlib manually. I just tried lean --make --memory 6000 which is 6GB and hit the limit with src/topology/metric_space/gromov_hausdorff.lean:381:2: error: excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold). What does it normally take to build mathlib: how much ram, how many compute hours?

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 20:58):

In the past I've compiled mathlib with those parameters in about 20 minutes

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 20:58):

But it's getting bigger all the time

view this post on Zulip Bryan Gin-ge Chen (Apr 06 2020 at 21:04):

It takes about 1h50m to build mathlib in our Github Actions workflow. Here's their page on the resources available. Apparently they let us use up to 7 GB of memory.


Last updated: May 09 2021 at 19:11 UTC