Skip to content

Commit ec5413a

Browse files
digama0digama0
authored
add test suite and CI (#55)
* add test suite * trim first & last line from expected * add documentation * add CI * clearly delimit diffs * more tests * add command line argument to set the metamath call * add env var diagnostic * common code * use quoted heredoc * include test.mm in output * another test
1 parent 1849c23 commit ec5413a

20 files changed

+282
-0
lines changed

‎.github/workflows/build.yml‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
on:
2+
push:
3+
pull_request:
4+
5+
name: ci
6+
7+
jobs:
8+
build:
9+
name: Build
10+
runs-on: ubuntu-latest
11+
steps:
12+
- uses: actions/checkout@v2
13+
14+
- name: build
15+
working-directory: build
16+
run: ./build.sh
17+
18+
- name: test
19+
working-directory: tests
20+
run: env METAMATH=../build/metamath ./run_test.sh *.in

‎.gitignore‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,3 +26,5 @@ configure.ac2
2626
# Doxygen related: configuration file and destination folder
2727
Doxyfile
2828
doc/doxy
29+
build/
30+
*.produced

‎tests/empty.expected‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
MM> READ "empty.mm"
2+
Reading source file "empty.mm"... 1 bytes
3+
1 bytes were read into the source buffer.
4+
The source has 0 statements; 0 are $a and 0 are $p.
5+
No errors were found. However, proofs were not checked. Type VERIFY PROOF *
6+
if you want to check them.
7+
MM> 0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%
8+
9+
All proofs in the database were verified.

‎tests/empty.in‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
ve p *

‎tests/empty.mm‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+

‎tests/empty_cmd.expected‎

Whitespace-only changes.

‎tests/empty_cmd.in‎

Whitespace-only changes.

‎tests/run_test.sh‎

Lines changed: 151 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,151 @@
1+
#!/bin/sh
2+
3+
usage() {
4+
cat >&2 << "HELP"
5+
Usage: run_test [-c CMD] [--bless] TESTS...
6+
Run tests from the test suite.
7+
8+
Each TEST should be the name of a TEST.in file in the current directory.
9+
It calls 'metamath TEST.mm < TEST.in > TEST.produced' and compares
10+
TEST.produced with TEST.expected, printing a test failure report.
11+
12+
If TEST.mm does not exist, then it just calls metamath without arguments.
13+
14+
The 'metamath' command can be modified by setting the METAMATH environment
15+
variable, or via the '-c CMD' option (which takes priority).
16+
17+
The --bless option can be used to update the TEST.expected file to match
18+
TEST.produced. Always review the changes after a call to run_test --bless.
19+
20+
TEST.in files have the syntax of metamath scripts, so leading ! can be used to
21+
write comments. This script contains some special directives in tests:
22+
23+
* '! run_test' means that the output will be ignored: TEST.produced will not be
24+
created and TEST.expected does not have to exist.
25+
* '! expect_fail' means that we expect metamath to return exit code 1
26+
instead of 0 on this input.
27+
HELP
28+
}
29+
30+
if [ "$1" = "--help" ]; then usage; exit; fi
31+
32+
# Allow overriding the 'metamath' command using the METAMATH env variable
33+
cmd="${METAMATH:-metamath}"
34+
35+
# Alternatively, use the '-c metamath' argument which overrides the env variable
36+
if [ "$1" = "-c" ]; then shift; cmd=$1; shift; fi
37+
38+
if [ "$1" = "--bless" ]; then bless=1; shift; fi
39+
40+
# Check that the 'metamath' command actually exists
41+
if ! [ -x "$(command -v "$cmd")" ]; then
42+
echo >&2 "'$cmd' not found on the PATH."
43+
if [ "$METAMATH" != "" ]; then
44+
echo >&2 "note: The METAMATH enviroment variable is set to '$METAMATH'."
45+
fi
46+
echo >&2 "Try 'METAMATH=path/to/metamath ./run_test.sh ...', or check your installation"
47+
exit 2
48+
fi
49+
50+
# color codes
51+
red='\033[0;31m'
52+
green='\033[0;32m'
53+
cyan='\033[0;36m'
54+
white='\033[0;37m'
55+
off='\033[0m'
56+
57+
# set to 1 if any test fails
58+
exit_code=0
59+
# set to 1 if rerunning with --bless would help
60+
needs_bless=0
61+
62+
for test in "$@"; do
63+
# strip .in from the test name if necessary
64+
test=$(basename "$test" .in)
65+
66+
# The test file input is the only required part.
67+
# If it doesn't exist then it's a hard error and we abort the test run
68+
if [ ! -f "$test.in" ]; then echo >&2 "$test.in ${red}missing${off}"; exit 2; fi
69+
70+
# For tests with `! run_test` in them, we want to ignore the output
71+
if grep -q "! run_test" "$test.in"; then
72+
outfile="/dev/null"
73+
else
74+
outfile="$test.produced"
75+
fi
76+
77+
# For tests with `! expect_fail` we expect exit code 1 instead of 0
78+
! grep -q "! expect_fail" "$test.in"; expect=$?
79+
80+
# Actually run the program
81+
if [ -f "$test.mm" ]; then
82+
echo -n "test ${white}$test${off}.in + $test.mm: "
83+
result=$("$cmd" "$test.mm" < "$test.in")
84+
else
85+
echo -n "test ${white}$test${off}.in: "
86+
result=$("$cmd" < "$test.in")
87+
fi
88+
# exit code stored in $?
89+
90+
if [ $? -ne $expect ]; then
91+
# If the exit code is wrong, the test is a failure and --bless won't help
92+
echo "${red}failed${off}"; exit_code=1; continue
93+
fi
94+
95+
# Strip the first and last line of the output.
96+
# The first line is always something like:
97+
# Metamath - Version 0.199.pre 7-Aug-2021 Type HELP for help, EXIT to exit.
98+
# which is problematic because we would have to fix all the tests every time
99+
# a new version comes out.
100+
# The last line is always 'MM> EXIT' which is not relevant.
101+
echo "$result" | head -n -1 | tail -n +2 > "$outfile"
102+
103+
if [ "$outfile" = "/dev/null" ]; then
104+
# If this is a run_test then we're done
105+
echo "${green}ok${off}"
106+
elif [ ! -f "$test.expected" ]; then
107+
# If the $test.expected file doesn't exist:
108+
if [ "$bless" = "1" ]; then
109+
# if we are in bless mode then copy the $test.produced and report success
110+
echo "${cyan}blessed${off}"
111+
cp "$test.produced" "$test.expected"
112+
echo "$test.expected:"
113+
else
114+
# otherwise this is a fail, and blessing will help
115+
echo "${red}failed${off}"; exit_code=1; needs_bless=1
116+
echo "$test.expected missing, $test.produced:"
117+
fi
118+
echo -n "---------------------------------------\n${green}"
119+
cat "$test.produced"
120+
echo "${off}---------------------------------------\n"
121+
# call diff and put the diff output in $diff_result
122+
elif diff_result=$(diff "$test.expected" "$outfile" --color=always); then
123+
# If it succeeded (the files are the same), then the test passed
124+
echo "${green}ok${off}"
125+
else
126+
if [ "$bless" = "1" ]; then
127+
# If the files are different but we are in bless mode then it's still okay,
128+
# but report that we've modified the $test.expected file
129+
echo "${cyan}blessed${off}"
130+
cp "$test.produced" "$test.expected"
131+
echo "$test.expected changes:"
132+
else
133+
# If the files are different and we aren't in bless mode
134+
# then this is a fail, but blessing will help
135+
echo "${red}failed${off}"; exit_code=1; needs_bless=1
136+
137+
# Give a verbose error report, including the file names being diffed
138+
echo "$test.expected and $test.produced differ"
139+
fi
140+
echo "---------------------------------------"
141+
echo "$diff_result"
142+
echo "---------------------------------------\n"
143+
fi
144+
done
145+
146+
# Remind the user about the --bless option if it looks like it might help
147+
if [ $needs_bless -eq 1 ]; then
148+
echo "run './run_test.sh --bless *.in' to update the test suite"
149+
fi
150+
151+
exit $exit_code

‎tests/verify_markup_1.expected‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
MM> READ "verify_markup_1.mm"
2+
Reading source file "verify_markup_1.mm"... 196 bytes
3+
196 bytes were read into the source buffer.
4+
The source has 4 statements; 0 are $a and 1 are $p.
5+
No errors were found. However, proofs were not checked. Type VERIFY PROOF *
6+
if you want to check them.
7+
MM> Checking statement label conventions...
8+
Checking latexdef, htmldef, althtmldef...
9+
Checking statement comments...
10+
?Warning: There is no "(Contributed by...)" in the comment above statement 4,
11+
label "ok".
12+
Checking section header comments...
13+
Checking bibliographic references...
14+
Checking mathbox independence...

‎tests/verify_markup_1.in‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
ve m *

0 commit comments

Comments
 (0)