-
Notifications
You must be signed in to change notification settings - Fork 55
Installation instructions
TL;DR: Run nix-env -iA nixpkgs.jasmin-compiler
(more info about the nix package manager), or run opam install jasmin
(more info about the opam package manager).
The Jasmin compiler is written in Coq and OCaml. It is built in two steps: OCaml code is first extracted from the Coq code then compiled together with the hand-written OCaml code.
If you are not interested in using the Coq formalization, you may skip the first step below.
Get the source code from the git repository hosted on https://github.com/jasmin-lang/jasmin/,
for instance the current version of the main
branch:
jasmin-main.tar.gz.
The exact set of dependencies can be found in the default.nix
file at the root of the git repository.
- Coq at version 8.19
- The Mathematical Components library, at version 2.2 (only the following sub-libraries are required: ssreflect, fingroup, algebra)
- The mathcomp-word library, at version 3.2
Once all dependencies are available (which can be achieved by running nix-shell
at the root directory),
change to the proof
directory and run make
Change to the compiler
directory and run make CIL
Get the full OCaml source code, either as a result of the extraction process described above, or from the jasmin-compiler repository,
for instance the current version of the main
branch:
jasmin-compiler.tar.gz
The precise set of dependencies can be found in the default.nix
file.
- OCaml at version 4.14, with the following tools and libraries: menhir, menhirLib, dune, findlib (aka ocamlfind), apron, camlidl, batteries, cmdliner, zarith, yojson.
- MPFR
- PPL
Once all dependencies are available (which can be achieved by running nix-shell
, either at the root of the source tree — if there is a default.nix
file there — or within the compiler
directory),
change to the compiler
directory (at the root of the source tree, not inside the proof
directory), and run make
.
This produces a jasminc
program (a symbolic link to the actual binary file, that might be moved to a different path; that program is dynamically linked to a few libraries: apron, mpfr, ppl, etc.).