From ac9c30114c5aa84370f4067780501d529df19601 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas.franceschino@inria.fr>
Date: Tue, 6 Feb 2024 09:47:45 +0100
Subject: [PATCH] fix(fstar/makefile): use common HAX variables

---
 proofs/fstar/extraction/Makefile | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/proofs/fstar/extraction/Makefile b/proofs/fstar/extraction/Makefile
index be8c41e0..5a5432f6 100644
--- a/proofs/fstar/extraction/Makefile
+++ b/proofs/fstar/extraction/Makefile
@@ -29,13 +29,18 @@
 # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
 #
 
-HAX_HOME      ?= $(shell git rev-parse --show-toplevel)/../hax/proof-libs/fstar
-FSTAR_HOME    ?= $(HAX_HOME)../FStar
-HACL_HOME     ?= $(HAX_HOME)../hacl-star
+WORKSPACE_ROOT ?= $(shell git rev-parse --show-toplevel)/..
+
+HAX_HOME            ?= $(WORKSPACE_ROOT)/hax
+HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
+HAX_LIBS_HOME       ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction
+
+FSTAR_HOME    ?= $(WORKSPACE_ROOT)/FStar
+HACL_HOME     ?= $(WORKSPACE_ROOT)/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_HOME)proof-libs/fstar/.cache
-HINT_DIR      ?= $(HAX_HOME)proof-libs/fstar/.hints
+CACHE_DIR     ?= .cache
+HINT_DIR      ?= .hints
 
 .PHONY: all verify clean
 
@@ -47,8 +52,9 @@ all:
 # *extend* the set of relevant files with the tests.
 ROOTS = $(wildcard *.fst)
 
-FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_HOME)/proof-libs/fstar/rust_primitives \
-	$(HAX_HOME)/proof-libs/fstar/core $(HAX_HOME)/proof-libs/fstar/hax_lib
+
+
+FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core $(HAX_LIBS_HOME)
 
 FSTAR_FLAGS = --cmi \
   --warn_error -331 \