From 67e1f695de60537e6d26cfb530dc7e52ab91f482 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 28 Feb 2024 16:59:41 +0100 Subject: [PATCH] fix(f* makefiles): uniformize env vars names This commit renames remaining occurences `HAX_PROOF_LIBS` into `HAX_PROOF_LIBS_HOME` and `HAX_LIB` into `HAX_LIBS_HOME`. --- .../chacha20/proofs/fstar/extraction/Makefile | 18 +++++++++--------- .../proofs/fstar/extraction/Makefile | 18 +++++++++--------- .../sha256/proofs/fstar/extraction/Makefile | 18 +++++++++--------- flake.nix | 4 ++-- 4 files changed, 29 insertions(+), 29 deletions(-) diff --git a/examples/chacha20/proofs/fstar/extraction/Makefile b/examples/chacha20/proofs/fstar/extraction/Makefile index 7c3be1f31..d2ea0bd48 100644 --- a/examples/chacha20/proofs/fstar/extraction/Makefile +++ b/examples/chacha20/proofs/fstar/extraction/Makefile @@ -6,8 +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_PROOF_LIBS to be set to the folder containing core, rust_primitives etc. -# We expect HAX_LIB to be set to the folder containing the crate `hax-lib`. +# 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 folder containing the crate `hax-lib`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies @@ -36,11 +36,11 @@ 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 ?= $(HAX_HOME)/proof-libs/fstar -HAX_LIB ?= $(HAX_HOME)/hax-lib +HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar +HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib -CACHE_DIR ?= $(HAX_PROOF_LIBS)/.cache -HINT_DIR ?= $(HAX_PROOF_LIBS)/.hints +CACHE_DIR ?= $(HAX_PROOF_LIBS_HOME)/.cache +HINT_DIR ?= $(HAX_PROOF_LIBS_HOME)/.hints .PHONY: all verify clean @@ -56,9 +56,9 @@ $(ROOTS): ../../../src/lib.rs ../../../src/hacspec_helper.rs cargo hax into fstar FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \ - $(HAX_PROOF_LIBS)/rust_primitives $(HAX_PROOF_LIBS)/core \ - $(HAX_PROOF_LIBS)/hax_lib \ - $(HAX_LIB)/proofs/fstar/extraction + $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \ + $(HAX_PROOF_LIBS_HOME)/hax_lib \ + $(HAX_LIBS_HOME)/proofs/fstar/extraction 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 index 5ca2d00e4..d199aabc1 100644 --- a/examples/limited-order-book/proofs/fstar/extraction/Makefile +++ b/examples/limited-order-book/proofs/fstar/extraction/Makefile @@ -6,8 +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_PROOF_LIBS to be set to the folder containing core, rust_primitives etc. -# We expect HAX_LIB to be set to the folder containing the crate `hax-lib`. +# 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 folder containing the crate `hax-lib`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies @@ -36,11 +36,11 @@ 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 ?= $(HAX_HOME)/proof-libs/fstar -HAX_LIB ?= $(HAX_HOME)/hax-lib +HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar +HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib -CACHE_DIR ?= $(HAX_PROOF_LIBS)/.cache -HINT_DIR ?= $(HAX_PROOF_LIBS)/.hints +CACHE_DIR ?= $(HAX_PROOF_LIBS_HOME)/.cache +HINT_DIR ?= $(HAX_PROOF_LIBS_HOME)/.hints .PHONY: all verify clean @@ -56,9 +56,9 @@ $(ROOTS): ../../../src/canister.rs ../../../src/lib.rs cargo hax into -i '-** +**::process_order' fstar FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \ - $(HAX_PROOF_LIBS)/rust_primitives $(HAX_PROOF_LIBS)/core \ - $(HAX_PROOF_LIBS)/hax_lib \ - $(HAX_LIB)/proofs/fstar/extraction + $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \ + $(HAX_PROOF_LIBS_HOME)/hax_lib \ + $(HAX_LIBS_HOME)/proofs/fstar/extraction FSTAR_FLAGS = --cmi \ --warn_error -331 \ diff --git a/examples/sha256/proofs/fstar/extraction/Makefile b/examples/sha256/proofs/fstar/extraction/Makefile index c677ceb78..04ce42e4c 100644 --- a/examples/sha256/proofs/fstar/extraction/Makefile +++ b/examples/sha256/proofs/fstar/extraction/Makefile @@ -6,8 +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_PROOF_LIBS to be set to the folder containing core, rust_primitives etc. -# We expect HAX_LIB to be set to the folder containing the crate `hax-lib`. +# 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 folder containing the crate `hax-lib`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies @@ -36,11 +36,11 @@ 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 ?= $(HAX_HOME)/proof-libs/fstar -HAX_LIB ?= $(HAX_HOME)/hax-lib +HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar +HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib -CACHE_DIR ?= $(HAX_PROOF_LIBS)/.cache -HINT_DIR ?= $(HAX_PROOF_LIBS)/.hints +CACHE_DIR ?= $(HAX_PROOF_LIBS_HOME)/.cache +HINT_DIR ?= $(HAX_PROOF_LIBS_HOME)/.hints .PHONY: all verify clean @@ -56,9 +56,9 @@ $(ROOTS): cargo hax into fstar FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \ - $(HAX_PROOF_LIBS)/rust_primitives $(HAX_PROOF_LIBS)/core \ - $(HAX_PROOF_LIBS)/hax_lib \ - $(HAX_LIB)/proofs/fstar/extraction + $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \ + $(HAX_PROOF_LIBS_HOME)/hax_lib \ + $(HAX_LIBS_HOME)/proofs/fstar/extraction FSTAR_FLAGS = --cmi \ --warn_error -331 \ diff --git a/flake.nix b/flake.nix index 191a9dec5..7f0e5419f 100644 --- a/flake.nix +++ b/flake.nix @@ -42,8 +42,8 @@ rustfmt = pkgs.rustfmt; fstar = inputs.fstar.packages.${system}.default; hax-env-file = pkgs.writeText "hax-env-file" '' - HAX_PROOF_LIBS="${./proof-libs/fstar}" - HAX_LIB="${./hax-lib}" + HAX_PROOF_LIBS_HOME="${./proof-libs/fstar}" + HAX_LIBS_HOME="${./hax-lib}" HACL_HOME="${hacl-star}" ''; hax-env = pkgs.writeScriptBin "hax-env" ''