Merge remote-tracking branch 'origin/master'

.docker/build/install-deps.sh

@@ -19,7 +19,7 @@ git clone --branch $FSTAR_BRANCH https://github.com/FStarLang/FStar "$FSTAR_HOME
 opam install --deps-only "$FSTAR_HOME/fstar.opam"
 OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$FSTAR_HOME"
 
-sudo "$FSTAR_HOME/bin/get_fstar_z3.sh" "/usr/local/bin"
+sudo "$FSTAR_HOME/.scripts/get_fstar_z3.sh" "/usr/local/bin"
 
 # Install other deps
 "$build_home"/install-other-deps.sh

.nix/karamel.nix

@@ -33,7 +33,6 @@ in
 
     outputs = ["out" "home"];
 
-    FSTAR_HOME = fstar;
     GIT_REV = version;
 
     configurePhase = "export KRML_HOME=$(pwd)";
@@ -58,9 +57,6 @@ in
     passthru = {
       lib = ocamlPackages.buildDunePackage {
         GIT_REV = version;
-        # the Makefile expects `FSTAR_HOME` to be or `fstar.exe` to be
-        # in PATH, but this is not useful for buulding the library
-        FSTAR_HOME = "dummy";
         inherit version propagatedBuildInputs;
         nativeBuildInputs = with ocamlPackages; [menhir];
         pname = "krml";

Makefile

@@ -14,30 +14,14 @@ include $(visitors_root)/Makefile.preprocess
 
 .PHONY: all minimal clean test pre krmllib install
 
-ifeq ($(OS),Windows_NT)
-  OCAMLPATH_SEP=;
-else
-  OCAMLPATH_SEP=:
-endif
+FSTAR_EXE ?= fstar.exe
 
 all: minimal krmllib
 
-ifdef FSTAR_HOME
-  OCAMLPATH:=$(OCAMLPATH)$(OCAMLPATH_SEP)$(FSTAR_HOME)/lib
-else
-  FSTAR_EXE=$(shell which fstar.exe)
-  ifneq ($(FSTAR_EXE),)
-    FSTAR_HOME=$(dir $(FSTAR_EXE))/..
-    OCAMLPATH:=$(OCAMLPATH)$(OCAMLPATH_SEP)$(FSTAR_HOME)/lib
-  else
-    # If we are just trying to do a minimal build, we don't need F*.
-    ifneq ($(MAKECMDGOALS),minimal)
-      $(error "fstar.exe not found, please install FStar")
-    endif
-  endif
-endif
-export FSTAR_HOME
-export OCAMLPATH
+# If we are just trying to do a minimal build, we don't need F*.
+# Note: lazy assignment so this does not warn if fstar.exe is not there
+# (e.g. on a minimal build or cleaning)
+FSTAR_OCAMLENV = $(shell $(FSTAR_EXE) --ocamlenv)
 
 minimal: lib/AutoConfig.ml lib/Version.ml
 	dune build
@@ -74,8 +58,9 @@ test: all
 
 # Auto-detection
 pre:
-	@ocamlfind query fstar.lib >/dev/null 2>&1 || \
-	  { echo "Didn't find fstar.lib via ocamlfind or in FSTAR_HOME (which is: $(FSTAR_HOME)); run $(MAKE) -C $(FSTAR_HOME)"; exit 1; }
+	@eval "$(FSTAR_OCAMLENV)" && \
+	ocamlfind query fstar.lib >/dev/null 2>&1 || \
+	  { echo "Didn't find fstar.lib via ocamlfind; is F* properly installed? (FSTAR_EXE = $(FSTAR_EXE))"; exit 1; }
 
 
 install: all

README.md

@@ -48,9 +48,10 @@ make via homebrew, and invoke `gmake` instead of `make`.
 
 `$ opam install ppx_deriving_yojson zarith pprint "menhir>=20161115" sedlex process fix "wasm>=2.0.0" visitors ctypes-foreign ctypes uucp`
 
-Next, make sure you have an up-to-date F\*, and that you ran `make` in the
-`ulib/ml` directory of F\*. The `fstar.exe` executable should be on your PATH
-and `FSTAR_HOME` should point to the directory where F\* is installed.
+Next, make sure you have an up-to-date F\*, either as a binary package
+or that you have built it by running `make`. The `fstar.exe` executable
+should be on your PATH, or you may set the variable `FSTAR_EXE` to its
+location.
 
 To build just run `make` from this directory.
 

book/Setup.rst

@@ -40,7 +40,7 @@ For a nix flake based install use
 
   $ nix shell 
 
-In any case, remember to export suitable values for the ``FSTAR_HOME`` and
+In any case, remember to export suitable values for the ``FSTAR_EXE`` and
 ``KRML_HOME`` environment variables once you're done.
 
 We strongly recommend using the `fstar-mode.el

book/tutorial/Makefile

@@ -51,19 +51,7 @@ FSTAR_EXTRACT = --extract 'OCaml:-* +Spec'
 # - --cache_checked_modules to rely on a pre-built ulib and krmllib
 # - --cache_dir, to avoid polluting our generated build artifacts outside o
 
-# Where is F* ?
-ifndef FSTAR_HOME
-  FSTAR_EXE=$(shell which fstar.exe)
-  ifneq ($(FSTAR_EXE),)
-    # Assuming that fstar.exe is in some ..../bin directory
-    FSTAR_HOME=$(dir $(FSTAR_EXE))/..
-  else
-    $(error "fstar.exe not found, please install FStar")
-  endif
-endif
-export FSTAR_HOME
-
-FSTAR_NO_FLAGS = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_HINTS) \
+FSTAR_NO_FLAGS = $(FSTAR_EXE) $(FSTAR_HINTS) \
   --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
   --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \
   --cache_dir obj --hint_dir hints
@@ -234,9 +222,9 @@ dist/libbignum.a: dist/Makefile.basic
 # First complication... no comment.
 # NOTE: if F* was installed via opam, then this is redundant
 ifeq ($(OS),Windows_NT)
-  export OCAMLPATH := $(FSTAR_HOME)/lib;$(OCAMLPATH)
+  export OCAMLPATH := $(shell $(FSTAR_EXE) --locate_ocaml);$(OCAMLPATH)
 else
-  export OCAMLPATH := $(FSTAR_HOME)/lib:$(OCAMLPATH)
+  export OCAMLPATH := $(shell $(FSTAR_EXE) --locate_ocaml):$(OCAMLPATH)
 endif
 
 # Second complication: F* generates a list of ML files in the reverse linking

book/tutorial/Makefile.include

@@ -4,22 +4,12 @@
 
 BIGNUM_HOME ?= .
 
-# Where is F* ?
-ifndef FSTAR_HOME
-  FSTAR_EXE=$(shell which fstar.exe)
-  ifneq ($(FSTAR_EXE),)
-    # Assuming that fstar.exe is in some ..../bin directory
-    FSTAR_HOME=$(dir $(FSTAR_EXE))/..
-  else
-    $(error "fstar.exe not found, please install FStar")
-  endif
-endif
-export FSTAR_HOME
-
 ifeq (,$(KRML_HOME))
   $(error KRML_HOME is not defined)
 endif
 
+FSTAR_EXE ?= fstar.exe
+
 # I prefer to always check all fst files in the source directories; otherwise,
 # it's too easy to add a new file only to find out later that it's not being
 # checked. Note the usage of BIGNUM_HOME

krmllib/Makefile

@@ -13,13 +13,7 @@ all: verify-all compile-all
 # Verification & extraction                                                    #
 ################################################################################
 
-ifdef FSTAR_HOME
-  # Assume there is a F* source tree
-  FSTAR_EXE=$(FSTAR_HOME)/bin/fstar.exe
-else
-  # Assume F* in the PATH
-  FSTAR_EXE=fstar.exe
-endif
+FSTAR_EXE ?= fstar.exe
 
 EXTRACT_DIR = .extract
 
@@ -98,7 +92,7 @@ $(EXTRACT_DIR)/%.krml: | .depend
 # We don't extract LowStar.Lib as everything is generic data structures that
 # need to be specialized based on their usage from client code.
 KRML_ARGS += -fparentheses -fcurly-braces -fno-shadow -header copyright-header.txt \
-  -minimal -skip-compilation -extract-uints \
+  -fstar $(FSTAR_EXE) -minimal -skip-compilation -extract-uints \
   -bundle 'LowStar.Lib.\*'
 
 MACHINE_INTS = \