Zulip Chat Archive

Stream: general

Topic: OOM errors when compiling mathlib on AWS

Jason Rute (Jan 11 2021 at 17:00):

I'm compiling mathlib with lean --make _target/dep/mathlib/src/all.lean on an 8G AWS EC2 instance (m4.large to be exact). But it gets prematurely killed due to Out of Memory. I'm not an expert in these sort of things. I think taken at face value, I can increase to a higher memory EC2 instance (but is 8G really not enough!?!) or add swap memory to my instance. However, before I explore those options, does anyone here have any experience with this sort of thing? (And to be clear, I need to compile it myself since I'm working with a modified version of lean core and mathlib.)

Jason Rute (Jan 11 2021 at 17:01):

For example, for CI and compiling mathlib olean files, what specs are used on the instances doing the work?

Bryan Gin-ge Chen (Jan 11 2021 at 17:41):

Mathlib CI uses GitHub-hosted runners for GitHub Actions, so the specs should be the ones here:

Each virtual machine has the same hardware resources available.
- 2-core CPU
- 7 GB of RAM memory
- 14 GB of SSD disk space

Jason Rute (Jan 11 2021 at 17:43):

@Bryan Gin-ge Chen Does it set the memory parameter --memory=num -M option when compiling lean? (Also, does it have swap memory?)

Bryan Gin-ge Chen (Jan 11 2021 at 17:46):

We don't set -M but we do set -T100000: https://github.com/leanprover-community/mathlib/blob/master/.github/workflows/build.yml#L69

I don't know whether the machines use swap memory. (I don't know anything about the systems beyond the page I linked, unfortunately.)

Gabriel Ebner (Jan 11 2021 at 17:50):

Setting --memory will just make Lean abort if it uses too much memory.

Gabriel Ebner (Jan 11 2021 at 17:50):

I'd add swap first.

Jason Rute (Jan 11 2021 at 17:51):

Do you know how much memory a (non-swap) instance needs in general to compile mathlib? (I'll probably will go with swap, but I'm curious.)

Gabriel Ebner (Jan 11 2021 at 18:05):

Ok, I just compiled mathlib real quick for you. Peak memory usage is 20.1 gigabytes 19.2 GiB:

        Command being timed: "lean --make src/"
        User time (seconds): 14476.39
        System time (seconds): 42.63
        Percent of CPU this job got: 2130%
        Elapsed (wall clock) time (h:mm:ss or m:ss): 11:21.40
        Average shared text size (kbytes): 0
        Average unshared data size (kbytes): 0
        Average stack size (kbytes): 0
        Average total size (kbytes): 0
        Maximum resident set size (kbytes): 20122968
        Average resident set size (kbytes): 0
        Major (requiring I/O) page faults: 6020
        Minor (reclaiming a frame) page faults: 5388330
        Voluntary context switches: 1972429
        Involuntary context switches: 389149
        Swaps: 0
        File system inputs: 32608
        File system outputs: 327072
        Socket messages sent: 0
        Socket messages received: 0
        Signals delivered: 0
        Page size (bytes): 4096
        Exit status: 0

Sebastian Ullrich (Jan 11 2021 at 18:11):

This probably scales more or less linearly with -j?

Gabriel Ebner (Jan 11 2021 at 18:12):

Yes. There are a few points where it only uses 4 cores, but typically Lean manages to utilize >20 threads.

Sebastian Ullrich (Jan 11 2021 at 18:13):

@Jason Rute So use -j0 for 0 memory usage :grinning_face_with_smiling_eyes:

Gabriel Ebner (Jan 11 2021 at 18:14):

Oh, you mean that memory usage scales? I don't think so. The memory usage grew at a pretty constant rate while compiling mathlib.

Gabriel Ebner (Jan 11 2021 at 18:15):

Or maybe there are thread-local leaks?

Mario Carneiro (Jan 11 2021 at 18:36):

I've been using -j0 to compile mathlib for a while

Last updated: Aug 03 2023 at 10:10 UTC