test.mk: Make sure to be silent on error output tests

mtzguido · Feb 7, 2025 · 3706dce · 3706dce
1 parent fb57af6
commit 3706dce
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 9 deletions.
diff --git a/mk/test.mk b/mk/test.mk
@@ -79,22 +79,22 @@ endif
 $(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
+	$(FSTAR) --message_format human --silent -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
+	$(FSTAR) --message_format human --silent -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
+	$(FSTAR) --message_format json --silent -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
+	$(FSTAR) --message_format json --silent -f --print_expected_failures $< >$@ 2>&1
 
 $(OUTPUT_DIR)/$(subst .,_,%).ml:
 	$(call msg, "EXTRACT", $(basename $(notdir $@)))

diff --git a/tests/error-messages/Makefile b/tests/error-messages/Makefile
@@ -13,9 +13,6 @@ OTHERFLAGS := $(filter-out --query_stats, $(OTHERFLAGS))
 OTHERFLAGS := $(filter-out --hint_info, $(OTHERFLAGS))
 OTHERFLAGS += --ext fstar:no_absolute_paths
 
-# Make sure we are silent
-OTHERFLAGS += --silent
-
 # For these tests, we check that the resugared output
 # matches the expected file. We have to repeat the lines for
 # json_output, sadly.

diff --git a/tests/vale/DeltaAttr.fst.output.expected b/tests/vale/DeltaAttr.fst.output.expected
@@ -173,5 +173,3 @@ let test_5 x = x + 1 - 1 + (x + 1 - 1) <: Prims.int
     "Calc.fst".
   - Rename "Calc.fst" to avoid conflicts.
 
-Verified module: DeltaAttr
-All verification conditions discharged successfully