Merge pull request #554 from hacspec/misc-ci-makefile-fixes

fix: misc fixes to Makefiles and Nix
hacspec · Mar 6, 2024 · 0753253 · 0753253
2 parents ee963ae + 902f784
commit 0753253
Show file tree

Hide file tree

Showing 6 changed files with 32 additions and 18 deletions.
diff --git a/examples/chacha20/proofs/fstar/extraction/Makefile b/examples/chacha20/proofs/fstar/extraction/Makefile
@@ -37,7 +37,7 @@ HACL_HOME      ?= $(HAX_HOME)/../../../hacl-star
 FSTAR_BIN      ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
 
 HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
-HAX_LIBS_HOME        ?= $(HAX_HOME)/hax-lib
+HAX_LIBS_HOME        ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction
 
 CACHE_DIR      ?= $(HAX_PROOF_LIBS_HOME)/.cache
 HINT_DIR       ?= $(HAX_PROOF_LIBS_HOME)/.hints
@@ -58,7 +58,7 @@ $(ROOTS): ../../../src/lib.rs ../../../src/hacspec_helper.rs
 FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \
 	$(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \
 	$(HAX_PROOF_LIBS_HOME)/hax_lib \
-	$(HAX_LIBS_HOME)/proofs/fstar/extraction
+	$(HAX_LIBS_HOME)
 
 FSTAR_FLAGS = --cmi \
   --warn_error -331 \

diff --git a/examples/limited-order-book/proofs/fstar/extraction/Makefile b/examples/limited-order-book/proofs/fstar/extraction/Makefile
@@ -37,7 +37,7 @@ HACL_HOME      ?= $(HAX_HOME)/../../../hacl-star
 FSTAR_BIN      ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
 
 HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
-HAX_LIBS_HOME        ?= $(HAX_HOME)/hax-lib
+HAX_LIBS_HOME        ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction
 
 CACHE_DIR      ?= $(HAX_PROOF_LIBS_HOME)/.cache
 HINT_DIR       ?= $(HAX_PROOF_LIBS_HOME)/.hints
@@ -58,7 +58,7 @@ $(ROOTS): ../../../src/canister.rs ../../../src/lib.rs
 FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \
 	$(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \
 	$(HAX_PROOF_LIBS_HOME)/hax_lib \
-	$(HAX_LIBS_HOME)/proofs/fstar/extraction
+	$(HAX_LIBS_HOME)
 
 FSTAR_FLAGS = --cmi \
   --warn_error -331 \

diff --git a/examples/sha256/proofs/fstar/extraction/Makefile b/examples/sha256/proofs/fstar/extraction/Makefile
@@ -37,7 +37,7 @@ HACL_HOME      ?= $(HAX_HOME)/../../../hacl-star
 FSTAR_BIN      ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
 
 HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
-HAX_LIBS_HOME        ?= $(HAX_HOME)/hax-lib
+HAX_LIBS_HOME        ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction
 
 CACHE_DIR      ?= $(HAX_PROOF_LIBS_HOME)/.cache
 HINT_DIR       ?= $(HAX_PROOF_LIBS_HOME)/.hints
@@ -58,7 +58,7 @@ $(ROOTS):
 FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \
 	$(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \
 	$(HAX_PROOF_LIBS_HOME)/hax_lib \
-	$(HAX_LIBS_HOME)/proofs/fstar/extraction
+	$(HAX_LIBS_HOME)
 
 FSTAR_FLAGS = --cmi \
   --warn_error -331 \

diff --git a/flake.nix b/flake.nix
@@ -43,7 +43,7 @@
         fstar = inputs.fstar.packages.${system}.default;
         hax-env-file = pkgs.writeText "hax-env-file" ''
           HAX_PROOF_LIBS_HOME="${./proof-libs/fstar}"
-          HAX_LIBS_HOME="${./hax-lib}"
+          HAX_LIBS_HOME="${./hax-lib}"/proofs/fstar/extraction
           HACL_HOME="${hacl-star}"
         '';
         hax-env = pkgs.writeScriptBin "hax-env" ''
@@ -151,8 +151,13 @@
         in {
           fstar = pkgs.mkShell {
             inherit inputsFrom LIBCLANG_PATH;
-            shellHook = "eval $(hax-env)";
-            packages = packages ++ [fstar hax-env];
+            HACL_HOME = "${hacl-star}";
+            shellHook = ''
+              HAX_ROOT=$(git rev-parse --show-toplevel)
+              export HAX_PROOF_LIBS_HOME="$HAX_ROOT/proof-libs/fstar"
+              export HAX_LIBS_HOME="$HAX_ROOT/hax-lib"
+            '';
+            packages = packages ++ [fstar];
           };
           default = pkgs.mkShell {
             inherit packages inputsFrom LIBCLANG_PATH;

diff --git a/proof-libs/fstar/core/Makefile b/proof-libs/fstar/core/Makefile
@@ -29,13 +29,17 @@
 # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
 #
 
-HAX_PROOF_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar
-FSTAR_HOME    ?= $(HAX_PROOF_LIBS_HOME)/../../../FStar
-HACL_HOME     ?= $(HAX_PROOF_LIBS_HOME)/../../../hacl-star
+
+HAX_HOME      ?= $(shell git rev-parse --show-toplevel)
+FSTAR_HOME    ?= $(HAX_LIBS_HOME)/../../../FStar
+HACL_HOME     ?= $(HAX_LIBS_HOME)/../../../hacl-star
 FSTAR_BIN     ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
 
-CACHE_DIR     ?= $(HAX_PROOF_LIBS_HOME)/.cache
-HINT_DIR      ?= $(HAX_PROOF_LIBS_HOME)/.hints
+HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
+HAX_LIBS_HOME       ?= $(HAX_HOME)/hax-lib
+
+CACHE_DIR     ?= ../core/.cache
+HINT_DIR      ?= ../core/.hints
 
 .PHONY: all verify clean
 
@@ -47,7 +51,8 @@ all:
 # *extend* the set of relevant files with the tests.
 ROOTS = $(wildcard *.fst)
 
-FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core $(HAX_PROOF_LIBS_HOME)/hax_lib
+FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core $(HAX_LIBS_HOME)/proofs/fstar/extraction/
+
 
 FSTAR_FLAGS = --cmi \
   --warn_error -331 \

diff --git a/proof-libs/fstar/rust_primitives/Makefile b/proof-libs/fstar/rust_primitives/Makefile
@@ -6,7 +6,8 @@
 #
 # We expect FSTAR_HOME to be set to your FSTAR repo/install directory
 # We expect HACL_HOME to be set to your HACL* repo location
-# We expect HAX_LIBS_HOME to be set to the folder containing core, rust_primitives etc.
+# We expect HAX_PROOF_LIBS_HOME to be set to the folder containing core, rust_primitives etc.
+# We expect HAX_LIBS_HOME to be set to the hax-lib folder
 #
 # ROOTS contains all the top-level F* files you wish to verify
 # The default target `verify` verified ROOTS and its dependencies
@@ -29,11 +30,14 @@
 # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
 #
 
-HAX_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar
+HAX_HOME      ?= $(shell git rev-parse --show-toplevel)
 FSTAR_HOME    ?= $(HAX_LIBS_HOME)/../../../FStar
 HACL_HOME     ?= $(HAX_LIBS_HOME)/../../../hacl-star
 FSTAR_BIN     ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
 
+HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
+HAX_LIBS_HOME       ?= $(HAX_HOME)/hax-lib
+
 CACHE_DIR     ?= $(HAX_LIBS_HOME)/.cache
 HINT_DIR      ?= $(HAX_LIBS_HOME)/.hints
 
@@ -47,7 +51,7 @@ all:
 # *extend* the set of relevant files with the tests.
 ROOTS = $(wildcard *.fst)
 
-FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_LIBS_HOME)/rust_primitives $(HAX_LIBS_HOME)/core $(HAX_LIBS_HOME)/hax_lib
+FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core $(HAX_LIBS_HOME)/proofs/fstar/extraction/
 
 FSTAR_FLAGS = --cmi \
   --warn_error -331 \