Fix Makefiles

5 files changed, 50 insertions, 55 deletions

diff --git a/tests/Makefile.template b/tests/Makefile.template
index ea838d2d..a16b0edb 100644
--- a/tests/Makefile.template
+++ b/tests/Makefile.template
@@ -5,17 +5,19 @@ FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
 FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
 
 FSTAR_OPTIONS = $(FSTAR_HINTS) \
-  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
   --warn_error '+241@247+285-274' \
-  --cache_dir obj
 
-FSTAR_NO_FLAGS = fstar.exe
+FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
 
 FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
 
 # The F* roots are used to compute the dependency graph, and generate the .depend file
 FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
 
+# Build all the files
+all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS)))
+
 # This is the right way to ensure the .depend file always gets re-built.
 ifeq (,$(filter %-in,$(MAKECMDGOALS)))
 ifndef NODEPEND
@@ -32,16 +34,13 @@ include .depend
 endif
 
 # For the interactive mode
-%.fst %.fsti:
-	$(FSTAR) $@
+%.fst-in %.fsti-in:
+	@echo $(FSTAR_OPTIONS)
 
-# Generete the .checked files in bash mode
+# Generete the .checked files in batch mode
 %.checked:
-	$(FSTAR) $(FSTAR_FLAGS) $* && \
-	touch -c $*
-
-# Build all the files
-all: $(ALL_CHECKED_FILES)
+	$(FSTAR) $(FSTAR_OPTIONS) $< && \
+	touch -c $@
 
 .PHONY: clean
 clean:
diff --git a/tests/betree/Makefile b/tests/betree/Makefile
index ea838d2d..a16b0edb 100644
--- a/tests/betree/Makefile
+++ b/tests/betree/Makefile
@@ -5,17 +5,19 @@ FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
 FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
 
 FSTAR_OPTIONS = $(FSTAR_HINTS) \
-  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
   --warn_error '+241@247+285-274' \
-  --cache_dir obj
 
-FSTAR_NO_FLAGS = fstar.exe
+FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
 
 FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
 
 # The F* roots are used to compute the dependency graph, and generate the .depend file
 FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
 
+# Build all the files
+all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS)))
+
 # This is the right way to ensure the .depend file always gets re-built.
 ifeq (,$(filter %-in,$(MAKECMDGOALS)))
 ifndef NODEPEND
@@ -32,16 +34,13 @@ include .depend
 endif
 
 # For the interactive mode
-%.fst %.fsti:
-	$(FSTAR) $@
+%.fst-in %.fsti-in:
+	@echo $(FSTAR_OPTIONS)
 
-# Generete the .checked files in bash mode
+# Generete the .checked files in batch mode
 %.checked:
-	$(FSTAR) $(FSTAR_FLAGS) $* && \
-	touch -c $*
-
-# Build all the files
-all: $(ALL_CHECKED_FILES)
+	$(FSTAR) $(FSTAR_OPTIONS) $< && \
+	touch -c $@
 
 .PHONY: clean
 clean:
diff --git a/tests/hashmap/Makefile b/tests/hashmap/Makefile
index ea838d2d..a16b0edb 100644
--- a/tests/hashmap/Makefile
+++ b/tests/hashmap/Makefile
@@ -5,17 +5,19 @@ FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
 FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
 
 FSTAR_OPTIONS = $(FSTAR_HINTS) \
-  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
   --warn_error '+241@247+285-274' \
-  --cache_dir obj
 
-FSTAR_NO_FLAGS = fstar.exe
+FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
 
 FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
 
 # The F* roots are used to compute the dependency graph, and generate the .depend file
 FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
 
+# Build all the files
+all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS)))
+
 # This is the right way to ensure the .depend file always gets re-built.
 ifeq (,$(filter %-in,$(MAKECMDGOALS)))
 ifndef NODEPEND
@@ -32,16 +34,13 @@ include .depend
 endif
 
 # For the interactive mode
-%.fst %.fsti:
-	$(FSTAR) $@
+%.fst-in %.fsti-in:
+	@echo $(FSTAR_OPTIONS)
 
-# Generete the .checked files in bash mode
+# Generete the .checked files in batch mode
 %.checked:
-	$(FSTAR) $(FSTAR_FLAGS) $* && \
-	touch -c $*
-
-# Build all the files
-all: $(ALL_CHECKED_FILES)
+	$(FSTAR) $(FSTAR_OPTIONS) $< && \
+	touch -c $@
 
 .PHONY: clean
 clean:
diff --git a/tests/hashmap_on_disk/Makefile b/tests/hashmap_on_disk/Makefile
index ea838d2d..a16b0edb 100644
--- a/tests/hashmap_on_disk/Makefile
+++ b/tests/hashmap_on_disk/Makefile
@@ -5,17 +5,19 @@ FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
 FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
 
 FSTAR_OPTIONS = $(FSTAR_HINTS) \
-  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
   --warn_error '+241@247+285-274' \
-  --cache_dir obj
 
-FSTAR_NO_FLAGS = fstar.exe
+FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
 
 FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
 
 # The F* roots are used to compute the dependency graph, and generate the .depend file
 FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
 
+# Build all the files
+all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS)))
+
 # This is the right way to ensure the .depend file always gets re-built.
 ifeq (,$(filter %-in,$(MAKECMDGOALS)))
 ifndef NODEPEND
@@ -32,16 +34,13 @@ include .depend
 endif
 
 # For the interactive mode
-%.fst %.fsti:
-	$(FSTAR) $@
+%.fst-in %.fsti-in:
+	@echo $(FSTAR_OPTIONS)
 
-# Generete the .checked files in bash mode
+# Generete the .checked files in batch mode
 %.checked:
-	$(FSTAR) $(FSTAR_FLAGS) $* && \
-	touch -c $*
-
-# Build all the files
-all: $(ALL_CHECKED_FILES)
+	$(FSTAR) $(FSTAR_OPTIONS) $< && \
+	touch -c $@
 
 .PHONY: clean
 clean:
diff --git a/tests/misc/Makefile b/tests/misc/Makefile
index ea838d2d..a16b0edb 100644
--- a/tests/misc/Makefile
+++ b/tests/misc/Makefile
@@ -5,17 +5,19 @@ FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
 FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
 
 FSTAR_OPTIONS = $(FSTAR_HINTS) \
-  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
   --warn_error '+241@247+285-274' \
-  --cache_dir obj
 
-FSTAR_NO_FLAGS = fstar.exe
+FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
 
 FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
 
 # The F* roots are used to compute the dependency graph, and generate the .depend file
 FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
 
+# Build all the files
+all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS)))
+
 # This is the right way to ensure the .depend file always gets re-built.
 ifeq (,$(filter %-in,$(MAKECMDGOALS)))
 ifndef NODEPEND
@@ -32,16 +34,13 @@ include .depend
 endif
 
 # For the interactive mode
-%.fst %.fsti:
-	$(FSTAR) $@
+%.fst-in %.fsti-in:
+	@echo $(FSTAR_OPTIONS)
 
-# Generete the .checked files in bash mode
+# Generete the .checked files in batch mode
 %.checked:
-	$(FSTAR) $(FSTAR_FLAGS) $* && \
-	touch -c $*
-
-# Build all the files
-all: $(ALL_CHECKED_FILES)
+	$(FSTAR) $(FSTAR_OPTIONS) $< && \
+	touch -c $@
 
 .PHONY: clean
 clean: