Add dependencies for Alectryon documentation

Update README on the status of Vericert

5 files changed, 15 insertions, 9 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: <a href="https://vericert.ymhg.org"><img src="https://vericert.ymhg.org/vericert-main.svg" width="100%" height="144" /></a>
 
 #+html: <p align=center><a href="https://github.com/ymherklotz/vericert/actions"><img src="https://github.com/ymherklotz/vericert/workflows/CI/badge.svg" /></a>&nbsp;<a href="https://vericert.ymhg.org/"><img src="https://github.com/ymherklotz/vericert-docs/workflows/docs/badge.svg" /></a></p>
@@ -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
-Subproject 5508c21e064276aa4d5146b3af5b6f6e9a4c236
+Subproject 42e19f2b20c907505a28486a8071147ed6c610f
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