From ae185063d204752d12e76609e60d69819d63ada8 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 27 Sep 2021 01:17:32 +0100 Subject: Export without title --- README.org | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.org b/README.org index 4426561..368804f 100644 --- a/README.org +++ b/README.org @@ -1,3 +1,5 @@ +#+options: title:nil + #+html: #+html:

 

-- cgit From 26fbe3803507fb95f658a888cb225a298644a77b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 27 Sep 2021 18:14:33 +0100 Subject: Add empty title --- README.org | 2 ++ docs | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/README.org b/README.org index 4426561..e899bde 100644 --- a/README.org +++ b/README.org @@ -1,3 +1,5 @@ +#+title: + #+html: #+html:

 

diff --git a/docs b/docs index 5508c21..42e19f2 160000 --- a/docs +++ b/docs @@ -1 +1 @@ -Subproject commit 5508c21e064276aa4d5146b3af5b6f6e9a4c2364 +Subproject commit 42e19f2b20c907505a28486a8071147ed6c610fb -- cgit From d7a08d9b3523aadc10b0d32baa6ec2d8508ef9a3 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 27 Sep 2021 20:12:21 +0100 Subject: Update README on the status of Vericert --- README.org | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.org b/README.org index e899bde..faee0cc 100644 --- a/README.org +++ b/README.org @@ -13,8 +13,8 @@ correctness. :PROPERTIES: :CUSTOM_ID: features :END: -The project is currently a work in progress, so proofs remain to be finished. Currently, the -following C features are supported, but are not all proven correct yet: + +Currently all proofs of the following features have been completed. - all int operations, - non-recursive function calls, -- cgit From 4b3457be6581a6ff280898fb45790621870d6882 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 29 Sep 2021 22:01:58 +0100 Subject: Update docs --- docs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs b/docs index 5508c21..42e19f2 160000 --- a/docs +++ b/docs @@ -1 +1 @@ -Subproject commit 5508c21e064276aa4d5146b3af5b6f6e9a4c2364 +Subproject commit 42e19f2b20c907505a28486a8071147ed6c610fb -- cgit From 1b36d45f27c450a6006241e1b48bbc36107f4464 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 1 Oct 2021 19:39:46 +0100 Subject: Update Changelog with 1.2.2 release --- CHANGELOG.org | 5 +++++ 1 file changed, 5 insertions(+) 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. -- cgit From 1cb470d7b34a6e4fba73e0c57e51c44a220912bb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 1 Oct 2021 19:42:17 +0100 Subject: Fix citation file and README --- CITATION.cff | 4 ++-- README.org | 1 - 2 files changed, 2 insertions(+), 3 deletions(-) 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..09e2968 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. -- cgit From 0b6938e44cde14ed66e6b7af943d3176b5c559cd Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 1 Oct 2021 20:11:17 +0100 Subject: Update README with checkout instructions --- README.org | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/README.org b/README.org index 09e2968..cf8bd34 100644 --- a/README.org +++ b/README.org @@ -42,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 @@ -71,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. @@ -84,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: @@ -104,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 -- cgit From bd26d2ee3a8fabefbff50de6c53549399f2b7762 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 1 Oct 2021 20:35:48 +0100 Subject: Add menhirLib as an explicit dependency --- default.nix | 1 + 1 file changed, 1 insertion(+) 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 -- cgit