From fee6cb39590969adafa18eee9f4b4f30e9213b99 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Wed, 16 Oct 2024 10:47:55 -0700
Subject: [PATCH] Makefile: simplifying F* detection (of library, ocaml files,
 etc)

---
 Makefile        |  2 +-
 Makefile.common | 32 +++++++-------------------------
 locate_fstar.mk | 27 +++++++++++++++++++++++++++
 3 files changed, 35 insertions(+), 26 deletions(-)
 create mode 100644 locate_fstar.mk

diff --git a/Makefile b/Makefile
index 1e19521bfa..041d32b560 100644
--- a/Makefile
+++ b/Makefile
@@ -1034,7 +1034,7 @@ obj/libhaclml.cmxa: $(filter-out $(HACL_HOME)/obj/Meta_Interface.cmx,$(ALL_CMX_F
 # JP: doesn't work because a PPX is prepended for some reason
 # ocamlfind mklib -o haclml -package fstar.lib -g -I $(HACL_HOME)/obj $(addprefix $(HACL_HOME)/obj/*.,cmo cmx ml o)
 	$(call run-with-log,\
-	  OCAMLFIND_IGNORE_DUPS_IN="`ocamlc -where`/compiler-libs" ocamlfind opt -thread -a -o $@ -package fstar.lib -g -I $(HACL_HOME)/obj $^ \
+	  OCAMLFIND_IGNORE_DUPS_IN="`ocamlc -where`/compiler-libs" $(FSTAR_EXE) --ocamlenv ocamlfind opt -thread -a -o $@ -package fstar.lib -g -I $(HACL_HOME)/obj $^ \
 	  ,[OCAMLOPT-CMXA] libhaclml,$(call to-obj-dir,$@))
 
 
diff --git a/Makefile.common b/Makefile.common
index a5ff71c1fb..54495539c3 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -21,31 +21,19 @@ ifndef KRML_HOME
 KRML_HOME 	:= $(HACL_HOME)/../karamel
 endif
 
-ifndef FSTAR_HOME
-  FSTAR_EXE=$(shell which fstar.exe)
-  ifeq ($(FSTAR_EXE),)
-    # F* not found in PATH, assuming an Everest source tree
-    FSTAR_HOME := $(HACL_HOME)/../FStar
-  else
-    # F* found in PATH, assuming directory name ends with /bin
-    FSTAR_HOME := $(dir $(FSTAR_EXE))/..
-  endif
-endif
-
-FSTAR_EXE := $(FSTAR_HOME)/bin/fstar.exe
+include locate_fstar.mk
 
 # Check that the relevant homes and executables at least exist.
 mustexist =						\
   $(if $(wildcard $(value $(strip $1))),,		\
     $(error $1 ($(value $(strip $1))) does not exist))
 
-$(call mustexist, FSTAR_HOME)
+# $(call mustexist, FSTAR_HOME)
+# ^ No longer needed, we just need the .exe
 $(call mustexist, FSTAR_EXE)
 $(call mustexist, KRML_HOME)
 
-ifndef FSTAR_ULIB
-FSTAR_ULIB := $(shell if test -d "$(FSTAR_HOME)/ulib" ; then echo "$(FSTAR_HOME)/ulib" ; else echo "$(FSTAR_HOME)/lib/fstar" ; fi)
-endif
+FSTAR_ULIB := $(shell $(FSTAR_EXE) --locate_lib)
 
 ifndef VALE_HOME
 # assuming an Everest source tree
@@ -67,7 +55,6 @@ sanitize_path=$(call maybe_cygpath,$(realpath $(1)))
 
 HACL_HOME := $(call sanitize_path,$(HACL_HOME))
 KRML_HOME := $(call sanitize_path,$(KRML_HOME))
-FSTAR_HOME := $(call sanitize_path,$(FSTAR_HOME))
 FSTAR_ULIB := $(call sanitize_path,$(FSTAR_ULIB))
 VALE_HOME := $(call sanitize_path,$(VALE_HOME))
 
@@ -243,14 +230,9 @@ TAC = $(shell which tac >/dev/null 2>&1 && echo "tac" || echo "tail -r")
 
 ALL_CMX_FILES = $(subst obj/Lib_Buffer.cmx,obj/Lib_Memzero0.cmx obj/Lib_Buffer.cmx,$(patsubst %.ml,%.cmx,$(shell echo $(ALL_ML_FILES) | $(TAC))))
 
-ifeq ($(OS),Windows_NT)
-  export OCAMLPATH := $(FSTAR_HOME)/lib;$(OCAMLPATH)
-else
-  export OCAMLPATH := $(FSTAR_HOME)/lib:$(OCAMLPATH)
-endif
-
 # Warning 8: this pattern-matching is not exhaustive.
 # Warning 20: this argument will not be used by the function.
 # Warning 26: unused variable
-OCAMLOPT = OCAMLFIND_IGNORE_DUPS_IN="`ocamlc -where`/compiler-libs" ocamlfind opt -package fstar.lib -linkpkg -thread -g -I $(HACL_HOME)/obj -w -8-20-26
-OCAMLSHARED = OCAMLFIND_IGNORE_DUPS_IN="`ocamlc -where`/compiler-libs" ocamlfind opt -shared -package fstar.lib -thread -g -I $(HACL_HOME)/obj -w -8-20-26
+export OCAMLFIND_IGNORE_DUPS_IN="`ocamlc -where`/compiler-libs"
+OCAMLOPT = $(FSTAR_EXE) --ocamlenv ocamlfind opt -package fstar.lib -linkpkg -thread -g -I $(HACL_HOME)/obj -w -8-20-26
+OCAMLSHARED = $(FSTAR_EXE) --ocamlenv ocamlfind opt -shared -package fstar.lib -thread -g -I $(HACL_HOME)/obj -w -8-20-26
diff --git a/locate_fstar.mk b/locate_fstar.mk
new file mode 100644
index 0000000000..d33d1185c5
--- /dev/null
+++ b/locate_fstar.mk
@@ -0,0 +1,27 @@
+# Find fstar.exe and set FSTAR_EXE to its absolute path.
+
+# If FSTAR_EXE is already externally set, we just use it. Note the use
+# of ?= everywhere below.
+
+# If FSTAR_HOME is set, we honor it and pick that F*.
+ifdef FSTAR_HOME
+FSTAR_EXE ?= $(abspath $(FSTAR_HOME)/bin/fstar.exe)
+endif
+
+# Otherwise we try to find it from the PATH.
+
+# Bash's 'type -P' is essentially 'which'. This relies on having bash
+# around, but does not require 'which'.
+FSTAR_EXE ?= $(shell bash -c 'type -P fstar.exe')
+
+# Force eval
+FSTAR_EXE := $(FSTAR_EXE)
+
+# Don't fail if we're cleaning
+ifneq ($(MAKECMDGOALS),clean)
+ifeq (,$(FSTAR_EXE))
+  $(error "Did not find fstar.exe in PATH and FSTAR_EXE/FSTAR_HOME unset, aborting.")
+endif
+endif
+
+export FSTAR_EXE