summaryrefslogtreecommitdiff
path: root/tests/betree
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/betree/Makefile21
1 files changed, 10 insertions, 11 deletions
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: