Add FSTAR_USE_KRML_EXE; migrate from KRML_HOME to KRML_EXE

.docker/build/build_funs.sh

@@ -39,10 +39,13 @@ function fetch_karamel() {
     echo Switching to KaRaMeL $ref
     git -C karamel reset --hard $ref
 
-    export_home KRML "$(pwd)/karamel"
+    # NB: make_karamel_pre builds karamel with the `minimal` target, which only
+    # produces the ./krml symlink (to the dune binary), not a full out/bin/krml
+    # install. So point KRML_EXE at karamel/krml here.
+    export KRML_EXE="$(pwd)/karamel/krml"
 
     # Install the Karamel dependencies
-    pushd $KRML_HOME
+    pushd karamel
     OPAMYES=true .docker/build/install-other-deps.sh
     popd
 }
@@ -67,7 +70,8 @@ function fstar_default_build () {
     # Start fetching and building karamel while we build F*
     if [[ -z "$CI_NO_KARAMEL" ]] ; then
         export FSTAR_CI_TEST_KARAMEL=1
-        export_home KRML "$(pwd)/karamel"
+        # karamel/krml (not out/bin/krml): see note in fetch_karamel (minimal build).
+        export KRML_EXE="$(pwd)/karamel/krml"
         (fetch_karamel ; make_karamel_pre) &
     fi
 

.github/agents/FStarDev.md

@@ -394,6 +394,8 @@ git submodule update --init karamel
 | Variable | Description |
 |----------|-------------|
 | `FSTAR_EXTERNAL_STAGE0` | Path to external fstar.exe to use as stage 0, usually not used |
+| `FSTAR_USE_KRML_EXE` | Set to `1` to skip building the karamel/ submodule and use the Karamel executable in `KRML_EXE` instead |
+| `KRML_EXE` | Path to the Karamel (`krml`) executable used to extract/build Pulse tests; required when `FSTAR_USE_KRML_EXE=1` |
 | `FSTAR_EXE` | Override which fstar.exe to use for a target |
 | `FSTAR_LIB` | Override the library path (ulib location) |
 | `FSTAR_DUNE_RELEASE` | Set to `1` for release (optimized) builds |

.scripts/advance.sh

@@ -129,9 +129,9 @@ build_and_refresh () {
     # If Karamel is around, we need to rebuild it.
     # To this end, we need to temporarily verify ulib
     # and clean it afterwards
-    if [[ -n "$KRML_HOME" ]] ; then
+    if [[ -n "$KRML_EXE" ]] ; then
         OTHERFLAGS='--admit_smt_queries true' make -j "$CI_THREADS" -C ulib
-        FSTAR_HOME="$PWD" make -j "$CI_THREADS" -C "$KRML_HOME"
+        FSTAR_HOME="$PWD" make -j "$CI_THREADS" -C karamel
         git clean -ffdx -- ulib
     fi
 

Makefile

@@ -12,6 +12,28 @@ FSTAR_DEFAULT_GOAL ?= build
 all: stage1 stage2 stage3 1.tests 2.tests boot-src-bare
 all-packages: package-1 package-2 package-src-1 package-src-2
 
+# By default, F* builds Karamel from the karamel/ submodule and uses the
+# resulting krml executable to test Pulse extraction. Set FSTAR_USE_KRML_EXE=1
+# to instead use an existing Karamel executable given by the KRML_EXE
+# environment variable; in that case the karamel/ submodule is not compiled.
+# KRML_EXE is a plain (non-exported) variable: it is passed explicitly to the
+# Pulse test sub-makes so that it does not leak into the Karamel build itself.
+.PHONY: karamel
+ifeq ($(FSTAR_USE_KRML_EXE),1)
+
+ifeq ($(KRML_EXE),)
+$(error FSTAR_USE_KRML_EXE is set to 1 but KRML_EXE is not set. Please set KRML_EXE to the full path of your Karamel executable.)
+endif
+
+# Nothing to build: use the user-provided Karamel executable.
+karamel:
+	@true
+
+else
+
+# Use the krml executable built from the karamel/ submodule.
+KRML_EXE := $(abspath karamel)/out/bin/krml
+
 karamel/Makefile:
 	$(error Error: $@ not found. Run `git submodule init && git submodule update` if you haven't)
 
@@ -30,6 +52,8 @@ karamel/Makefile:
 
 karamel: .krml.touch
 
+endif
+
 ### STAGES
 
 # For developers: you can set this variable externally, pointing
@@ -412,8 +436,8 @@ define install-stage
 	$(call bold_msg, "INSTALL", "STAGE $(1)")
 	$(MAKE) -C stage$(1) install PREFIX=$(CURDIR)/stage$(1)/out $(2)
 	@# ^ pass PREFIX to make sure we don't get it from env
-	@# Karamel install
-	$(MAKE) -C karamel install PREFIX=$(CURDIR)/stage$(1)/out LOWSTAR=false
+	@# Karamel install (skipped when using an external Karamel executable)
+	$(if $(filter 1,$(FSTAR_USE_KRML_EXE)),,$(MAKE) -C karamel install PREFIX=$(CURDIR)/stage$(1)/out LOWSTAR=false)
 	touch $@
 endef
 
@@ -570,42 +594,39 @@ test-2: stage2
 	$(MAKE) _test FSTAR_EXE=$(FSTAR_EXE)
 
 test-3: override FSTAR_EXE := $(abspath stage3/out/bin/fstar.exe)
-test-3: override KRML_HOME := $(abspath karamel)
 test-3: stage3
 	# Only test-3 calls test_pulse. The other compilers do not
 	# support Pulse.
-	$(MAKE) _test _test_pulse FSTAR_EXE=$(FSTAR_EXE) KRML_HOME=$(KRML_HOME)
+	$(MAKE) _test _test_pulse FSTAR_EXE=$(FSTAR_EXE) KRML_EXE=$(KRML_EXE)
 
 unit-tests: override FSTAR_EXE := $(abspath stage2/out/bin/fstar.exe)
 unit-tests: _unit-tests
 
 # Use directly only at your own risk.
 _test_pulse: FSTAR_EXE ?= $(abspath out/bin/fstar.exe)
-_test_pulse: KRML_HOME ?= $(abspath karamel)
 _test_pulse: _test_pulse_test _test_pulse_examples
 
 _test_pulse_test: karamel
 	env \
 	  STAGE3=1 \
-	  $(MAKE) -C pulse/test/ FSTAR_EXE=$(FSTAR_EXE) KRML_HOME=$(KRML_HOME)
+	  $(MAKE) -C pulse/test/ FSTAR_EXE=$(FSTAR_EXE) KRML_EXE=$(KRML_EXE)
 
 _test_pulse_examples: karamel
 	env \
 	  STAGE3=1 \
-	  $(MAKE) -C pulse/share/pulse/examples/ FSTAR_EXE=$(FSTAR_EXE) KRML_HOME=$(KRML_HOME)
+	  $(MAKE) -C pulse/share/pulse/examples/ FSTAR_EXE=$(FSTAR_EXE) KRML_EXE=$(KRML_EXE)
 
 accept_pulse_test:
 	env \
 	  STAGE3=1 \
-	  $(MAKE) -C pulse/test/ accept FSTAR_EXE=$(FSTAR_EXE) KRML_HOME=$(KRML_HOME)
+	  $(MAKE) -C pulse/test/ accept FSTAR_EXE=$(FSTAR_EXE) KRML_EXE=$(KRML_EXE)
 
 accept_pulse_examples:
 	env \
 	  STAGE3=1 \
-	  $(MAKE) -C pulse/share/pulse/examples/ accept FSTAR_EXE=$(FSTAR_EXE) KRML_HOME=$(KRML_HOME)
+	  $(MAKE) -C pulse/share/pulse/examples/ accept FSTAR_EXE=$(FSTAR_EXE) KRML_EXE=$(KRML_EXE)
 
 accept_pulse: override FSTAR_EXE := $(abspath stage3/out/bin/fstar.exe)
-accept_pulse: override KRML_HOME := $(abspath karamel)
 accept_pulse: accept_pulse_test accept_pulse_examples
 
 .PHONY: _test_pulse_test _test_pulse_examples accept_pulse_test accept_pulse_examples accept_pulse

examples/tactics/Makefile

@@ -3,19 +3,26 @@ EXCLUDED_FSTAR_FILES=Launch.fst Poly1.fst Poly2.fst
 SUBDIRS += eci19
 FSTAR_FILES = $(filter-out $(EXCLUDED_FSTAR_FILES), $(wildcard *.fst))
 
-ifndef KRML_HOME
+# The StringPrinter demo extracts to C and needs Karamel's krmllib to verify
+# and the krml executable to extract. Only enable it when a Karamel executable
+# is provided in KRML_EXE (checked before mk/test.mk sets a default value).
+ifdef KRML_EXE
+HAVE_KRML := 1
+endif
+
+ifndef HAVE_KRML
   EXCLUDED_FSTAR_FILES += $(wildcard StringPrinter*)
 endif
-ifdef KRML_HOME
-OTHERFLAGS += --include $(KRML_HOME)/krmllib
+ifdef HAVE_KRML
+OTHERFLAGS += --include "$(shell "$(KRML_EXE)" -locate-krmllib)"
 endif
 
 FSTAR_ROOT ?= ../..
 include $(FSTAR_ROOT)/mk/test.mk
 
-ifdef KRML_HOME
+ifdef HAVE_KRML
 stringprintertest: $(CACHE_DIR)
-	 [ ! -f $(KRML_HOME)/krml ] || [ ! -x $(KRML_HOME)/krml ] || $(KRML_HOME)/krml -tmpdir stringprintertest -bundle 'StringPrinter.\*' -bundle StringPrinterTest.Aux -drop 'FStar.Tactics.\*' -drop 'FStar.Reflection.\*' StringPrinterTest.fst -skip-linking
+	 [ ! -f "$(KRML_EXE)" ] || [ ! -x "$(KRML_EXE)" ] || "$(KRML_EXE)" -tmpdir stringprintertest -bundle 'StringPrinter.\*' -bundle StringPrinterTest.Aux -drop 'FStar.Tactics.\*' -drop 'FStar.Reflection.\*' StringPrinterTest.fst -skip-linking
 else
 stringprintertest:
 endif

examples/tactics/bench/Makefile

@@ -1,9 +1,15 @@
 FSTAR_HOME=../../..
 INCLUDE_PATHS=..
-KRML_HOME?=$(FSTAR_HOME)/../Karamel
-INCLUDE_PATHS=$(KRML_HOME)/krmllib ..
 EXCLUDED_FSTAR_FILES=PolyStub.fst
 
+# If a Karamel executable is provided, add its krmllib to the F* include path.
+# Pass it to F* directly via --include (quoted) instead of through INCLUDE_PATHS,
+# which is expanded with $(addprefix --include , ...) and would split a path
+# containing whitespace (e.g. C:\Program Files on Windows).
+ifdef KRML_EXE
+KRMLLIB_INCLUDE = --include "$(shell "$(KRML_EXE)" -locate-krmllib)"
+endif
+
 POLYS=$(foreach FACTOR,1 2 3,\
       $(foreach SE, 0 1,\
       $(foreach ED, 0 1,\
@@ -35,6 +41,6 @@ CanonCommSemiring.cmxs: ../CanonCommSemiring.cmxs
 	ln -sf $< $@
 
 _cache/Bench.%.fst.checked: Bench.%.fst CanonCommSemiring.cmxs
-	$(FSTAR) --cache_off --odir _output --cache_dir _cache $< --load CanonCommSemiring --include ..
+	$(FSTAR) --cache_off --odir _output --cache_dir _cache $(KRMLLIB_INCLUDE) $< --load CanonCommSemiring --include ..
 
 verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))

pulse/.devcontainer/fromscratch/minimal.Dockerfile

@@ -72,7 +72,7 @@ RUN eval $(opam env) \
  && make -j$(nproc)
 
 ENV FSTAR_EXE  $HOME/FStar/bin/fstar.exe
-ENV KRML_HOME $HOME/karamel
+ENV KRML_EXE $HOME/karamel/out/bin/krml
 
 # Instrument .profile and .bashrc to set the opam switch. Note that this
 # just appends the *call* to eval $(opam env) in these files, so we

pulse/.github/workflows/ci.yml

@@ -79,7 +79,7 @@ jobs:
           path: karamel
           key: karamel-${{ runner.os }}-${{ runner.arch }}-${{ steps.checkout-fstar.outputs.commit }}-${{ steps.checkout-karamel.outputs.commit }}
 
-      - run: echo "KRML_HOME=$(pwd)/karamel" | sudo tee -a $GITHUB_ENV
+      - run: echo "KRML_EXE=$(pwd)/karamel/out/bin/krml" | sudo tee -a $GITHUB_ENV
 
       - uses: actions/checkout@master
         with:

pulse/.scripts/mk_package.sh

@@ -2,7 +2,7 @@
 
 # This scripts builds a "standalone" package with F* and Pulse. It
 # does not include karamel as there is no way to install it and use it
-# without setting a KRML_HOME, which I would like to avoid. This will be
+# without setting a KRML_EXE, which I would like to avoid. This will be
 # fixed soon.
 
 set -eux

pulse/CONTRIBUTING.md

@@ -122,7 +122,8 @@ go into `test/`. All of `share/pulse` is distributed in the package.
 
 You can run `make -j test` to verify and test them. This rule will
 work whether you have Karamel or not. If you have Karamel with the
-`KRML_HOME` variable set, then this rule will also extract and compile
+`KRML_EXE` variable pointing to the `krml` executable, then this rule
+will also extract and compile
 (and sometimes run) C extraction examples. Alternatively, you can run
 `make -j test` from the Pulse root directory, which will build Pulse
 beforehand.

pulse/mk/locate.mk

@@ -4,12 +4,8 @@ FSTAR_EXE ?= fstar.exe
 $(call need_exe, FSTAR_EXE)
 
 ifeq ($(KRML_EXE),)
-ifneq ($(KRML_HOME),)
-KRML_EXE := $(KRML_HOME)/krml
-else
 KRML_EXE := krml
 endif
-endif
 
 export KRML_EXE
 

pulse/pulse2rust/dpe/c.Makefile

@@ -24,9 +24,9 @@ include $(PULSE_ROOT)/mk/boot.mk
 .DEFAULT_GOAL := all
 
 
-$(call need_dir,KRML_HOME)
+$(call need,KRML_EXE)
 
-KRML ?= $(KRML_HOME)/krml
+KRML ?= $(KRML_EXE)
 
 .PHONY: extract
 extract: $(ALL_KRML_FILES)

pulse/share/pulse/examples/dice/c.Makefile

@@ -17,7 +17,7 @@ include $(PULSE_ROOT)/mk/boot.mk
 
 .DEFAULT_GOAL := myall
 
-KRML ?= $(KRML_HOME)/krml
+KRML ?= $(KRML_EXE)
 
 myall: verify test
 

pulse/share/pulse/examples/dice/cbor/Makefile

@@ -22,7 +22,7 @@ include $(PULSE_ROOT)/mk/boot.mk
 
 .DEFAULT_GOAL := myall
 
-KRML=$(KRML_HOME)/krml $(KRML_OPTS)
+KRML=$(KRML_EXE) $(KRML_OPTS)
 myall: verify test
 
 .PHONY: extract_all

pulse/share/pulse/examples/dice/cbor/extern/Makefile

@@ -4,7 +4,10 @@ all: build
 
 build: CBOR.o
 
+KRML_INCLUDE = $(shell "$(KRML_EXE)" -locate-include)
+KRML_KRMLLIB = $(shell "$(KRML_EXE)" -locate-krmllib)
+
 %.o: %.c
-	$(CC) -Wall -I $(KRML_HOME)/include -I $(KRML_HOME)/krmllib/dist/generic -c -o $@ $<
+	$(CC) -Wall -I "$(KRML_INCLUDE)" -I "$(KRML_KRMLLIB)/dist/generic" -c -o $@ $<
 
 CBOR.o: CBOR.h internal/CBOR.h

pulse/share/pulse/examples/dice/cbor/test/Makefile

@@ -10,8 +10,11 @@ CBORTest: .CBORTest.touch
 	./CBORTest.exe
 	touch $@
 
+KRML_INCLUDE = $(shell "$(KRML_EXE)" -locate-include)
+KRML_KRMLLIB = $(shell "$(KRML_EXE)" -locate-krmllib)
+
 CBORTest.o: CBORTest.c
-	$(CC) -Werror -I $(KRML_HOME)/include -I $(KRML_HOME)/krmllib/dist/generic -I ../_output/ -c -o $@ $<
+	$(CC) -Werror -I "$(KRML_INCLUDE)" -I "$(KRML_KRMLLIB)/dist/generic" -I ../_output/ -c -o $@ $<
 
 CBORTest.exe: CBORTest.o ../_output/CBOR_Pulse.o ../extern/CBOR.o
 	$(CC) -o CBORTest.exe $^

pulse/share/pulse/examples/dice/external/Makefile

@@ -12,7 +12,7 @@
 
 # include $(PULSE_HOME)/share/pulse/Makefile.include
 
-# KRML ?= $(KRML_HOME)/krml
+# KRML ?= $(KRML_EXE)
 
 # .PHONY: extract
 # extract: $(ALL_KRML_FILES)