fix tests

metamath · Sep 28, 2023 · 6b00a75 · 6b00a75
1 parent 98c89f5
commit 6b00a75
Show file tree

Hide file tree

Showing 13 changed files with 16 additions and 13 deletions.
diff --git a/tests/anatomy.expected b/tests/anatomy.expected
@@ -7,4 +7,4 @@ if you want to check them.
 MM> Continuous scrolling is now in effect.
 MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
 ..................................................
-All proofs in the database were verified.
+All proofs in the database were verified in x.xx s.
diff --git a/tests/big-unifier.expected b/tests/big-unifier.expected
@@ -7,4 +7,4 @@ if you want to check them.
 MM> Continuous scrolling is now in effect.
 MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
 ..................................................
-All proofs in the database were verified.
+All proofs in the database were verified in x.xx s.
diff --git a/tests/demo0-includer.expected b/tests/demo0-includer.expected
@@ -8,4 +8,4 @@ if you want to check them.
 MM> Continuous scrolling is now in effect.
 MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
 ..................................................
-All proofs in the database were verified.
+All proofs in the database were verified in x.xx s.
diff --git a/tests/demo0.expected b/tests/demo0.expected
@@ -7,4 +7,4 @@ if you want to check them.
 MM> Continuous scrolling is now in effect.
 MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
 ..................................................
-All proofs in the database were verified.
+All proofs in the database were verified in x.xx s.
diff --git a/tests/disjoint1.expected b/tests/disjoint1.expected
@@ -16,4 +16,4 @@ requires that variables "x" and "y" be disjoint.  But "x" was substituted with
 "x" and "y" was substituted with "x".  These substitutions have variable "x" in
 common.
 
-All proofs in the database were verified.
+All proofs in the database were verified in x.xx s.
diff --git a/tests/disjoint2.expected b/tests/disjoint2.expected
@@ -135,4 +135,4 @@ requires that variables "x" and "y" be disjoint.  But "x" was substituted with
 Variables "w" and "y" do not have a disjoint variable requirement in the
 assertion being proved, "almostgood".
 ...................
-All proofs in the database were verified.
+All proofs in the database were verified in x.xx s.
diff --git a/tests/disjoint3.expected b/tests/disjoint3.expected
@@ -17,4 +17,4 @@ requires that variables "x" and "y" be disjoint.  But "x" was substituted with
 Variables "x" and "y" do not have a disjoint variable requirement in the
 assertion being proved, "bad".
 
-All proofs in the database were verified.
+All proofs in the database were verified in x.xx s.
diff --git a/tests/empty.expected b/tests/empty.expected
@@ -7,4 +7,4 @@ if you want to check them.
 MM> Continuous scrolling is now in effect.
 MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
 
-All proofs in the database were verified.
+All proofs in the database were verified in x.xx s.
diff --git a/tests/local-var-bad.expected b/tests/local-var-bad.expected
@@ -20,4 +20,4 @@ The variable "x" does not appear in an active "$f" statement.
 MM> Continuous scrolling is now in effect.
 MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
 ..................................................
-All proofs in the database were verified.
+All proofs in the database were verified in x.xx s.
diff --git a/tests/local-var-good.expected b/tests/local-var-good.expected
@@ -7,4 +7,4 @@ if you want to check them.
 MM> Continuous scrolling is now in effect.
 MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
 ..................................................
-All proofs in the database were verified.
+All proofs in the database were verified in x.xx s.
diff --git a/tests/missing-dollar-p.expected b/tests/missing-dollar-p.expected
@@ -12,4 +12,4 @@ One error was found.
 MM> Continuous scrolling is now in effect.
 MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
 ..................................................
-All proofs in the database were verified.
+All proofs in the database were verified in x.xx s.
diff --git a/tests/nuniq-gram.expected b/tests/nuniq-gram.expected
@@ -7,4 +7,4 @@ if you want to check them.
 MM> Continuous scrolling is now in effect.
 MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
 ..................................................
-All proofs in the database were verified.
+All proofs in the database were verified in x.xx s.
diff --git a/tests/run_test.sh b/tests/run_test.sh
@@ -109,7 +109,10 @@ for test in "$@"; do
   # which is problematic because we would have to fix all the tests every time
   # a new version comes out.
   # The last line is always 'MM> EXIT' which is not relevant.
-  echo "$result" | head -n -1 | tail -n +2 > "$outfile"
+  # The sed is to redact timings, which are nondeterministic
+  echo "$result" | head -n -1 | tail -n +2 \
+    | sed -e 's/ \+[0-9]\+\.[0-9]\+ s/ x.xx s/g' \
+    > "$outfile"
 
   if [ "$outfile" = "/dev/null" ]; then
     # If this is a run_test then we're done