Tony Arcieri (Feb 10 2023 at 19:26): Tony Arcieri (Feb 10 2023 at 19:26):I've been trying to compile fiat-crypto many, many different ways and keep running into issues. I'm currently attempting to use Docker starting from the coqorg/coq:8.15.2 container (tried a few different versions of that) and building the v0.0.17 tag (tried several different tags as a starting point)
I keep running into stack overflows during compilation (i.e. running make standalone-ocaml) on saturated_solinas.mli. Here are some examples:
#6 10902.6 Fatal error: exception Stack overflow
#6 10902.7 make: *** [Makefile:534: src/ExtractionOCaml/saturated_solinas] Error 2
#6 10902.7 make: *** Waiting for unfinished jobs....
#6 10904.7 Fatal error: exception Stack overflow
#6 10904.8 make: *** [Makefile:534: src/ExtractionOCaml/base_conversion] Error 2
#6 3548.8 OCAMLOPT src/ExtractionOCaml/saturated_solinas.mli
#6 3548.8 Warning: Stack size (8192) may be too small.
#6 3548.8 Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
I've tried setting the OCAMLRUNPARAM="b,l=32768" environment variable as well as disabling the stack ulimit on Docker, with no apparent effect. Docker's memory limit is set to 30GB.
Karl Palmskog (Feb 10 2023 at 19:33):did you try the opam package in the latest Coq Platform? https://github.com/coq/platform/blob/2022.09.1/doc/README~8.16~2022.09.md#coq-platform-2022091-with-coq-8161-extended-level
From what I remember, it works fine even without ulimit changes. Doesn't have to be installed via the Platform, of course.
Paolo Giarrusso (Feb 10 2023 at 19:51):Which hw architecture and OCaml version are you using?
Paolo Giarrusso (Feb 10 2023 at 19:53):I've seen much worse usage by Coq on ARM with older OCaml versions (OCaml 4.14.* includes the fix, and maybe some earlier versions do as well)
Karl Palmskog (Feb 10 2023 at 20:01):This is on OCaml 4.14.1 and Coq 8.16.1:
$ opam install coq-fiat-crypto.0.0.17
...
∗ installed coq-record-update.0.3.1
∗ installed coq-bignums.8.16.0
∗ installed coq-coqutil.0.0.2
∗ installed coq-coqprime.1.2.0
∗ installed coq-rewriter.0.0.7
∗ installed coq-riscv.0.0.3
∗ installed coq-bedrock2.0.0.4
∗ installed coq-rupicola.0.0.6
∗ installed coq-bedrock2-compiler.0.0.4
∗ installed coq-fiat-crypto.0.0.17
Some nice release engineering (even tweaking inside package definitions) was done by Jason Gross et al. to make this work out, so I'd avoid deviating from those versions/tags.
Tony Arcieri (Feb 10 2023 at 20:01):it's x86_64 (which doesn't help as I'm on an M2). If you have suggestions for a better starter Docker image than coqorg/coq:8.15.2 I'm all ears.
I had other trouble with 8.16 FWIW
Tony Arcieri (Feb 10 2023 at 20:01):oh nice!
Tony Arcieri (Feb 10 2023 at 20:01):I'll give that a try
Karl Palmskog (Feb 10 2023 at 20:03):(I'm on x86_64 though, no idea if M2 makes a difference)
Jason Gross (Feb 10 2023 at 20:04):The message you saw (" ... setting stack size to the recommended minimum ...") indicates that it should be autosetting a large enough stack size, but you can try ulimit -S -s unlimited before building and see if that helps.
Karl Palmskog (Feb 10 2023 at 20:09):for the record, the Platform has a Mac M1/M2 binary installer, which I believe already contains fiat-crypto. And it's built from source via opam, so someone (presumably Michael Soegtrop) has gotten coq-fiat-crypto.0.0.17 to compile from scratch on M1/M2.
Paolo Giarrusso (Feb 10 2023 at 20:25):Potentially relevant: last I tried, the standard Docker images were only for x86_64, and they only run on Apple Silicon with high overhead (not Rosetta emulation, but much slower Qemu emulation)... But Docker 4.16 has opt-in beta Rosetta support https://github.com/docker/roadmap/issues/384#issuecomment-1377337935
Paolo Giarrusso (Feb 10 2023 at 20:26):Otherwise, I'd try Karl's suggestions.
Karl Palmskog (Feb 10 2023 at 20:26):doesn't opam work out-of-the-box on M1/M2? They say they have precompiled binaries.
Paolo Giarrusso (Feb 10 2023 at 20:26):Yes but the OP mentions Docker
Paolo Giarrusso (Feb 10 2023 at 20:27):I can use Docker x86-64 containers, but with something like a 3x-6x slowdown so I don't bother
Paolo Giarrusso (Feb 10 2023 at 20:28):But I hope to try the Rosetta thing soon
Karl Palmskog (Feb 10 2023 at 20:29):yeah, we use x86-64 + Debian for Docker since x86-64 Linux is the most common dev and CI environment, but Coq itself has or will soon have ongoing CI testing for M1.
Karl Palmskog (Feb 10 2023 at 20:30):and arm64 is to my knowledge tier 1 OCaml supported
Paolo Giarrusso (Feb 10 2023 at 20:31):@Tony Arcieri If you try again setting ulimit/environment variables, you should make sure they actually reach the container... Setting ulimit/env vars before calling Docker has no effect, so you'd have to do it inside the container and in the right way... You can open a shell in the container for development, or you can add those commands to a Dockerfile in the right way — each RUN line creates a different shell IIRC, so I think these settings won't persist across RUN directives.
Paolo Giarrusso (Feb 10 2023 at 20:33):@Karl Palmskog @Erik Martin-Dorel at some point it might be nice to have multi-arch Docker containers. But I agree x86 is still primary (and Rosetta support will decrease priority): my CI is x86-64 only after all
Karl Palmskog (Feb 10 2023 at 20:34):since we now have a co-maintainer with Erik for Docker-Coq, might be worth opening an issue about it. We were typically limited in the past by Erik's available bandwidth
Erik Martin-Dorel (Feb 10 2023 at 21:51):Yes, thanks.
Tony Arcieri (Feb 10 2023 at 22:11):Paolo Giarrusso said:
Tony Arcieri If you try again setting ulimit/environment variables, you should make sure they actually reach the container...
I was trying to do it via docker build --ulimit='stack=-1:-1' -t fiat . but I have no idea if that actually worked, guess I could try printing it
Tony Arcieri (Feb 10 2023 at 22:13):and yeah, using an x86_64 image on M2 is not ideal. I do have a server I can throw it on once I image it
Tony Arcieri (Feb 10 2023 at 22:15):really I'm just after the Rust 32-bit/64-bit output for the P-224 scalar field (and after that, the P-521 scalar field, and a more complete base field as well, though I imagine that might be a bit more difficult)
Jason Gross (Feb 10 2023 at 22:51):really I'm just after the Rust 32-bit/64-bit output for the P-224 scalar field
You can download prebuilt binaries (and the generated .ml files) from our CI for Ubuntu LTS at, e.g., https://github.com/mit-plv/fiat-crypto/actions/runs/4059752119 and for the GH Actions Coq dev docker image at, e.g., https://github.com/mit-plv/fiat-crypto/actions/runs/3814637541. (Take your pick of the OCaml binaries & source or the Haskell binaries & source, both should work fine.)
Jason Gross (Feb 10 2023 at 22:53):Mac OCaml binaries & source at e.g., https://github.com/mit-plv/fiat-crypto/actions/runs/4060043916
Windows at e.g., https://github.com/mit-plv/fiat-crypto/actions/runs/4059971104
Paolo Giarrusso (Feb 10 2023 at 23:48):Filed https://github.com/coq-community/docker-coq/issues/54
Tony Arcieri (Feb 11 2023 at 21:38):Karl Palmskog said:
This is on OCaml 4.14.1 and Coq 8.16.1:
$ opam install coq-fiat-crypto.0.0.17 ```` It's not working for me for some reason?$ opam install coq-fiat-crypto.0.0.17
[ERROR] No package named coq-fiat-crypto found.
Karl Palmskog (Feb 11 2023 at 21:39):@Tony Arcieri you need to first do:
opam repo add coq-released https://coq.inria.fr/opam/released
beware that the full build is quite memory-demanding, I had a 32GB machine that had to swap a bit
Tony Arcieri (Feb 11 2023 at 21:41):also on a 32GB machine, guess we'll see
Karl Palmskog (Feb 11 2023 at 21:43):I guess it also depends on how many jobs are used by opam, I think this can be controlled by OPAMJOBS variable or some other option
Tony Arcieri (Feb 11 2023 at 22:22):∗ installed coq-fiat-crypto.0.0.17
Done.
nice
Tony Arcieri (Feb 11 2023 at 22:28):and it works! or at least it output some Rust code roughly like what I was expecting
Tony Arcieri (Feb 11 2023 at 22:28):P-224 anyway. I'll see what happens when I try P-521 :wink:
Tony Arcieri (Feb 11 2023 at 23:28):Fatal error: exception Failure("Synthesis failed")
Jason Gross (Feb 12 2023 at 00:05):It should give you more of an error message than just that (possibly in the .rs file you're having it output to or whatever)
Tony Arcieri (Feb 12 2023 at 00:42):@Jason Gross oh, that particular one was trying to use word_by_word_montgomery when I guess I should be using unsaturated_solinas?
Tony Arcieri (Feb 12 2023 at 00:43):not sure what I should use for the scalar field exactly
Tony Arcieri (Feb 12 2023 at 14:55):oh, tried word_by_word_montgomery --lang Rust --inline p521_scalar 64 '0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409' mul square add sub opp nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp and that seems to have worked. Seems I'm good to go :tada:
Well, after I test this all and make sure I generated it correctly :sweat_smile:
Last updated: Oct 08 2024 at 14:01 UTC