Merge branch 'master' into dev/scheduling

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
diff --git a/README.org b/README.org
index faee0cc..cf8bd34 100644
--- a/README.org
+++ b/README.org
@@ -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