From db1ff490603350b76163a980b07cef89d0b5bf64 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Wed, 6 Nov 2024 14:11:44 -0800
Subject: [PATCH] test.mk: do not write checked files for output tests

Since we have both human and json tests, they can clash, and create a
race during CI runs. We also do not need them.
---
 mk/test.mk | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/mk/test.mk b/mk/test.mk
index a3ceaab9dee..9418013d279 100644
--- 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