Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

redistributable binaries #1250

Open
JasonGross opened this issue May 20, 2022 · 4 comments
Open

redistributable binaries #1250

JasonGross opened this issue May 20, 2022 · 4 comments

Comments

@JasonGross
Copy link
Collaborator

It would be nice to build statically-linked portable binaries for Windows, Mac, and Linux (c.f. this blog post, for example), and include them, as well as the generated OCaml source code and a simple make/dune file, with releases. Presumably these binaries should support bedrock2, but, unlike the current bedrock2 binaries, should default to C.

JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue May 22, 2022
This is in preparation for mit-plv#1250.  We generate `with_bedrock2_*`
binaries which support bedrock2 output but default to C.  We also
install these by default when we are installing with bedrock2 enabled.
These will be the source files that we want to package up into source
releases of our generated code, as well as the source we use for
generating statically-linked redistributable binaries.
JasonGross added a commit that referenced this issue May 22, 2022
This is in preparation for #1250.  We generate `with_bedrock2_*`
binaries which support bedrock2 output but default to C.  We also
install these by default when we are installing with bedrock2 enabled.
These will be the source files that we want to package up into source
releases of our generated code, as well as the source we use for
generating statically-linked redistributable binaries.
@armfazh
Copy link
Contributor

armfazh commented Sep 13, 2023

At least a Docker image published in docker hub.

@JasonGross
Copy link
Collaborator Author

At least a Docker image published in docker hub.

This should be doable. MathComp automatically publishes docker images on top of Coq, maybe we can do the same (just opam install coq-fiat-crypto on top of the Coq docker images, copy math-comp infrastructure to publish)

@andres-erbsen
Copy link
Contributor

andres-erbsen commented Sep 14, 2023

Do you really want to maintain this, though? I would much rather spend my time learning how to statically link ocaml than dealing with docker and deployment automation.

@armfazh
Copy link
Contributor

armfazh commented Sep 23, 2023

Docker is known to be a painful experience, but these days is more stable.

The docker image I have in mind is one that contains the executables produced during extraction, e.g. word_by_word_montgomery, unsaturated_solinas, etc.
Thus, a user can only execute:

$ docker pull fiat-crypto
$ docker run <docker-params> fiat-crypto word_by_word_montgomery <params>

To build this image, it requires first to compile fiat-crypto in a builder image, which can be done in Github/CI
The second step is copying only the binaries in the distribution image. And then just publish this image to docker hub.

All these steps can be triggered only when a new version is released.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants