diff --git a/.github/agents/FStarDev.md b/.github/agents/FStarDev.md
index 23c4f70c415..a27107c8573 100644
--- a/.github/agents/FStarDev.md
+++ b/.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 |
diff --git a/Makefile b/Makefile
index 2426db90380..2a1fec8fb13 100644
--- a/Makefile
+++ b/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
diff --git a/examples/tactics/Makefile b/examples/tactics/Makefile
index 41da0fa978f..873d1b4d463 100644
--- a/examples/tactics/Makefile
+++ b/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
diff --git a/examples/tactics/bench/Makefile b/examples/tactics/bench/Makefile
index e63cb321554..bdb500d2685 100644
--- a/examples/tactics/bench/Makefile
+++ b/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)))
diff --git a/pulse/.devcontainer/fromscratch/minimal.Dockerfile b/pulse/.devcontainer/fromscratch/minimal.Dockerfile
index bd67988479d..c8465265865 100644
--- a/pulse/.devcontainer/fromscratch/minimal.Dockerfile
+++ b/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
diff --git a/pulse/.github/workflows/ci.yml b/pulse/.github/workflows/ci.yml
index 282ed7700ee..295479d4d78 100644
--- a/pulse/.github/workflows/ci.yml
+++ b/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:
diff --git a/pulse/.scripts/mk_package.sh b/pulse/.scripts/mk_package.sh
deleted file mode 100755
index 8e5c11815c9..00000000000
--- a/pulse/.scripts/mk_package.sh
+++ /dev/null
@@ -1,52 +0,0 @@
-#!/bin/bash
-
-# 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
-# fixed soon.
-
-set -eux
-
-if [ "$(uname -s)" = "Darwin" ]; then
-MAKE="gmake -ksj$(nproc)"
-else
-MAKE="make -ksj$(nproc)"
-fi
-
-if ! [ -d FStar ]; then
-  git clone https://github.com/FStarLang/FStar --depth 1
-fi
-
-$MAKE -C FStar ADMIT=1
-export FSTAR_EXE=$(pwd)/FStar/bin/fstar.exe
-
-$MAKE ADMIT=1
-
-rm -rf _pak
-mkdir -p _pak/pulse
-$MAKE -C FStar install PREFIX=$(pwd)/_pak/pulse
-
-$MAKE install PREFIX=$(pwd)/_pak/pulse
-
-cat >_pak/pulse/bin/pulse << EOF
-#!/bin/bash
-
-# Pulse is really just F* + an include path. The pulse plugin
-# is loaded automatically by F* when needed (e.g. when processing
-# a #lang-pulse declaration).
-
-D=\$(dirname "\$0")
-
-exec \$D/fstar.exe --include "\$D/../lib/pulse" "\$@"
-EOF
-
-chmod +x _pak/pulse/bin/pulse
-
-KERNEL=$(uname -s)
-ARCH=$(uname -m)
-PAK=pulse-$KERNEL-$ARCH.tar.gz
-
-tar czf $PAK -C _pak .
-
-echo Done
-ls -l $PAK
diff --git a/pulse/CONTRIBUTING.md b/pulse/CONTRIBUTING.md
index 1f439d6381c..2c0b47675cf 100644
--- a/pulse/CONTRIBUTING.md
+++ b/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.
diff --git a/pulse/mk/locate.mk b/pulse/mk/locate.mk
index 0eacae5c27e..5483ebf6da6 100644
--- a/pulse/mk/locate.mk
+++ b/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
 
diff --git a/pulse/pulse2rust/dpe/c.Makefile b/pulse/pulse2rust/dpe/c.Makefile
index d01e39e5d72..d529f503a4b 100644
--- a/pulse/pulse2rust/dpe/c.Makefile
+++ b/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)
diff --git a/pulse/share/pulse/examples/dice/c.Makefile b/pulse/share/pulse/examples/dice/c.Makefile
index 9e4fc26fcb6..2469145c169 100644
--- a/pulse/share/pulse/examples/dice/c.Makefile
+++ b/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
 
diff --git a/pulse/share/pulse/examples/dice/cbor/Makefile b/pulse/share/pulse/examples/dice/cbor/Makefile
index 4e68b1887f5..4709ce936df 100644
--- a/pulse/share/pulse/examples/dice/cbor/Makefile
+++ b/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
diff --git a/pulse/share/pulse/examples/dice/cbor/extern/Makefile b/pulse/share/pulse/examples/dice/cbor/extern/Makefile
index 3271ab7d258..1daa027f52e 100644
--- a/pulse/share/pulse/examples/dice/cbor/extern/Makefile
+++ b/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
diff --git a/pulse/share/pulse/examples/dice/cbor/test/Makefile b/pulse/share/pulse/examples/dice/cbor/test/Makefile
index 810e688e400..58e01749b59 100644
--- a/pulse/share/pulse/examples/dice/cbor/test/Makefile
+++ b/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 $^
diff --git a/pulse/share/pulse/examples/dice/external/Makefile b/pulse/share/pulse/examples/dice/external/Makefile
index 1ad86749bc1..067d87d051f 100644
--- a/pulse/share/pulse/examples/dice/external/Makefile
+++ b/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)
diff --git a/stage0/INSTALL.md b/stage0/INSTALL.md
index c866301516b..52b33b0033f 100644
--- a/stage0/INSTALL.md
+++ b/stage0/INSTALL.md
@@ -129,7 +129,7 @@ commands. (Note: On Windows this requires Cygwin and `make`)
          are interested in compiling these examples.
 
    Note: Some of the examples currently require having [KaRaMeL](https://github.com/FStarLang/karamel)
-         installed and the `KRML_HOME` variable pointing to its location.
+         installed and the `KRML_EXE` variable pointing to its `krml` executable.
          If KaRaMeL is absent, then these examples will be skipped.
 
    Note: On Linux if you get a file descriptor exhaustion error that looks