From 6b00a7552f288de5061b77bf132e6abad854eaec Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 27 Sep 2023 21:29:42 -0400 Subject: [PATCH] fix tests --- tests/anatomy.expected | 2 +- tests/big-unifier.expected | 2 +- tests/demo0-includer.expected | 2 +- tests/demo0.expected | 2 +- tests/disjoint1.expected | 2 +- tests/disjoint2.expected | 2 +- tests/disjoint3.expected | 2 +- tests/empty.expected | 2 +- tests/local-var-bad.expected | 2 +- tests/local-var-good.expected | 2 +- tests/missing-dollar-p.expected | 2 +- tests/nuniq-gram.expected | 2 +- tests/run_test.sh | 5 ++++- 13 files changed, 16 insertions(+), 13 deletions(-) diff --git a/tests/anatomy.expected b/tests/anatomy.expected index e7c1a88d..e09a7195 100644 --- 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 index f1b3f192..1034564f 100644 --- 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 index 0b387213..91e63519 100644 --- 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 index 86a2a4f8..3968bd2e 100644 --- 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 index af757ea9..05cff87b 100644 --- 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 index 4656232a..d388ad26 100644 --- 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 index 69e2b2dc..9902f01f 100644 --- 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 index ca6d025f..439d8574 100644 --- 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 index 33ed4fd5..d59522eb 100644 --- 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 index 4ef7227c..a11c8f94 100644 --- 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 index 772ce7a8..bc70d224 100644 --- 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 index 816afd21..327397e6 100644 --- 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 index ad83e3a7..052782f1 100755 --- 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