Stream: fiat-crypto

Topic: Fiat crypto and flambda

Karl Palmskog (Oct 12 2022 at 18:27):

I was going to try and play around with coq-fiat-crypto.0.0.15 on Coq 8.15, but I quickly got this compilation issue, seemingly during compilation of code extracted to OCaml:

Fatal error: exception Stack overflow
make: *** [Makefile:596: src/ExtractionOCaml/saturated_solinas] Error 2
make: *** Waiting for unfinished jobs....

Is it because I use OCaml with flambda maybe? What is the recommended OCaml version?

Karl Palmskog (Oct 12 2022 at 18:29):

for the record:

ocaml-option-flambda     1              Set OCaml to be compiled with flambda activated
ocaml-variants           4.13.1+options Official release of OCaml 4.13.1

Paolo Giarrusso (Oct 12 2022 at 18:40):

If Flambda just needs some more stack, increasing your soft ulimit on stack size. For instance, my hard limit is 64MB, my soft limit is 8MB, and I can raise the soft one:

$ ulimit -H -s
65520
$ ulimit -S -s
8176
$ ulimit -S -s 16384
$ ulimit -S -s
16384

Paolo Giarrusso (Oct 12 2022 at 18:41):

If Flambda just needs some more stack, increasing your soft ulimit on stack size. For instance, my hard limit is 64MB, my soft limit is 8MB, and I can raise the soft one:

$ ulimit -H -s
65520
$ ulimit -S -s
8176
$ ulimit -S -s 16384
$ ulimit -S -s
16384

Paolo Giarrusso (Oct 12 2022 at 18:41):

(this is from a Mac, but the same commands should work on Linux)

Jason Gross (Oct 12 2022 at 18:43):

Yeah, those particular Makefile targets run out of stack easily on the default soft limits. I should tag a new release; I recently added a warning suggesting an increase in stack size for those targets.

Karl Palmskog (Oct 12 2022 at 18:47):

OK, yes, that needs to be flagged up somewhere for sure, preferably also in the opam package description

Paolo Giarrusso (Oct 12 2022 at 18:52):

maybe the Makefile have wrapper targets that automate that — I agree that can't work for all systems, but it probably would work for many?

Paolo Giarrusso (Oct 12 2022 at 18:54):

strawman:

all_wrapped:
    $(SHELL) -c "ulimit -S -s 16384; $(MAKE) all"

Karl Palmskog (Oct 12 2022 at 19:16):

for flambda, 16384 was not enough... succeeded with 32768

Michael Soegtrop (Oct 13 2022 at 08:46):

Yes, in Coq Platform (which has lambda enabled), I also needed 32M stack size for fiat-crypto. 16M would not do. Since we are talking Ms and not Gs here, I don't see a good reason for not being a bit generous.

Jason Gross (Oct 13 2022 at 09:10):

I've made https://github.com/mit-plv/fiat-crypto/pull/1430

Michael Soegtrop (Oct 13 2022 at 09:14):

Does this mean I can remove the ulimit calls from Coq Platform?

Jason Gross (Oct 13 2022 at 09:14):

Not until I tag a new release and update the opam package

Jason Gross (Oct 13 2022 at 09:15):

(and merge the PR)

Michael Soegtrop (Oct 13 2022 at 09:15):

I had 2023.03 in mind ...

Jason Gross (Oct 13 2022 at 17:21):

Yeah, once 1430 is merged, you can remove the calls to ulimit. Btw, do you know if there's a conf-* opam package to require to make sure ulimit is available?

Karl Palmskog (Oct 13 2022 at 17:37):

there's no conf-ulimit or similar to my knowledge. I suppose we could create one, preferably in the OCaml repo, but could otherwise live in the Platform repo....

Michael Soegtrop (Oct 14 2022 at 07:45):

I would create one in the OCaml main repo - in my experience they are very open to such things and arguably this is really useful for OCaml.

Karl Palmskog (Oct 14 2022 at 07:47):

as per discussion here, it seems bash is already assumed in many opam packages, and there is no obvious conf- for ulimit.

Jason Gross (Oct 16 2022 at 07:12):

@Michael Soegtrop I have merged https://github.com/coq/opam-coq-archive/pull/2352 so when you use fiat-crypto 0.0.16, you should no longer need ulimit

Michael Soegtrop (Oct 16 2022 at 08:46):

@Jason Gross : should I change it in the 2022.09 release. The beta is out. I usually don't change packages from beta to release without a good reason, but for a new and experimental package I don't see issues doing so if you recommend it.

Jason Gross (Oct 16 2022 at 08:49):

I think in this case it might be worth changing (actually let me release 0.0.17, there's a bug in the ulimit script that makes it always be invoked in 0.0.16). The main improvement is that the most RAM-intensive file now takes under 3GB RAM instead of over 5GB RAM. This is probably worth picking up for people building from source? There's very little of note changed beyond that.

Michael Soegtrop (Oct 16 2022 at 09:04):

OK, sounds good. Can you please reopen https://github.com/coq/platform/issues/178 and leave a note there, both to document the decisions and to make sure I don't forget to update?

Last updated: Apr 19 2024 at 16:01 UTC