Stream: Coq devs & plugin devs

Topic: Building with memory limits


view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Jul 21 2021 at 14:29):

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

view this post on Zulip Ali Caglayan (Jul 21 2021 at 14:29):

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

view this post on Zulip Ali Caglayan (Jul 21 2021 at 14:29):

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

view this post on Zulip Ali Caglayan (Jul 21 2021 at 14:29):

but be careful since there is something wrong here

view this post on Zulip Ali Caglayan (Jul 21 2021 at 14:31):

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

view this post on Zulip Ali Caglayan (Jul 21 2021 at 14:32):

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

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 14:34):

it's rare to get OOM when compiling the stdlib

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Jul 22 2021 at 14:59):

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

view this post on Zulip Ali Caglayan (Jul 22 2021 at 14:59):

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

view this post on Zulip Ali Caglayan (Jul 22 2021 at 14:59):

I wonder if there is a global setting for dune

view this post on Zulip Gaëtan Gilbert (Jul 22 2021 at 15:10):

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

view this post on Zulip Gaëtan Gilbert (Jul 22 2021 at 15:10):

(or man dune-config)

view this post on Zulip Ali Caglayan (Jul 22 2021 at 15:16):

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

view this post on Zulip Ali Caglayan (Jul 22 2021 at 15:23):

Wonderful worked like a charm

view this post on Zulip Ali Caglayan (Jul 22 2021 at 15:24):

Thanks!


Last updated: Oct 16 2021 at 09:07 UTC