Merge pull request #516 from mtzguido/no_fstar_home

No FSTAR_HOME

.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 = \

lib/Driver.ml

@@ -45,8 +45,7 @@ module P = Process
  * understood as a cyclic dependency on our own [Output] module. *)
 
 (** These three variables filled in by [detect_fstar] *)
-let fstar = ref ""
-let fstar_home = ref ""
+let fstar = Options.fstar
 let fstar_lib = ref ""
 let fstar_rev = ref "<unknown>"
 let fstar_options = ref []
@@ -202,63 +201,50 @@ let detect_karamel_if () =
 let expand_prefixes s =
   if KString.starts_with s "FSTAR_LIB" then
     !fstar_lib ^^ KString.chop s "FSTAR_LIB"
-  else if KString.starts_with s "FSTAR_HOME" then
-    !fstar_home ^^ KString.chop s "FSTAR_HOME"
   else
     s
 
-(* Fills in fstar{,_home,_options} *)
+(* Fills in fstar{,_lib,_options}. Does NOT read any environment variables. *)
 let detect_fstar () =
   detect_karamel_if ();
 
   if not !Options.silent then
     KPrint.bprintf "%s⚙ KaRaMeL will drive F*.%s Here's what we found:\n" Ansi.blue Ansi.reset;
 
-  begin try
-    let r = Sys.getenv "FSTAR_HOME" in
-    if not !Options.silent then
-      KPrint.bprintf "read FSTAR_HOME via the environment\n";
-    fstar_home := r;
-    fstar := r ^^ "bin" ^^ "fstar.exe"
-  with Not_found -> try
-    fstar := read_one_line "which" [| "fstar.exe" |];
-    fstar_home := d (d !fstar);
-    if not !Options.silent then
-      KPrint.bprintf "FSTAR_HOME is %s (via fstar.exe in PATH)\n" !fstar_home
-  with _ ->
-    fatal_error "Did not find fstar.exe in PATH and FSTAR_HOME is not set"
+  (* Try to resolve fstar to an absolute path. This is just so the
+     full path appears in logs. *)
+  if not (KString.starts_with !fstar "/") then begin
+    try fstar := read_one_line "which" [| !fstar |]
+    with _ -> ()
   end;
 
-  let fstar_ulib = !fstar_home ^^ "ulib" in
-  if not (Sys.file_exists fstar_ulib && Sys.is_directory fstar_ulib) ; then begin
-    if not !Options.silent then
-      KPrint.bprintf "F* library not found in ulib; falling back to lib/fstar\n";
-    fstar_lib := !fstar_home ^^ "lib" ^^ "fstar"
-  end else begin
-    fstar_lib := fstar_ulib
+  if not !Options.silent then
+    KPrint.bprintf "Using fstar.exe = %s\n" !fstar;
+
+  (* Ask F* for the location of its library *)
+  begin try fstar_lib := read_one_line !fstar [| "--locate_lib" |]
+  with | _ ->
+    fatal_error "Could not locate F* library: %s --locate_lib failed" !fstar
   end;
+  if not !Options.silent then
+    KPrint.bprintf "F* library root: %s\n" !fstar_lib;
 
   if success "which" [| "cygpath" |] then begin
     fstar := read_one_line "cygpath" [| "-m"; !fstar |];
     if not !Options.silent then
       KPrint.bprintf "%sfstar converted to windows path:%s %s\n" Ansi.underline Ansi.reset !fstar;
-    fstar_home := read_one_line "cygpath" [| "-m"; !fstar_home |];
-    if not !Options.silent then
-      KPrint.bprintf "%sfstar home converted to windows path:%s %s\n" Ansi.underline Ansi.reset !fstar_home;
     fstar_lib := read_one_line "cygpath" [| "-m"; !fstar_lib |];
     if not !Options.silent then
       KPrint.bprintf "%sfstar lib converted to windows path:%s %s\n" Ansi.underline Ansi.reset !fstar_lib
   end;
 
-  if try Sys.is_directory (!fstar_home ^^ ".git") with Sys_error _ -> false then begin
-    let cwd = Sys.getcwd () in
-    Sys.chdir !fstar_home;
-    let branch = read_one_line "git" [| "rev-parse"; "--abbrev-ref"; "HEAD" |] in
-    fstar_rev := String.sub (read_one_line "git" [| "rev-parse"; "HEAD" |]) 0 8;
-    let color = if branch = "master" then Ansi.green else Ansi.orange in
+  (* Record F* version, as output by the executable. *)
+  begin try
+    let lines = Process.read_stdout !fstar [| "--version" |] in
+    fstar_rev := String.trim (String.concat " " lines);
     if not !Options.silent then
-      KPrint.bprintf "fstar is on %sbranch %s%s\n" color branch Ansi.reset;
-    Sys.chdir cwd
+      KPrint.bprintf "%sfstar version:%s %s\n" Ansi.underline Ansi.reset !fstar_rev
+  with | _ -> ()
   end;
 
   let fstar_includes = List.map expand_prefixes !Options.includes in
@@ -268,7 +254,16 @@ let detect_fstar () =
   ] @ List.flatten (List.rev_map (fun d -> ["--include"; d]) fstar_includes);
   (* This is a superset of the needed modules... some will be dropped very early
    * on in Karamel.ml *)
-  fstar_options := (!fstar_lib ^^ "FStar.UInt128.fst") :: !fstar_options;
+
+  (* Locate and pass FStar.UInt128 *)
+  let fstar_locate_file f =
+    try read_one_line !fstar [| "--locate_file"; f |]
+    with
+    | _ ->
+      Warn.fatal_error "Could not locate file %s, is F* properly installed?" f
+  in
+  fstar_options := fstar_locate_file "FStar.UInt128.fst" :: !fstar_options;
+
   fstar_options := (!runtime_dir ^^ "WasmSupport.fst") :: !fstar_options;
   if not !Options.silent then
     KPrint.bprintf "%sfstar is:%s %s %s\n" Ansi.underline Ansi.reset !fstar (String.concat " " !fstar_options);

lib/Options.ml

@@ -16,6 +16,7 @@ let no_prefix: Bundle.pat list ref = ref Bundle.[
   Module [ "C"; "Compat"; "Endianness" ];
   Module [ "LowStar"; "Endianness" ]
 ]
+let fstar = ref "fstar.exe" (* F* command to use *)
 (* krmllib.h now added directly in Output.ml so that it appears before the first
  * #ifdef *)
 let add_include: (include_ * string) list ref = ref [ ]

src/Karamel.ml

@@ -136,9 +136,6 @@ The default arguments are: %s
 All include directories and paths supports special prefixes:
   - if a path starts with FSTAR_LIB, this will expand to wherever F*'s ulib
     directory is
-  - if a path starts with FSTAR_HOME, this will expand to wherever the source
-    checkout of F* is (this does not always exist, e.g. in the case of an OPAM
-    setup)
 
 The compiler switches turn on the following options.
   [-cc gcc] (default) adds [%s]
@@ -192,6 +189,8 @@ Supported options:|}
   in
   let spec = [
     (* KaRaMeL as a driver *)
+    "-fstar", Arg.Set_string Options.fstar, " fstar.exe to use; defaults to \
+      'fstar.exe'";
     "-cc", Arg.Set_string Options.cc, " compiler to use; one of gcc (default), \
       compcert, g++, clang, msvc";
     "-m32", Arg.Set Options.m32, " turn on 32-bit cross-compiling";

test/Makefile

@@ -5,32 +5,26 @@ ifeq (3.81,$(MAKE_VERSION))
     install make, then invoke gmake instead of make)
 endif
 
-ifdef FSTAR_HOME
-  # Assume there is a F* source tree
-  FSTAR_EXE=$(FSTAR_HOME)/bin/fstar.exe
-else
-  FSTAR_EXE=$(shell which fstar.exe)
-  ifeq ($(FSTAR_EXE),)
-    $(error "fstar.exe not found, please install F*")
-  endif
-  # Assume F* in the PATH, in some ..../bin directory
-  FSTAR_HOME=$(dir FSTAR_EXE)/..
-endif
+FSTAR_EXE ?= fstar.exe
 
+# Note: these files have been moved in the F* repo in Dec 2023,
+# so this has not been tested in a while.
+ifdef FSTAR_HOME
 CRYPTO = $(shell \
   if test -d $(FSTAR_HOME)/examples/low-level/crypto ; \
   then echo $(FSTAR_HOME)/examples/low-level/crypto ; \
   elif test -d $(FSTAR_HOME)/share/fstar/examples/low-level/crypto ; \
   then echo $(FSTAR_HOME)/share/fstar/examples/low-level/crypto ; \
   fi \
 )
+endif
 
 ifneq ($(CRYPTO),)
   CRYPTO_OPTS	= -I $(CRYPTO) -I $(CRYPTO)/real
 endif
 TEST_OPTS	= -warn-error @4 -verbose -skip-makefiles
 KRML_BIN	= ../_build/default/src/Karamel.exe
-KRML		= $(KRML_BIN) $(KOPTS) $(TEST_OPTS)
+KRML		= $(KRML_BIN) -fstar $(FSTAR_EXE) $(KOPTS) $(TEST_OPTS)
 
 # TODO: disambiguate between broken tests that arguably should work (maybe
 # HigherOrder6?) and helper files that are required for multiple-module tests

test/sepcomp/a/Makefile

@@ -38,12 +38,7 @@ include Makefile.include
 # - --cache_checked_modules to rely on a pre-built ulib and krmllib
 # - --cache_dir, to avoid polluting our generated build artifacts outside o
 
-ifdef FSTAR_HOME
-  FSTAR_EXE=$(FSTAR_HOME)/bin/fstar.exe
-else
-  FSTAR_EXE=fstar.exe
-endif
-
+FSTAR_EXE ?= fstar.exe
 FSTAR_NO_FLAGS = $(FSTAR_EXE) \
   --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
   --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \
@@ -141,7 +136,7 @@ obj/%.krml:
 # F* --> C
 # --------
 
-KRML=$(KRML_HOME)/krml
+KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE)
 
 # Note: the implementation of the intrinsic uses external linkage, but you could
 # easily turn this file into a .h, use -add-include '"Impl_Bignum_Intrinsics.h"'

test/sepcomp/b/Makefile

@@ -39,12 +39,8 @@ include Makefile.include
 #   inline_for_extraction in the presence of interfaces
 # - --cache_checked_modules to rely on a pre-built ulib and krmllib
 # - --cache_dir, to avoid polluting our generated build artifacts outside o
-ifdef FSTAR_HOME
-  FSTAR_EXE=$(FSTAR_HOME)/bin/fstar.exe
-else
-  FSTAR_EXE=fstar.exe
-endif
 
+FSTAR_EXE ?= fstar.exe
 FSTAR_NO_FLAGS = $(FSTAR_EXE) \
   --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
   --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport A' --warn_error '+241@247+285' \
@@ -142,7 +138,7 @@ obj/%.krml:
 # F* --> C
 # --------
 
-KRML=$(KRML_HOME)/krml
+KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE)
 
 # Note: the implementation of the intrinsic uses external linkage, but you could
 # easily turn this file into a .h, use -add-include '"Impl_Bignum_Intrinsics.h"'