From 056681b763aeeb1066adccd7c4c8bc28d815ba02 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Tue, 27 Sep 2022 14:46:22 -0700
Subject: Fix Makefiles

---
 tests/betree/Makefile | 21 ++++++++++-----------
 1 file changed, 10 insertions(+), 11 deletions(-)

(limited to 'tests/betree')

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:
-- 
cgit v1.2.3