I managed to hog all the memory (24GB) and completely freeze my PC building the stdlib with dune. What can I do to avoid this in the future?
The changes that caused this are https://github.com/coq/coq/pull/14685
if you do dune build theories/
it will complain about two places
change the attributes there to #[local]
and then do dune build theories/
again
but be careful since there is something wrong here
I'm doing this all in vscode I don't know if that affects anything
Does anybody else have a safety net when hacking? If so how?
it's rare to get OOM when compiling the stdlib
some developments are memory intensive, in which case I usually restrict the number of jobs
You can use ulimit
. Beware that restricting the resident (real) memory doesn't work, you can only restrict the virtual memory. Luckily, unlike Haskell programs which always ask for a terabyte of virtual RAM, OCaml programs generally only ask for slightly more than they use
VSCode uses async proofs which adds some bugs over Coqc, but I can't imagine bugs from the vscode-dune combo
OTOH please restrict the number of jobs with -j N, using too many jobs is unlikely to speed things up
Yeah, it is a bit annoying to have to specify -j everytime to dune
at least with makefile not supplying j doesnt get you into trouble
I wonder if there is a global setting for dune
https://github.com/ocaml/dune/blob/d75bd885262b98075299e9145a2aa3bd1a54a35d/bin/help.ml#L68-L72
(or man dune-config)
Huh weird man dune-config says the default value is 4
Wonderful worked like a charm
Thanks!
Last updated: Dec 07 2023 at 04:02 UTC