forked from leanprover-community/repl
-
Notifications
You must be signed in to change notification settings - Fork 0
/
test.sh
executable file
·43 lines (34 loc) · 1.06 KB
/
test.sh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
#!/bin/bash
# Define the paths
IN_DIR="test"
EXPECTED_DIR="test"
lake build
# Iterate over each .in file in the test directory
for infile in $IN_DIR/*.in; do
# Extract the base filename without the extension
base=$(basename "$infile" .in)
# Define the path for the expected output file
expectedfile="$EXPECTED_DIR/$base.expected.out"
# Check if the expected output file exists
if [[ ! -f $expectedfile ]]; then
echo "Expected output file $expectedfile does not exist. Skipping $infile."
continue
fi
# Run the command and store its output in a temporary file
tmpfile=$(mktemp)
.lake/build/bin/repl < "$infile" > "$tmpfile" 2>&1
# Compare the output with the expected output
if diff "$tmpfile" "$expectedfile"; then
echo "$base: PASSED"
# Remove the temporary file
rm "$tmpfile"
else
echo "$base: FAILED"
# Remove the temporary file
rm "$tmpfile"
exit 1
fi
done
# Run the Mathlib tests
cp lean-toolchain test/Mathlib/
cd test/Mathlib/ && ./test.sh