diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-04-03 12:05:23 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-04-03 12:05:23 +0100 |
commit | 2410baab447328e7134afb93ee9625b44a8b8cf2 (patch) | |
tree | 098d912a7a4bad56e34056baa6dc13cea76a2bc7 | |
parent | 1cdf3b8257d1fbd1ba0bff67656163ae3f153774 (diff) | |
download | vericert-2410baab447328e7134afb93ee9625b44a8b8cf2.tar.gz vericert-2410baab447328e7134afb93ee9625b44a8b8cf2.zip |
Update the readmev0.1.0
-rw-r--r-- | README.md | 48 |
1 files changed, 47 insertions, 1 deletions
@@ -1,3 +1,49 @@ # Coqup -A formally verified HLS tool in Coq. +A formally verified HLS tool in Coq, building on top of [CompCert](https://github.com/AbsInt/CompCert). + +## Building + +To build coqup, the provided [Makefile](/Makefile) can be used. External dependencies are needed to build the project, which can be pulled in automatically with [nix](https://nixos.org/nix/) using the provided [default.nix](/default.nix) and [shell.nix](/shell.nix) files. + +The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following: + +- [Coq](https://coq.inria.fr/): theorem prover that is used to also program the HLS tool. +- [OCaml](https://ocaml.org/): the OCaml compiler to compile the extracted files. +- [bbv](https://github.com/mit-plv/bbv): an efficient bit vector library. +- [dune](https://github.com/ocaml/dune): build tool for ocaml projects to gather all the ocaml files and compile them in the right order. +- [menhir](http://gallium.inria.fr/~fpottier/menhir/): parser generator for ocaml. +- [findlib](https://github.com/ocaml/ocamlfind) to find installed OCaml libraries. +- [GCC](https://gcc.gnu.org/): compiler to help build CompCert. + +These dependencies can be installed manually, or automatically through Nix. + +### Setting up Nix + +Nix is a package manager that can create an isolated environment so that the builds are reproducible. Once nix is installed, it can be used in the following way. + +To just build the project once, the following command can be executed. + +``` shell +nix-build +``` + +The output will then be in `results/bin/coqup`. + +To open a shell which includes all the necessary dependencies instead, one can use: + +``` shell +nix-shell +``` + +which will open a shell that has all the dependencies loaded. + +### Makefile build + +If the dependencies were installed manually, or if one is in the `nix-shell`, the project can be built by running: + +``` shell +make +``` + +Which will install the binary in `./bin/coqup` by default. However, this can be changed by changing the `PREFIX` environment variable, in which case the binary will be installed in `$PREFIX/bin/coqup`. |