Merge pull request #3606 from mtzguido/fix

test.mk: do not write checked files for output tests
FStarLang · Nov 6, 2024 · b41ea17 · b41ea17
2 parents 2e20e7e + db1ff49
commit b41ea17
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/mk/test.mk b/mk/test.mk
@@ -45,7 +45,7 @@ OUTPUT_DIR ?= _output
 CACHE_DIR ?= _cache
 
 FSTAR = $(FSTAR_EXE) $(SIL) 				\
-	--cache_checked_modules				\
+	$(if $(NO_WRITE_CHECKED),,--cache_checked_modules)		\
 	--odir $(OUTPUT_DIR)				\
 	--cache_dir $(CACHE_DIR)			\
 	--already_cached Prims,FStar			\
@@ -78,18 +78,22 @@ endif
 	$(FSTAR) $<
 	touch -c $@
 
+$(OUTPUT_DIR)/%.fst.output: NO_WRITE_CHECKED=1
 $(OUTPUT_DIR)/%.fst.output: %.fst
 	$(call msg, "OUTPUT", $(basename $(notdir $@)))
 	$(FSTAR) --message_format human -f --print_expected_failures $< >$@ 2>&1
 
+$(OUTPUT_DIR)/%.fsti.output: NO_WRITE_CHECKED=1
 $(OUTPUT_DIR)/%.fsti.output: %.fsti
 	$(call msg, "OUTPUT", $(basename $(notdir $@)))
 	$(FSTAR) --message_format human -f --print_expected_failures $< >$@ 2>&1
 
+$(OUTPUT_DIR)/%.fst.json_output: NO_WRITE_CHECKED=1
 $(OUTPUT_DIR)/%.fst.json_output: %.fst
 	$(call msg, "JSONOUT", $(basename $(notdir $@)))
 	$(FSTAR) --message_format json -f --print_expected_failures $< >$@ 2>&1
 
+$(OUTPUT_DIR)/%.fsti.json_output: NO_WRITE_CHECKED=1
 $(OUTPUT_DIR)/%.fsti.json_output: %.fsti
 	$(call msg, "JSONOUT", $(basename $(notdir $@)))
 	$(FSTAR) --message_format json -f --print_expected_failures $< >$@ 2>&1