Too many open files in system

Stream: lean4

[Yaël Dillies]

I am maintaining a repo with a large number of parallel files and lake build only builds about 20% of the files because all the other ones fail with "Too many open files in system". This means I need to run lake build five times in a row for the build to complete! Could this be improved?

[Yaël Dillies]

The repo in question is no other than formal-conjectures, which I maintain as part of my work for GDM. The file structure is roughly

1. Some meta files
2. ...imported by FormalConjectures.Util.ProblemImports
3. ...imported by all the conjecture files

[Henrik Böving]

Yaël Dillies said:

I am maintaining a repo with a large number of parallel files and lake build only builds about 20% of the files because all the other ones fail with "Too many open files in system". This means I need to run lake build five times in a row for the build to complete! Could this be improved?

Are you doing this on a Linux system?

[Henrik Böving]

If so you should be able to overwrite the limit using ulimit -Hn and ulimit -Sn with some big value. On some systems this value is 1024 by default which is by far not enough for something like this.

[Sebastian Ullrich]

While we do not currently have OS integration on this level in Lake, it should be technically feasible to check and raise unreasonably low soft limits there as well, so please consider opening an issue

[Joseph Myers]

"Too many open files in system" (ENFILE) is not the same as "Too many open files" (EMFILE). ulimit will only help with the latter. What's the content of /proc/sys/fs/file-max? Maybe you have something in /etc/sysctl.d or /etc/sysctl.conf that reduces file-max a lot? (I'm not sure if anything can e.g. limit the number of open files in a control group as opposed to a single process or the system as a whole, and which error you'd get in that case.)

[Sebastian Ullrich]

Ah. I think Lean should be okay with the value on my machine at least...

$ sysctl fs/file-max
fs.file-max = 9223372036854775807

[Moritz Firsching]

I run in this all the time, also for buildling mathlib. Without further investigation I had usually set

export LEAN_NUM_THREADS=64

(while 128 threads are available)
when that happens.

A repo where this problem seems to be even worse is https://github.com/trishullab/PutnamBench
on that machine

$ sysctl fs/file-max                                                                                                                                                                                (base)
fs.file-max = 1048576

Next time I will try setting the limits as suggested...