From 592001db581a5875e44646438657154ee44e1a1d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 5 Jan 2025 14:57:11 -0800 Subject: [PATCH 1/5] Karamel: do not read FSTAR_HOME, introduce -fstar option Karamel will just find fstar.exe in the PATH. If one wants to override this then `-fstar /path/to/fstar.exe` can be used. There is also no trying to peek into the an F* Git repo to get a commit hash, just looking at the output of `fstar.exe --version` instead. --- README.md | 7 ++--- book/Setup.rst | 2 +- lib/Driver.ml | 69 +++++++++++++++++++++++--------------------------- lib/Options.ml | 1 + src/Karamel.ml | 5 ++-- 5 files changed, 40 insertions(+), 44 deletions(-) diff --git a/README.md b/README.md index cca80f42..58998190 100644 --- a/README.md +++ b/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. diff --git a/book/Setup.rst b/book/Setup.rst index a401f242..6c437233 100644 --- a/book/Setup.rst +++ b/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 diff --git a/lib/Driver.ml b/lib/Driver.ml index 43a47049..1af728b5 100644 --- a/lib/Driver.ml +++ b/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 "" 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); diff --git a/lib/Options.ml b/lib/Options.ml index b796f1e5..e9ea07ce 100644 --- a/lib/Options.ml +++ b/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 [ ] diff --git a/src/Karamel.ml b/src/Karamel.ml index 19db0da3..425a3cc3 100644 --- a/src/Karamel.ml +++ b/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"; From 2b81a9dc5462aeddb629dee11d1d10ec2ffd956b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 8 Jan 2025 09:56:59 -0800 Subject: [PATCH 2/5] Makefiles: no FSTAR_HOME, use FSTAR_EXE ?= fstar.exe --- Makefile | 22 ++++++---------------- book/tutorial/Makefile | 18 +++--------------- book/tutorial/Makefile.include | 14 ++------------ krmllib/Makefile | 10 ++-------- test/Makefile | 16 ++++------------ test/sepcomp/a/Makefile | 9 ++------- test/sepcomp/b/Makefile | 8 ++------ 7 files changed, 21 insertions(+), 76 deletions(-) diff --git a/Makefile b/Makefile index b02343cf..76b97d5e 100644 --- a/Makefile +++ b/Makefile @@ -14,6 +14,8 @@ include $(visitors_root)/Makefile.preprocess .PHONY: all minimal clean test pre krmllib install +FSTAR_EXE ?= fstar.exe + ifeq ($(OS),Windows_NT) OCAMLPATH_SEP=; else @@ -22,22 +24,10 @@ endif 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 +# If we are just trying to do a minimal build, we don't need F*. +ifneq ($(MAKECMDGOALS),minimal) +export OCAMLPATH := $(OCAMLPATH)$(OCAMLPATH_SEP)$(shell $(FSTAR_EXE) --locate_ocaml) endif -export FSTAR_HOME -export OCAMLPATH minimal: lib/AutoConfig.ml lib/Version.ml dune build @@ -75,7 +65,7 @@ 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; } + { echo "Didn't find fstar.lib via ocamlfind; is F* properly installed? (FSTAR_EXE = $(FSTAR_EXE))"; exit 1; } install: all diff --git a/book/tutorial/Makefile b/book/tutorial/Makefile index 6890ca70..1d0309f7 100644 --- a/book/tutorial/Makefile +++ b/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 diff --git a/book/tutorial/Makefile.include b/book/tutorial/Makefile.include index e75675ec..5ffd6a5d 100644 --- a/book/tutorial/Makefile.include +++ b/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 diff --git a/krmllib/Makefile b/krmllib/Makefile index 83f79fd5..1ed57866 100644 --- a/krmllib/Makefile +++ b/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 = \ diff --git a/test/Makefile b/test/Makefile index 7b04a8e4..a081f156 100644 --- a/test/Makefile +++ b/test/Makefile @@ -5,18 +5,9 @@ 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 +ifdef FSTAR_HOME CRYPTO = $(shell \ if test -d $(FSTAR_HOME)/examples/low-level/crypto ; \ then echo $(FSTAR_HOME)/examples/low-level/crypto ; \ @@ -24,13 +15,14 @@ CRYPTO = $(shell \ 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 diff --git a/test/sepcomp/a/Makefile b/test/sepcomp/a/Makefile index 50ac09a3..e32e8cc3 100644 --- a/test/sepcomp/a/Makefile +++ b/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"' diff --git a/test/sepcomp/b/Makefile b/test/sepcomp/b/Makefile index db8693e6..e8c20d86 100644 --- a/test/sepcomp/b/Makefile +++ b/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"' From 7ff460e2cc37ddcf68f87eac3ad69b7387a4d953 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 8 Jan 2025 09:55:49 -0800 Subject: [PATCH 3/5] test/Makefile: a note about a use of FSTAR_HOME --- test/Makefile | 2 ++ 1 file changed, 2 insertions(+) diff --git a/test/Makefile b/test/Makefile index a081f156..a587761b 100644 --- a/test/Makefile +++ b/test/Makefile @@ -7,6 +7,8 @@ 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 ; \ From 21ea5a0a0d277630b4b2dddd9b429dd582d53e66 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 7 Jan 2025 23:19:47 -0800 Subject: [PATCH 4/5] nix: remove FSTAR_HOME --- .nix/karamel.nix | 4 ---- 1 file changed, 4 deletions(-) diff --git a/.nix/karamel.nix b/.nix/karamel.nix index b7421294..3aca7926 100644 --- a/.nix/karamel.nix +++ b/.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"; From abeca9a54f8439fcb832de4ec6fe256e86c14ce9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 8 Jan 2025 16:36:10 -0800 Subject: [PATCH 5/5] Makefile: remove warning on startup when no F* is present Wait until the ocamlenv is actually needed. It seems to be only relevant for the 'pre' rule, which also does not seem to be required... --- Makefile | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/Makefile b/Makefile index 76b97d5e..e275ee40 100644 --- a/Makefile +++ b/Makefile @@ -16,18 +16,12 @@ include $(visitors_root)/Makefile.preprocess FSTAR_EXE ?= fstar.exe -ifeq ($(OS),Windows_NT) - OCAMLPATH_SEP=; -else - OCAMLPATH_SEP=: -endif - all: minimal krmllib # If we are just trying to do a minimal build, we don't need F*. -ifneq ($(MAKECMDGOALS),minimal) -export OCAMLPATH := $(OCAMLPATH)$(OCAMLPATH_SEP)$(shell $(FSTAR_EXE) --locate_ocaml) -endif +# 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 @@ -64,7 +58,8 @@ test: all # Auto-detection pre: - @ocamlfind query fstar.lib >/dev/null 2>&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; }