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.
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.
Which hw architecture and OCaml version are you using?
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)
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-bedrock220.127.116.11 ∗ 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.
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
I'll give that a try
(I'm on x86_64 though, no idea if M2 makes a difference)
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.
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.
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
Otherwise, I'd try Karl's suggestions.
doesn't opam work out-of-the-box on M1/M2? They say they have precompiled binaries.
Yes but the OP mentions Docker
I can use Docker x86-64 containers, but with something like a 3x-6x slowdown so I don't bother
But I hope to try the Rosetta thing soon
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.
and arm64 is to my knowledge tier 1 OCaml supported
@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.
@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
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
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
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
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)
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.)
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
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.
@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
also on a 32GB machine, guess we'll see
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
∗ installed coq-fiat-crypto.0.0.17 Done.
and it works! or at least it output some Rust code roughly like what I was expecting
P-224 anyway. I'll see what happens when I try P-521 :wink:
Fatal error: exception Failure("Synthesis failed")
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)
@Jason Gross oh, that particular one was trying to use
word_by_word_montgomery when I guess I should be using
not sure what I should use for the scalar field exactly
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: Dec 01 2023 at 06:01 UTC