Building coq with dune leads to OOM

Ecosystem
1

Is anyone able to build coq 8.13 with dune 2.8 and ocaml 4.10/4.11/4.12?

For me the dune process triggers the OOM killer. I requested up to 24G for the build VM, and reduced the number of jobs to two in the dune build --verbose --for-release-of-packages=coq,coqide,coqide-server -jN @install command.

[ 270s] [ 264.545711] Out of memory: Killed process 1984 (dune) total-vm:26941436kB, anon-rss:23756844kB, file-rss:4kB, shmem-rss:0kB, UID:399 pgtables:50608kB oom_score_adj:0

I will try to go back to dune 2.7 and see if that makes any difference.

2

I’m seeing something similar on the CI machines today (not with coq though). e.g.

Out of memory: Killed process 1779038 (dune)
total-vm:91250240kB,
anon-rss:86825656kB,
file-rss:0kB, shmem-rss:0kB, UID:1000
pgtables:173220kB oom_score_adj:0
3

Am just guessing, but there was a OOM bug that was supposedly fixed just before the release, see

Could it be that the problem was not fully fixed? cc @rgrinberg @snowleopard

Cheers,
Nicolas

4

With dune 2.7.0 the build of coq gets further, but fails for other reasons.

5

That would be my first suspicion as well. Note that this issue occurs only for failing builds. I think I have an idea for what’s going on

6

We also face some OOM since we upgraded from dune 2.7.1 to 2.8.0.

7

I’ve seen this in one of my builds, too. Is there an issue associated with it to watch it?

8

This is supposed to be fixed with dune 2.8.2, via #4134 and #4122.

1 Like