project-everest · tahina-pro · Apr 3, 2026 · Apr 3, 2026 · Apr 3, 2026 · Apr 3, 2026
diff --git a/.gitignore b/.gitignore
@@ -30,4 +30,5 @@ nuget_package
 .*.touch
 .opam
 .opam.tmp
+krmllib.done
 opam-env.Makefile
diff --git a/Makefile b/Makefile
@@ -112,7 +112,7 @@ lowparse-bitfields-test: lowparse
 #	+$(MAKE) -C tests/bitfields
 
 ifeq (,$(NO_PULSE))
-lowparse-pulse-test: lowparse
+lowparse-pulse-test: lowparse krmllib.done
 	+$(MAKE) -C share/everparse/tests/lowparse
 #	+$(MAKE) -C tests/pulse # TODO: move it into `share/everparse/tests/lowparse` and re-enable it
 else
@@ -128,7 +128,7 @@ quackyducky-lowstar-test: quackyducky
 
 .PHONY: quackyducky-lowstar-test
 
-quackyducky-pulse-test: quackyducky
+quackyducky-pulse-test: quackyducky krmllib.done
 	+$(MAKE) -C share/everparse/tests/qd
 
 .PHONY: quackyducky-pulse-test

diff --git a/README.md b/README.md
@@ -387,10 +387,8 @@ variables:
   `EVERPARSE_USE_OPAMROOT=1`.
 
 * If you want to use your own Karamel, first set
-  `EVERPARSE_USE_KRML_HOME=1`, then set `KRML_HOME` to the full path
-  of your clone of the Karamel repository. This will automatically set
-  `EVERPARSE_USE_FSTAR_HOME=1`, since the Karamel library must be
-  compiled with the same F\* as EverParse.
+  `EVERPARSE_USE_KRML_EXE=1`, then set `KRML_EXE` to the full path
+  of the Karamel executable.
 
 As a shortcut, setting `EVERPARSE_USE_MY_DEPS=1` has the same effect
 as setting all of those environment variables to 1.

diff --git a/deps.Makefile b/deps.Makefile
@@ -18,25 +18,17 @@ EVERPARSE_Z3_VERSION ?= 4.13.3
 ifeq (1,$(EVERPARSE_USE_MY_DEPS))
 export EVERPARSE_USE_OPAMROOT:=1
 export EVERPARSE_USE_FSTAR_EXE:=1
-export EVERPARSE_USE_KRML_HOME:=1
+export EVERPARSE_USE_KRML_EXE:=1
 endif
 
 NEED_KRML :=
-ifneq (1,$(EVERPARSE_USE_KRML_HOME))
-export KRML_HOME := $(EVERPARSE_OPT_PATH)/FStar/karamel
-
-# Needed by LowParse (Pulse) tests
-export KRML_LIBDIR := $(KRML_HOME)/krmllib
-export KRML_INCLUDEDIR := $(KRML_HOME)/include
-export KRML_MISCDIR := $(KRML_HOME)/misc
-export KRML_EXE := $(KRML_HOME)/krml
-
+ifneq (1,$(EVERPARSE_USE_KRML_EXE))
+export KRML_EXE := $(EVERPARSE_OPT_PATH)/FStar/karamel/out/bin/krml
 NEED_KRML := $(EVERPARSE_OPT_PATH)/karamel.done
 else
-export EVERPARSE_USE_FSTAR_EXE:=1
-ifeq (,$(KRML_HOME))
+ifeq (,$(KRML_EXE))
 # TODO: fix Karamel to not require KRML_HOME set
-$(error "Inconsistent setup: EVERPARSE_USE_KRML_HOME set but KRML_HOME not set")
+$(error "Inconsistent setup: EVERPARSE_USE_KRML_EXE set but KRML_EXE not set")
 endif
 endif
 
@@ -96,6 +88,8 @@ export PATH := $(z3_dir):$(PATH)
 $(EVERPARSE_OPT_PATH)/opam/opam-init/init.sh:
 	+$(MAKE) -C $(EVERPARSE_OPT_PATH) opam
 
+clean_rules += clean-krmllib
+
 ifeq (,$(filter clean distclean $(clean_rules),$(MAKECMDGOALS)))
 opam-env.Makefile: $(NEED_OPAM_DIR)
 	rm -rf $@.tmp
@@ -139,17 +133,20 @@ $(EVERPARSE_OPT_PATH)/z3: $(EVERPARSE_OPT_PATH)/FStar/Makefile
 $(EVERPARSE_OPT_PATH)/karamel.done: $(EVERPARSE_OPT_PATH)/FStar/karamel/Makefile $(NEED_FSTAR) $(NEED_OPAM)
 	rm -f $@
 	+$(with_opam) env OTHERFLAGS='--admit_smt_queries true' $(MAKE) -C $(EVERPARSE_OPT_PATH)/FStar/karamel minimal
+	touch $@
+
+krmllib.done: $(NEED_KRML)
 	# Needed by LowParse (Pulse) tests
-	+$(MAKE) -C $(KRML_LIBDIR)/dist/generic -f Makefile.basic
+	+export KRML_LIBPATH="$$($(KRML_EXE) -locate-krmllib)" && $(MAKE) -C "$$KRML_LIBPATH"/dist/generic -f Makefile.basic
 	touch $@
 
 env:
 	@echo export EVERPARSE_USE_OPAMROOT=$(EVERPARSE_USE_OPAMROOT)
 	@echo export EVERPARSE_USE_FSTAR_EXE=$(EVERPARSE_USE_FSTAR_EXE)
-	@echo export EVERPARSE_USE_KRML_HOME=$(EVERPARSE_USE_KRML_HOME)
+	@echo export EVERPARSE_USE_KRML_EXE=$(EVERPARSE_USE_KRML_EXE)
 	@echo export FSTAR_EXE=$(FSTAR_EXE)
 	@echo export DICE_HOME=$(DICE_HOME)
-	@echo export KRML_HOME=$(KRML_HOME)
+	@echo export KRML_EXE=$(KRML_EXE)
 ifeq ($(OS),Windows_NT)
 	@echo export EVERPARSE_HOME=$(shell cygpath -u $(CURDIR))
 else
@@ -162,9 +159,17 @@ endif
 
 deps: $(NEED_OPAM) $(NEED_FSTAR) $(NEED_Z3) $(NEED_KRML)
 
+deps: krmllib.done
+
 .PHONY: deps
 
-distclean: clean
+clean-krmllib:
+	rm -f krmllib.done
+	# +$(MAKE) -C "$$($(KRML_EXE) -locate-krmllib)"/dist/generic -f Makefile.basic clean || true # This works, but I am not sure we should clean up anything outside of the EverParse tree. In the opt/ case, krmllib is in opt/FStar, which `distclean` will remove altogether.
+
+.PHONY: clean-krmllib
+
+distclean: clean clean-krmllib
 	rm -rf opam-env.Makefile
 	+$(MAKE) -C opt clean
 

diff --git a/share/everparse/tests/lowparse/Makefile b/share/everparse/tests/lowparse/Makefile
@@ -22,7 +22,7 @@ ifeq ($(OS),Darwin)
 KRML_OPTS += -ccopt -Wno-tautological-constant-out-of-range-compare
 endif
 
-KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS)
+KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS)
 
 EXAMPLES=Example3 ExampleConstInt32le Example2 Example5 Example7 Example8 Example9 Example10 Example11 Example12 ExampleDepLen
 

diff --git a/share/everparse/tests/qd/unit/extracted.Makefile b/share/everparse/tests/qd/unit/extracted.Makefile
@@ -2,13 +2,11 @@ EVERPARSE_HOME ?= $(realpath ../../../../../..)
 EVERPARSE_SRC_PATH ?= $(EVERPARSE_HOME)/src
 
 LOWPARSE_HOME ?= $(EVERPARSE_SRC_PATH)/lowparse
-KRML_HOME ?= $(EVERPARSE_HOME)/opt/karamel
 
 include $(EVERPARSE_SRC_PATH)/fstar.Makefile
 
 export FSTAR_EXE
 export LOWPARSE_HOME
-export KRML_HOME
 
 ifdef NO_QD_VERIFY
 LAX_EXT=.lax
@@ -37,7 +35,7 @@ KRML_OPTS += -ccopt -Wno-tautological-constant-out-of-range-compare
 endif
 
 # -Wno-tautological-overlap-compare because of T32
-KRML = $(KRML_HOME)/krml \
+KRML = $(KRML_EXE) \
 	 -fstar $(FSTAR_EXE) \
 	 -ccopt "-O3" -ccopt "-ffast-math" \
 	 -ccopt "-Wno-tautological-overlap-compare" \

diff --git a/src/ASN1/Makefile b/src/ASN1/Makefile
@@ -1,7 +1,6 @@
 all: verify compile
 
 EVERPARSE_HOME ?= ../..
-KRML_HOME ?= $(EVERPARSE_HOME)/../karamel
 
 LOWPARSE_HOME=$(EVERPARSE_HOME)/src/lowparse
 
@@ -55,7 +54,7 @@ krml.rsp: $(ALL_KRML_FILES)
 	mv $@.tmp $@
 
 Test.c: krml.rsp
-	$(KRML_HOME)/krml -fstar $(FSTAR_EXE) \
+	$(KRML_EXE) -fstar $(FSTAR_EXE) \
 	  -bundle 'ASN1Test=ASN1Test.\*,Prims,FStar.\*,C.\*,C,LowStar.\*,LowParse.\*' \
 	  -no-prefix ASN1Test \
 	  -skip-makefiles \

diff --git a/src/cbor/pulse/det/vertest/c/Makefile b/src/cbor/pulse/det/vertest/c/Makefile
@@ -25,7 +25,7 @@ $(OUTPUT_DIRECTORY)/test.exe: $(OUTPUT_DIRECTORY)/CBORTest.o
 	$(CC) $(CFLAGS) -c -o $@ $<
 
 $(OUTPUT_DIRECTORY)/CBORTest.c: $(ALL_KRML_FILES)
-	$(KRML_HOME)/krml $(KRML_OPTS) -warn-error @1..27 -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C=CBOR.\*[rename=CBORDetAPI]' -bundle 'CBORTest=\*' -add-include '"CBORDetAbstract.h"' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBORTest -tmpdir $(OUTPUT_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^
+	$(KRML_EXE) $(KRML_OPTS) -warn-error @1..27 -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C=CBOR.\*[rename=CBORDetAPI]' -bundle 'CBORTest=\*' -add-include '"CBORDetAbstract.h"' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBORTest -tmpdir $(OUTPUT_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^
 
 test: extract
 	$(OUTPUT_DIRECTORY)/test.exe

diff --git a/src/cbor/pulse/det/vertest/common/Makefile b/src/cbor/pulse/det/vertest/common/Makefile
@@ -25,10 +25,10 @@ $(OUTPUT_DIRECTORY)/test.exe: $(OUTPUT_DIRECTORY)/CBORTest.o
 	$(CC) $(CFLAGS) -c -o $@ $<
 
 $(OUTPUT_DIRECTORY)/CBORTest.c: $(ALL_KRML_FILES)
-	$(KRML_HOME)/krml $(KRML_OPTS) -warn-error @1..27 -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C=CBOR.\*[rename=CBORDetAPI]' -bundle 'CBORTest.C=\*[rename=CBORTest]' -add-include '"CBORDetAbstract.h"' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBORTest.C -tmpdir $(OUTPUT_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^
+	$(KRML_EXE) $(KRML_OPTS) -warn-error @1..27 -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C=CBOR.\*[rename=CBORDetAPI]' -bundle 'CBORTest.C=\*[rename=CBORTest]' -add-include '"CBORDetAbstract.h"' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBORTest.C -tmpdir $(OUTPUT_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^
 
 $(OUTPUT_DIRECTORY)/CBORTest.rs: $(ALL_KRML_FILES)
-	$(KRML_HOME)/krml $(KRML_OPTS) -backend rust -fno-box -fkeep-tuples -fcontained-type cbor_raw_iterator -warn-error @1..27 -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C=CBOR.\*[rename=CBORDetAPI]' -bundle 'CBORTest.Rust=\*[rename=CBORTest]' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBORTest.C -tmpdir $(OUTPUT_DIRECTORY) -skip-compilation $^
+	$(KRML_EXE) $(KRML_OPTS) -backend rust -fno-box -fkeep-tuples -fcontained-type cbor_raw_iterator -warn-error @1..27 -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C=CBOR.\*[rename=CBORDetAPI]' -bundle 'CBORTest.Rust=\*[rename=CBORTest]' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBORTest.C -tmpdir $(OUTPUT_DIRECTORY) -skip-compilation $^
 
 test: extract
 	$(OUTPUT_DIRECTORY)/test.exe

diff --git a/src/cbor/pulse/krml/Makefile b/src/cbor/pulse/krml/Makefile
@@ -24,17 +24,17 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile
 
 $(NONDET_C_DIRECTORY)/CBORNondet.c: $(filter-out %CBOR_Pulse_API_Det_Rust.krml %CBOR_Pulse_API_Det_C.krml,$(ALL_KRML_FILES))
 	mkdir -p $(dir $@)
-	$(KRML_HOME)/krml $(KRML_OPTS) -faggressive-inlining -fnoshort-names -warn-error @1..27 -skip-linking -bundle 'CBOR.Pulse.API.Nondet.Type=CBOR.Pulse.Raw.Type,Pulse.Lib.Slice,CBOR.Pulse.Raw.Iterator.Base,CBOR.Pulse.Raw.Iterator,CBOR.Spec.Raw.Base[rename=CBORNondetType]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Nondet.C=\*[rename=CBORNondet]' -no-prefix CBOR.Pulse.API.Nondet.C -no-prefix CBOR.Pulse.API.Nondet.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Nondet.Type -no-prefix CBOR.Pulse.Raw.Type -tmpdir $(NONDET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation -fextern-c -fparentheses $^
+	$(KRML_EXE) $(KRML_OPTS) -faggressive-inlining -fnoshort-names -warn-error @1..27 -skip-linking -bundle 'CBOR.Pulse.API.Nondet.Type=CBOR.Pulse.Raw.Type,Pulse.Lib.Slice,CBOR.Pulse.Raw.Iterator.Base,CBOR.Pulse.Raw.Iterator,CBOR.Spec.Raw.Base[rename=CBORNondetType]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Nondet.C=\*[rename=CBORNondet]' -no-prefix CBOR.Pulse.API.Nondet.C -no-prefix CBOR.Pulse.API.Nondet.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Nondet.Type -no-prefix CBOR.Pulse.Raw.Type -tmpdir $(NONDET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation -fextern-c -fparentheses $^
 
 $(DET_C_DIRECTORY)/CBORDet.c: $(filter-out %CBOR_Pulse_API_Det_Rust.krml,$(ALL_KRML_FILES))
 	mkdir -p $(dir $@)
-	$(KRML_HOME)/krml $(KRML_OPTS) -faggressive-inlining -warn-error @1..27 -skip-linking -bundle 'CBOR.Spec.Constants+CBOR.Pulse.Raw.Type+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C+CBOR.Pulse.API.Det.C.Copy=\*[rename=CBORDet]' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Pulse.Raw.Type -no-prefix CBOR.Pulse.API.Det.C.Copy -no-prefix CBOR.Pulse.Raw.Copy -tmpdir $(DET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation -fextern-c -fparentheses $^
+	$(KRML_EXE) $(KRML_OPTS) -faggressive-inlining -warn-error @1..27 -skip-linking -bundle 'CBOR.Spec.Constants+CBOR.Pulse.Raw.Type+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C+CBOR.Pulse.API.Det.C.Copy=\*[rename=CBORDet]' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Pulse.Raw.Type -no-prefix CBOR.Pulse.API.Det.C.Copy -no-prefix CBOR.Pulse.Raw.Copy -tmpdir $(DET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation -fextern-c -fparentheses $^
 
 $(DET_RUST_DIRECTORY)/cbordetver.rs: $(filter-out %CBOR_Pulse_API_Det_C.krml,$(ALL_KRML_FILES))
-	$(KRML_HOME)/krml $(KRML_OPTS) -backend rust -fno-box -fkeep-tuples -fcontained-type cbor_raw_iterator -warn-error @1..27 -skip-linking -bundle 'CBOR.Pulse.API.Det.Rust=[rename=CBORDetVer]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.Raw.Type+CBOR.Pulse.API.Det.Type=\*[rename=CBORDetVerAux]' -tmpdir $(DET_RUST_DIRECTORY) -skip-compilation $^
+	$(KRML_EXE) $(KRML_OPTS) -backend rust -fno-box -fkeep-tuples -fcontained-type cbor_raw_iterator -warn-error @1..27 -skip-linking -bundle 'CBOR.Pulse.API.Det.Rust=[rename=CBORDetVer]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.Raw.Type+CBOR.Pulse.API.Det.Type=\*[rename=CBORDetVerAux]' -tmpdir $(DET_RUST_DIRECTORY) -skip-compilation $^
 
 $(NONDET_RUST_DIRECTORY)/cbornondetver.rs: $(filter-out %CBOR_Pulse_API_Det_C.krml %CBOR_Pulse_API_Det_Rust.krml %CBOR_Pulse_API_Nondet_C.krml,$(ALL_KRML_FILES))
-	$(KRML_HOME)/krml $(KRML_OPTS) -backend rust -fno-box -fkeep-tuples -fcontained-type cbor_raw_iterator -warn-error @1..27 -skip-linking -bundle 'CBOR.Pulse.API.Nondet.Rust=[rename=CBORNondetVer]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.Raw.Type+CBOR.Pulse.API.Nondet.Type=\*[rename=CBORNondetVerAux]' -tmpdir $(NONDET_RUST_DIRECTORY) -skip-compilation $^
+	$(KRML_EXE) $(KRML_OPTS) -backend rust -fno-box -fkeep-tuples -fcontained-type cbor_raw_iterator -warn-error @1..27 -skip-linking -bundle 'CBOR.Pulse.API.Nondet.Rust=[rename=CBORNondetVer]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.Raw.Type+CBOR.Pulse.API.Nondet.Type=\*[rename=CBORNondetVerAux]' -tmpdir $(NONDET_RUST_DIRECTORY) -skip-compilation $^
 
 extract-krml: $(ALL_KRML_FILES)
 

diff --git a/src/cbor/pulse/krml/h.Makefile b/src/cbor/pulse/krml/h.Makefile
@@ -21,12 +21,12 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile
 
 $(NONDET_C_DIRECTORY)/CBORNondetBase.h: $(filter-out %CBOR_Pulse_API_Det_Rust.krml %CBOR_Pulse_API_Det_C.krml,$(ALL_KRML_FILES))
 	mkdir -p $(dir $@)
-	$(KRML_HOME)/krml $(KRML_OPTS) -faggressive-inlining -fnoshort-names -warn-error @1..27 -skip-linking -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Nondet.Type+CBOR.Pulse.API.Nondet.C=\*[rename=CBORNondetBase]' -no-prefix CBOR.Pulse.API.Nondet.C -no-prefix CBOR.Pulse.API.Nondet.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Nondet.Type -tmpdir $(NONDET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^
+	$(KRML_EXE) $(KRML_OPTS) -faggressive-inlining -fnoshort-names -warn-error @1..27 -skip-linking -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Nondet.Type+CBOR.Pulse.API.Nondet.C=\*[rename=CBORNondetBase]' -no-prefix CBOR.Pulse.API.Nondet.C -no-prefix CBOR.Pulse.API.Nondet.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Nondet.Type -tmpdir $(NONDET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^
 	test ! -e $(basename $@).c
 
 $(DET_C_DIRECTORY)/CBORDetBase.h: $(filter-out %CBOR_Pulse_API_Det_Rust.krml,$(ALL_KRML_FILES))
 	mkdir -p $(dir $@)
-	$(KRML_HOME)/krml $(KRML_OPTS) -faggressive-inlining -warn-error @1..27 -skip-linking -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C+CBOR.Pulse.API.Det.C.Copy=\*[rename=CBORDetBase]' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Pulse.API.Det.C.Copy -tmpdir $(DET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^
+	$(KRML_EXE) $(KRML_OPTS) -faggressive-inlining -warn-error @1..27 -skip-linking -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C+CBOR.Pulse.API.Det.C.Copy=\*[rename=CBORDetBase]' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Pulse.API.Det.C.Copy -tmpdir $(DET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^
 	test ! -e $(basename $@).c
 
 extract: $(NONDET_C_DIRECTORY)/CBORNondetBase.h $(DET_C_DIRECTORY)/CBORDetBase.h

diff --git a/src/cbor/pulse/raw/extract-det-type.Makefile b/src/cbor/pulse/raw/extract-det-type.Makefile
@@ -16,4 +16,4 @@ include $(EVERPARSE_SRC_PATH)/karamel.Makefile
 .PHONY: extract
 
 extract: $(ALL_KRML_FILES)
-	$(KRML_HOME)/krml -bundle 'CBOR.Pulse.API.Det.Type=\*' -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -tmpdir $(OUTPUT_DIRECTORY) -skip-compilation $^
+	$(KRML_EXE) -bundle 'CBOR.Pulse.API.Det.Type=\*' -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -tmpdir $(OUTPUT_DIRECTORY) -skip-compilation $^
diff --git a/src/cddl/pulse/Makefile b/src/cddl/pulse/Makefile
@@ -14,7 +14,7 @@ include $(EVERPARSE_SRC_PATH)/karamel.Makefile
 include $(EVERPARSE_SRC_PATH)/pulse.Makefile
 include $(EVERPARSE_SRC_PATH)/common.Makefile
 
-KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE)
+KRML=$(KRML_EXE) -fstar $(FSTAR_EXE)
 
 extract: $(ALL_KRML_FILES)
 #	$(KRML) -bundle CBOR.Spec.Constants+CBOR.Pulse.Type+CBOR.Pulse.Extern=[rename=CBOR] -no-prefix CBOR.Spec.Constants,CBOR.Pulse.Type,CBOR.Pulse.Extern -bundle CDDL.Pulse.Test=*[rename=CDDLExtractionTest] -skip-linking $^ -tmpdir $(OUTPUT_DIRECTORY)

diff --git a/src/cddl/tests/demo/extract.Makefile b/src/cddl/tests/demo/extract.Makefile
@@ -19,7 +19,7 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile
 
 KRML_OPTS += -warn-error @4@6
 
-KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS)
+KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS)
 
 $(OUTPUT_DIRECTORY)/CDDLExtractionTest.o: $(ALL_KRML_FILES)
 	$(KRML) -fnoshort-enums -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C=CBOR.\*[rename=CBORDetAPI]'  -bundle CDDLTest.Client+CDDLTest.Test=*[rename=CDDLExtractionTest] -add-include '"CBORDetAbstract.h"' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants  -skip-linking -skip-makefiles $^ -tmpdir $(OUTPUT_DIRECTORY) -I $(EVERPARSE_SRC_PATH)/cbor/pulse/det/c

diff --git a/src/cddl/tests/dpe/dpe/Makefile b/src/cddl/tests/dpe/dpe/Makefile
@@ -35,7 +35,7 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile
 
 KRML_OPTS += -warn-error @4@6
 
-KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS)
+KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS)
 
 extract: $(ALL_KRML_FILES)
 	$(KRML) -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C=CBOR.\*[rename=CBORDetAPI]'  -bundle CDDLTest.DPEMain=*[rename=CDDLExtractionTest] -add-include '"CBORDetAbstract.h"' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -skip-linking -skip-makefiles $^ -tmpdir $(OUTPUT_DIRECTORY) -I $(EVERPARSE_SRC_PATH)/cbor/pulse/det/c

diff --git a/src/cddl/tests/dpe/extract0.Makefile b/src/cddl/tests/dpe/extract0.Makefile
@@ -16,7 +16,7 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile
 
 KRML_OPTS += -warn-error @4@6
 
-KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS)
+KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS)
 
 extract: $(ALL_KRML_FILES)
 	$(KRML) -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C=CBOR.\*[rename=CBORDetAPI]'  -bundle CDDLTest.Test=*[rename=CDDLExtractionTest] -add-include '"CBORDetAbstract.h"' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -skip-linking $^ -tmpdir $(OUTPUT_DIRECTORY) -I $(EVERPARSE_SRC_PATH)/cbor/pulse/det/c

diff --git a/src/cddl/tests/rust/extract.Makefile b/src/cddl/tests/rust/extract.Makefile
@@ -19,7 +19,7 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile
 
 #KRML_OPTS += -warn-error @4@6
 
-KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS)
+KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS)
 
 extract: $(ALL_KRML_FILES)
 	$(KRML) -backend rust -fno-box -fkeep-tuples -fcontained-type cbor_raw_iterator -warn-error @1..27 -skip-linking -bundle 'CDDLTest.Test=[rename=CDDLExtractionTest]' -bundle 'CBOR.Pulse.API.Det.Rust=[rename=CBORDetVer]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.Raw.Type+CBOR.Pulse.API.Det.Type=\*[rename=CBORDetVerAux]' -tmpdir $(OUTPUT_DIRECTORY) -skip-compilation $^

diff --git a/src/cddl/tests/unit/Makefile b/src/cddl/tests/unit/Makefile
@@ -82,7 +82,7 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile
 
 KRML_OPTS += -warn-error @4@6
 
-KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS)
+KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS)
 
 CBOR_KRML_FILES = $(patsubst %,%.krml,$(subst .,_,$(CBOR_KRML_MODULES)))