From 3706dce39ac8c1f4e85dedf55f6013fb68474059 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 7 Feb 2025 13:11:46 -0800
Subject: [PATCH] test.mk: Make sure to be silent on error output tests

---
 mk/test.mk                               | 8 ++++----
 tests/error-messages/Makefile            | 3 ---
 tests/vale/DeltaAttr.fst.output.expected | 2 --
 3 files changed, 4 insertions(+), 9 deletions(-)

diff --git a/mk/test.mk b/mk/test.mk
index e05180aac1a..dcff34a958c 100644
--- 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
index b431deb8697..2a3fbe18f43 100644
--- 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
index 3b0a7f24cd0..af16be38e6b 100644
--- 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