Merge pull request #536 from mtzguido/simpl

Simplify Makefiles after F* changes

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

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

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) #

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
 # --------

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
 # --------