Stream: Coq devs & plugin devs

Topic: Building with memory limits

Ali Caglayan (Jul 21 2021 at 14:27):

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?

Ali Caglayan (Jul 21 2021 at 14:29):

The changes that caused this are https://github.com/coq/coq/pull/14685

Ali Caglayan (Jul 21 2021 at 14:29):

if you do dune build theories/ it will complain about two places

Ali Caglayan (Jul 21 2021 at 14:29):

change the attributes there to #[local] and then do dune build theories/ again

Ali Caglayan (Jul 21 2021 at 14:29):

but be careful since there is something wrong here

Ali Caglayan (Jul 21 2021 at 14:31):

I'm doing this all in vscode I don't know if that affects anything

Ali Caglayan (Jul 21 2021 at 14:32):

Does anybody else have a safety net when hacking? If so how?

Pierre-Marie Pédrot (Jul 21 2021 at 14:34):

it's rare to get OOM when compiling the stdlib

Pierre-Marie Pédrot (Jul 21 2021 at 14:34):

some developments are memory intensive, in which case I usually restrict the number of jobs

Jason Gross (Jul 22 2021 at 00:52):

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

Paolo Giarrusso (Jul 22 2021 at 14:48):

VSCode uses async proofs which adds some bugs over Coqc, but I can't imagine bugs from the vscode-dune combo

Paolo Giarrusso (Jul 22 2021 at 14:50):

OTOH please restrict the number of jobs with -j N, using too many jobs is unlikely to speed things up

Ali Caglayan (Jul 22 2021 at 14:59):

Yeah, it is a bit annoying to have to specify -j everytime to dune

Ali Caglayan (Jul 22 2021 at 14:59):

at least with makefile not supplying j doesnt get you into trouble

Ali Caglayan (Jul 22 2021 at 14:59):

I wonder if there is a global setting for dune

Gaëtan Gilbert (Jul 22 2021 at 15:10):

https://github.com/ocaml/dune/blob/d75bd885262b98075299e9145a2aa3bd1a54a35d/bin/help.ml#L68-L72

Gaëtan Gilbert (Jul 22 2021 at 15:10):

(or man dune-config)

Ali Caglayan (Jul 22 2021 at 15:16):

Huh weird man dune-config says the default value is 4

Ali Caglayan (Jul 22 2021 at 15:23):

Wonderful worked like a charm

Ali Caglayan (Jul 22 2021 at 15:24):

Thanks!

Last updated: Jun 08 2023 at 04:01 UTC