No --cmi

Author: mtzguido

book/tutorial/Makefile

@@ -44,12 +44,10 @@ FSTAR_EXTRACT = --extract 'OCaml:-* +Spec'
 # - 241: stale dependencies, almost always a sign that the build is incorrect
 #
 # But also:
-# - --cmi, for cross-module inlining, a must-have for anyone who relies on
-#   inline_for_extraction in the presence of interfaces
 # - --cache_dir, to place checked files there
 
 FSTAR_NO_FLAGS = $(FSTAR_EXE) --ext optimize_let_vc \
-  --odir obj $(FSTAR_INCLUDES) --cmi \
+  --odir obj $(FSTAR_INCLUDES) \
   --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \
   --cache_dir obj
 

krmllib/Makefile

@@ -47,7 +47,7 @@ ifneq ($(RESOURCEMONITOR),)
 endif
 
 FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_dir obj \
-  $(addprefix --include , $(INCLUDE_PATHS)) --cmi \
+  $(addprefix --include , $(INCLUDE_PATHS)) \
   --already_cached 'Prims FStar -FStar.Krml.Endianness LowStar -LowStar.Lib'
 
 # Note: not compatible with the OPAM layout until fstar can be queried for the

test/Makefile

@@ -88,7 +88,7 @@ FSTAR		= $(FSTAR_EXE) \
   $(INCLUDE_CRYPTO) --include ../book --include ../book/notfslit --ext optimize_let_vc \
   --already_cached 'Prims FStar C TestLib Spec.Loops -C.Compat -C.Nullity LowStar WasmSupport' \
   --trivial_pre_for_unannotated_effectful_fns false \
-  --cmi --warn_error -274
+  --warn_error -274
 
 all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test rust-val-test bundle-test rust-propererasure-bundle-test
 

test/bundle/Makefile

@@ -36,13 +36,11 @@ include Makefile.include
 # - 241: stale dependencies, almost always a sign that the build is incorrect
 #
 # But also:
-# - --cmi, for cross-module inlining, a must-have for anyone who relies on
-#   inline_for_extraction in the presence of interfaces
 # - --cache_dir, to place checked files there
 
 FSTAR_EXE ?= fstar.exe
 FSTAR_NO_FLAGS = $(FSTAR_EXE) \
-  --odir obj $(FSTAR_INCLUDES) --cmi \
+  --odir obj $(FSTAR_INCLUDES) \
   --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \
   --cache_dir obj
 

test/rust-propererasure-bundle/Makefile

@@ -18,7 +18,7 @@ FSTAR		= $(FSTAR_EXE) --cache_checked_modules \
   --ext optimize_let_vc \
   --already_cached 'Prims FStar C TestLib Spec.Loops -C.Compat -C.Nullity LowStar WasmSupport' \
   --trivial_pre_for_unannotated_effectful_fns false \
-  --cmi --warn_error -274
+  --warn_error -274
 SED=$(shell which gsed >/dev/null 2>&1 && echo gsed || echo sed)
 
 all: derived.rust-test

test/rust-val/Makefile

@@ -20,7 +20,7 @@ FSTAR		= $(FSTAR_EXE) --cache_checked_modules \
   --ext optimize_let_vc \
   --already_cached 'Prims FStar C TestLib Spec.Loops -C.Compat -C.Nullity LowStar WasmSupport' \
   --trivial_pre_for_unannotated_effectful_fns false \
-  --cmi --warn_error -274
+  --warn_error -274
 SED=$(shell which gsed >/dev/null 2>&1 && echo gsed || echo sed)
 
 all: rusttest.rust-test impl

test/rust-val/impl/Makefile

@@ -19,7 +19,7 @@ FSTAR		= $(FSTAR_EXE) --cache_checked_modules \
   --ext optimize_let_vc \
   --already_cached 'Prims FStar C TestLib Spec.Loops -C.Compat -C.Nullity LowStar WasmSupport' \
   --trivial_pre_for_unannotated_effectful_fns false \
-  --cmi --warn_error -274
+  --warn_error -274
 SED=$(shell which gsed >/dev/null 2>&1 && echo gsed || echo sed)
 
 all: auxiliary.rust-test

test/sepcomp/a/Makefile

@@ -36,13 +36,11 @@ include Makefile.include
 # - 241: stale dependencies, almost always a sign that the build is incorrect
 #
 # But also:
-# - --cmi, for cross-module inlining, a must-have for anyone who relies on
-#   inline_for_extraction in the presence of interfaces
 # - --cache_dir, to place checked files there
 
 FSTAR_EXE ?= fstar.exe
 FSTAR_NO_FLAGS = $(FSTAR_EXE) \
-  --odir obj $(FSTAR_INCLUDES) --cmi \
+  --odir obj $(FSTAR_INCLUDES) \
   --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \
   --cache_dir obj
 

test/sepcomp/b/Makefile

@@ -36,13 +36,11 @@ include Makefile.include
 # - 241: stale dependencies, almost always a sign that the build is incorrect
 #
 # But also:
-# - --cmi, for cross-module inlining, a must-have for anyone who relies on
-#   inline_for_extraction in the presence of interfaces
 # - --cache_dir, to place checked files there
 
 FSTAR_EXE ?= fstar.exe
 FSTAR_NO_FLAGS = $(FSTAR_EXE) \
-  --odir obj $(FSTAR_INCLUDES) --cmi \
+  --odir obj $(FSTAR_INCLUDES) \
   --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport A' --warn_error '+241@247+285' \
   --cache_dir obj