diff options
-rw-r--r-- | CHANGELOG.org | 5 | ||||
-rw-r--r-- | CITATION.cff | 4 | ||||
-rw-r--r-- | README.org | 23 | ||||
-rw-r--r-- | default.nix | 1 |
4 files changed, 20 insertions, 13 deletions
diff --git a/CHANGELOG.org b/CHANGELOG.org index af5e771..66f754d 100644 --- a/CHANGELOG.org +++ b/CHANGELOG.org @@ -12,6 +12,11 @@ - Add *RTLPar*, which can execute groups of instructions in parallel. - Add scheduling pass to go from RTLBlock to RTLPar. +* 2021-10-01 - v1.2.2 + +Mainly fix some documentation and remove any ~Admitted~ theorems, even though +these were in parts of the compiler that were never used. + * 2021-07-12 - v1.2.1 Main release for OOPSLA'21 paper. diff --git a/CITATION.cff b/CITATION.cff index 9328474..c114ec6 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -15,9 +15,9 @@ authors: given-names: "John" orcid: "https://orcid.org/0000-0001-6735-5533" title: "Vericert" -version: 1.2.1 +version: 1.2.2 doi: 10.5281/zenodo.5093839 -date-released: 2021-07-12 +date-released: 2021-10-01 url: "https://github.com/ymherklotz/vericert" preferred-citation: type: article @@ -34,7 +34,6 @@ compiled and executed. The dependencies of this project are the following: - [[https://coq.inria.fr/][Coq]]: theorem prover that is used to also program the HLS tool. - [[https://ocaml.org/][OCaml]]: the OCaml compiler to compile the extracted files. -- [[https://github.com/mit-plv/bbv][bbv]]: an efficient bit vector library. - [[https://github.com/ocaml/dune][dune]]: build tool for ocaml projects to gather all the ocaml files and compile them in the right order. - [[http://gallium.inria.fr/~fpottier/menhir/][menhir]]: parser generator for ocaml. @@ -43,23 +42,25 @@ compiled and executed. The dependencies of this project are the following: These dependencies can be installed manually, or automatically through Nix. -*** Downloading CompCert +*** Downloading Vericert and CompCert :PROPERTIES: :CUSTOM_ID: downloading-compcert :END: CompCert is added as a submodule in the =lib/CompCert= directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded -together with the repository. To clone CompCert together with this project, you can run: +together with the repository. To clone CompCert together with this project, and check it out at the +correct revision, you can run: #+begin_src shell - git clone --recursive https://github.com/ymherklotz/vericert +git clone -b v1.2.2 --recursive https://github.com/ymherklotz/vericert #+end_src If the repository is already cloned, you can run the following command to make sure that CompCert is -also downloaded: +also downloaded and the correct branch is checked out: #+begin_src shell - git submodule update --init +git checkout v1.2.2 +git submodule update --init #+end_src *** Setting up Nix @@ -72,7 +73,7 @@ reproducible. Once nix is installed, it can be used in the following way. To open a shell which includes all the necessary dependencies, one can use: #+begin_src shell - nix-shell +nix-shell #+end_src which will open a shell that has all the dependencies loaded. @@ -85,7 +86,7 @@ If the dependencies were installed manually, or if one is in the =nix-shell=, th by running: #+begin_src shell - make -j8 +make -j8 #+end_src and installed locally, or under the =PREFIX= location using: @@ -105,9 +106,9 @@ To test out =vericert= you can try the following examples which are in the test following: #+begin_src shell - ./bin/vericert test/loop.c -o loop.v - ./bin/vericert test/conditional.c -o conditional.v - ./bin/vericert test/add.c -o add.v +./bin/vericert test/loop.c -o loop.v +./bin/vericert test/conditional.c -o conditional.v +./bin/vericert test/add.c -o add.v #+end_src ** Citation diff --git a/default.nix b/default.nix index 0e5b40d..6350e3e 100644 --- a/default.nix +++ b/default.nix @@ -10,6 +10,7 @@ stdenv.mkDerivation { buildInputs = [ ncoq dune_2 gcc ncoq.ocaml ncoq.ocamlPackages.findlib ncoq.ocamlPackages.menhir ncoq.ocamlPackages.ocamlgraph ncoq.ocamlPackages.merlin + ncoq.ocamlPackages.menhirLib ncoqPackages.serapi python3 python3Packages.docutils python3Packages.pygments |