OOM errors when compiling mathlib on AWS

Stream: general

[Jason Rute]

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]

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

[Bryan Gin-ge Chen]

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]

@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]

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]

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

[Gabriel Ebner]

I'd add swap first.

[Jason Rute]

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]

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]

This probably scales more or less linearly with -j?

[Gabriel Ebner]

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

[Sebastian Ullrich]

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

[Gabriel Ebner]

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]

Or maybe there are thread-local leaks?

[Mario Carneiro]

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