From 02ca043e9c2d2aec31aec5a323535924a4414696 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 27 Sep 2021 18:14:33 +0100 Subject: Add dependencies for Alectryon documentation Update README on the status of Vericert --- README.org | 6 ++++-- default.nix | 6 +++++- docs | 2 +- src/extraction/Extraction.v | 8 ++++---- src/hls/Sat.v | 4 ++-- 5 files changed, 16 insertions(+), 10 deletions(-) diff --git a/README.org b/README.org index 4426561..faee0cc 100644 --- a/README.org +++ b/README.org @@ -1,3 +1,5 @@ +#+title: + #+html: #+html:

 

@@ -11,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, diff --git a/default.nix b/default.nix index 1121469..fa60637 100644 --- a/default.nix +++ b/default.nix @@ -1,4 +1,4 @@ -with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/8dd8bd8be74879f9f7919b16a4cb5ab2a75f18e5.tar.gz") {}; +with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/1a56d76d718afb6c47dd96602c915b6d23f7c45d.tar.gz") {}; let ncoq = coq_8_13; ncoqPackages = coqPackages_8_13; @@ -10,6 +10,10 @@ stdenv.mkDerivation { buildInputs = [ ncoq dune_2 gcc ncoq.ocaml ncoq.ocamlPackages.findlib ncoq.ocamlPackages.menhir ncoq.ocamlPackages.ocamlgraph + ncoqPackages.serapi + python3 python3Packages.docutils python3Packages.pygments + python3Packages.dominate + python3Packages.pelican ]; enableParallelBuilding = true; diff --git a/docs b/docs index 5508c21..42e19f2 160000 --- a/docs +++ b/docs @@ -1 +1 @@ -Subproject commit 5508c21e064276aa4d5146b3af5b6f6e9a4c2364 +Subproject commit 42e19f2b20c907505a28486a8071147ed6c610fb diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 6abe4e0..6bbfc05 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -179,7 +179,7 @@ Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". Extract Constant Pipeline.pipeline => "SoftwarePipelining.pipeline". Extract Constant RTLBlockgen.partition => "Partition.partition". -(*Extract Constant RTLPargen.schedule => "Schedule.schedule_fn".*) +Extract Constant RTLPargen.schedule => "Schedule.schedule_fn". (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. @@ -187,11 +187,11 @@ Set Extraction AccessOpaque. Cd "src/extraction". Separate Extraction Verilog.module vericert.Compiler.transf_hls -(* vericert.Compiler.transf_hls_temp*) -(* RTLBlockgen.transl_program RTLBlockInstr.successors_instr*) + vericert.Compiler.transf_hls_temp + RTLBlockgen.transl_program RTLBlockInstr.successors_instr HTLgen.tbl_to_case_expr Pipeline.pipeline -(* RTLBlockInstr.sat_pred_temp*) + RTLBlockInstr.sat_pred_simple Verilog.stmnt_to_list Compiler.transf_c_program Compiler.transf_cminor_program diff --git a/src/hls/Sat.v b/src/hls/Sat.v index 9549947..679f5ec 100644 --- a/src/hls/Sat.v +++ b/src/hls/Sat.v @@ -202,9 +202,9 @@ Local Hint Resolve satLit_contra : core. obligations that it can't solve, or obligations that it takes 42 years to solve. However, if you think enough like me, each of the four definitions you fill in - should read like: [[ + should read like: refine some_expression_with_holes; clear function_name; magic_solver. -]] leaving out the [clear] invocation for non-recursive function definitions. + leaving out the [clear] invocation for non-recursive function definitions. *) Ltac magic_solver := simpl; intros; subst; intuition eauto; firstorder; match goal with -- cgit