building mathlib

Stream: new members

[Iocta]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

But it's getting bigger all the time

[Bryan Gin-ge Chen]

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.