diff --git a/book/tutorial/Makefile b/book/tutorial/Makefile index b1456e01..5ba570f6 100644 --- a/book/tutorial/Makefile +++ b/book/tutorial/Makefile @@ -46,11 +46,10 @@ FSTAR_EXTRACT = --extract 'OCaml:-* +Spec' # But also: # - --cmi, for cross-module inlining, a must-have for anyone who relies on # 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 +# - --cache_dir, to place checked files there FSTAR_NO_FLAGS = $(FSTAR_EXE) --ext context_pruning \ - --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ + --odir obj $(FSTAR_INCLUDES) --cmi \ --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \ --cache_dir obj @@ -72,7 +71,7 @@ FSTAR_ROOTS = $(wildcard $(addsuffix /*.fsti,$(SOURCE_DIRS))) \ # mtime of the moved files. ifndef MAKE_RESTARTS .depend: .FORCE - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) --output_deps_to $@ + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) -o $@ .PHONY: .FORCE .FORCE: @@ -115,32 +114,22 @@ obj: # up-to-date (checksum matches, file unchanged), but this will confuse # make and result in endless rebuilds. So, we touch that file. %.checked: | obj - $(FSTAR) $< $(FSTAR_FLAGS) && touch -c $@ + $(FSTAR) $(FSTAR_FLAGS) -c $< -o $@ && touch -c $@ # Extraction # ---------- -# A few mismatches here between the dependencies present in the .depend and the -# expected F* invocation. In .depend: -# -# obj/Bignum_Impl.ml: obj/Bignum.Impl.fst.checked ... more dependencies ... -# -# But F* wants (remember that F* searches for source files anywhere on the -# include path): -# -# fstar Bignum.Impl.fst --extract_module BigNum.Impl -# -# We use basename because we may also extract krml files from .fsti.checked -# files (not true for OCaml, we don't extract mlis from fstis). .PRECIOUS: obj/%.ml obj/%.ml: - $(FSTAR) $(notdir $(subst .checked,,$<)) --codegen OCaml \ - --extract_module $(basename $(notdir $(subst .checked,,$<))) + $(FSTAR) --codegen OCaml $< -o $@ +# By default, krml extraction in F* will extract every module into a +# single out.krml file. Make sure to extract the single module we want. .PRECIOUS: obj/%.krml obj/%.krml: - $(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \ - --extract_module $(basename $(notdir $(subst .checked,,$<))) + $(FSTAR) $< --codegen krml \ + --extract_module $(basename $(notdir $(subst .checked,,$<))) \ + -o $@ obj/Specs_Driver.ml: specs/ml/Specs_Driver.ml # This ensures that all the source directories are not polluted with diff --git a/krmllib/Makefile b/krmllib/Makefile index 1cbb6fe9..d119c012 100644 --- a/krmllib/Makefile +++ b/krmllib/Makefile @@ -36,7 +36,7 @@ ifneq ($(RESOURCEMONITOR),) RUNLIM = runlim -p -o $@.runlim endif -FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_checked_modules --cache_dir obj \ +FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_dir obj \ $(addprefix --include , $(INCLUDE_PATHS)) --cmi \ --already_cached 'Prims FStar -FStar.Krml.Endianness LowStar -LowStar.Lib' @@ -64,7 +64,7 @@ FSTAR_EXTRACT+=-FStar.Stubs # This namespace is for interfaces into the compiler ifndef NODEPEND ifndef MAKE_RESTARTS .depend: .FORCE obj - $(FSTAR) $(OTHERFLAGS) --extract '$(FSTAR_EXTRACT)' --dep full $(ROOTS) --output_deps_to $@ + $(FSTAR) $(OTHERFLAGS) --extract '$(FSTAR_EXTRACT)' --dep full $(ROOTS) -o $@ .PHONY: .FORCE .FORCE: @@ -77,15 +77,15 @@ obj: mkdir $@ %.checked: | obj - $(FSTAR) $(OTHERFLAGS) $< && \ + $(FSTAR) $(OTHERFLAGS) -c $< -o $@ && \ touch $@ verify-all: $(ALL_CHECKED_FILES) $(EXTRACT_DIR)/%.krml: | .depend - $(FSTAR) $(OTHERFLAGS) --codegen krml \ + $(FSTAR) $(OTHERFLAGS) $< --codegen krml \ --extract_module $(basename $(notdir $(subst .checked,,$<))) \ - $(notdir $(subst .checked,,$<)) && \ + -o $@ && \ touch -c $@ # We don't extract LowStar.Lib as everything is generic data structures that diff --git a/test/Makefile b/test/Makefile index 66469537..e7cafbff 100644 --- a/test/Makefile +++ b/test/Makefile @@ -74,7 +74,7 @@ OUTPUT_DIR = .output ifneq ($(CRYPTO),) INCLUDE_CRYPTO=--include $(CRYPTO) endif -FSTAR = $(FSTAR_EXE) --cache_checked_modules \ +FSTAR = $(FSTAR_EXE) \ --cache_dir $(CACHE_DIR) --odir $(OUTPUT_DIR) \ --include hello-system --include ../krmllib/compat --include ../krmllib/obj \ --include ../krmllib --include ../runtime \ @@ -99,7 +99,7 @@ ifndef MAKE_RESTARTS ifndef NODEPEND .depend: .FORCE $(FSTAR) --dep full $(subst .wasm-test,.fst,$(WASM_FILES)) $(subst .test,.fst,$(FILES)) \ - $(BROKEN) ../runtime/WasmSupport.fst --extract 'krml:*,-Prims' --output_deps_to $@ + $(BROKEN) ../runtime/WasmSupport.fst --extract 'krml:*,-Prims' -o $@ .PHONY: .FORCE .FORCE: @@ -109,13 +109,14 @@ endif include .depend $(CACHE_DIR)/%.checked: | .depend - $(FSTAR) $(OTHERFLAGS) $< && \ + $(FSTAR) $(OTHERFLAGS) -c $< -o $@ && \ touch $@ $(OUTPUT_DIR)/%.krml: | .depend $(FSTAR) $(OTHERFLAGS) --codegen krml \ --extract_module $(basename $(notdir $(subst .checked,,$<))) \ - $(notdir $(subst .checked,,$<)) + -o $@ \ + $< ############### # Regular (C) # diff --git a/test/sepcomp/a/Makefile b/test/sepcomp/a/Makefile index e32e8cc3..1b496ec9 100644 --- a/test/sepcomp/a/Makefile +++ b/test/sepcomp/a/Makefile @@ -35,12 +35,11 @@ include Makefile.include # But also: # - --cmi, for cross-module inlining, a must-have for anyone who relies on # 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 +# - --cache_dir, to place checked files there FSTAR_EXE ?= fstar.exe FSTAR_NO_FLAGS = $(FSTAR_EXE) \ - --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ + --odir obj $(FSTAR_INCLUDES) --cmi \ --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \ --cache_dir obj @@ -63,7 +62,7 @@ FSTAR_ROOTS = $(wildcard $(addsuffix /*.fsti,$(SOURCE_DIRS))) \ ifndef MAKE_RESTARTS obj/.depend: .FORCE mkdir -p obj - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) --output_deps_to $@ + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) -o $@ .PHONY: .FORCE .FORCE: @@ -106,32 +105,23 @@ obj: # up-to-date (checksum matches, file unchanged), but this will confuse # make and result in endless rebuilds. So, we touch that file. %.checked: | obj - $(FSTAR) $< $(FSTAR_FLAGS) && touch -c $@ + $(FSTAR) $(FSTAR_FLAGS) -c $< -o $@ && touch -c $@ # Extraction # ---------- -# A few mismatches here between the dependencies present in the .depend and the -# expected F* invocation. In .depend: -# -# obj/Bignum_Impl.ml: obj/Bignum.Impl.fst.checked ... more dependencies ... -# -# But F* wants (remember that F* searches for source files anywhere on the -# include path): -# -# fstar Bignum.Impl.fst --extract_module BigNum.Impl -# -# We use basename because we may also extract krml files from .fsti.checked -# files (not true for OCaml, we don't extract mlis from fstis). .PRECIOUS: obj/%.ml obj/%.ml: - $(FSTAR) $(notdir $(subst .checked,,$<)) --codegen OCaml \ - --extract_module $(basename $(notdir $(subst .checked,,$<))) + $(FSTAR) $< --codegen OCaml +# By default, krml extraction in F* will extract every module into a +# single out.krml file. Make sure to extract the single module we want +# to get a single-properly named file. .PRECIOUS: obj/%.krml obj/%.krml: - $(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \ - --extract_module $(basename $(notdir $(subst .checked,,$<))) + $(FSTAR) $< --codegen krml \ + --extract_module $(basename $(notdir $(subst .checked,,$<))) \ + -o $@ # F* --> C # -------- diff --git a/test/sepcomp/b/Makefile b/test/sepcomp/b/Makefile index e8c20d86..1ef3b99b 100644 --- a/test/sepcomp/b/Makefile +++ b/test/sepcomp/b/Makefile @@ -37,12 +37,11 @@ include Makefile.include # But also: # - --cmi, for cross-module inlining, a must-have for anyone who relies on # 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 +# - --cache_dir, to place checked files there FSTAR_EXE ?= fstar.exe FSTAR_NO_FLAGS = $(FSTAR_EXE) \ - --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ + --odir obj $(FSTAR_INCLUDES) --cmi \ --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport A' --warn_error '+241@247+285' \ --cache_dir obj @@ -65,7 +64,7 @@ FSTAR_ROOTS = $(wildcard $(addsuffix /*.fsti,$(SOURCE_DIRS))) \ ifndef MAKE_RESTARTS obj/.depend: .FORCE mkdir -p obj - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) --output_deps_to $@ + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) -o $@ .PHONY: .FORCE .FORCE: @@ -108,32 +107,23 @@ obj: # up-to-date (checksum matches, file unchanged), but this will confuse # make and result in endless rebuilds. So, we touch that file. %.checked: | obj - $(FSTAR) $< $(FSTAR_FLAGS) && touch -c $@ + $(FSTAR) $(FSTAR_FLAGS) -c $< -o $@ && touch -c $@ # Extraction # ---------- -# A few mismatches here between the dependencies present in the .depend and the -# expected F* invocation. In .depend: -# -# obj/Bignum_Impl.ml: obj/Bignum.Impl.fst.checked ... more dependencies ... -# -# But F* wants (remember that F* searches for source files anywhere on the -# include path): -# -# fstar Bignum.Impl.fst --extract_module BigNum.Impl -# -# We use basename because we may also extract krml files from .fsti.checked -# files (not true for OCaml, we don't extract mlis from fstis). .PRECIOUS: obj/%.ml obj/%.ml: - $(FSTAR) $(notdir $(subst .checked,,$<)) --codegen OCaml \ - --extract_module $(basename $(notdir $(subst .checked,,$<))) + $(FSTAR) $< --codegen OCaml +# By default, krml extraction in F* will extract every module into a +# single out.krml file. Make sure to extract the single module we want +# to get a single-properly named file. .PRECIOUS: obj/%.krml obj/%.krml: - $(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \ - --extract_module $(basename $(notdir $(subst .checked,,$<))) + $(FSTAR) $< --codegen krml \ + --extract_module $(basename $(notdir $(subst .checked,,$<))) \ + -o $@ # F* --> C # --------