max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: test each example using a separate file

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-19 13:51:52 -08:00
parent 72a6ce498a
commit e29cc367f3
1 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
doc/test
View file

@ -1,2 +1,11 @@
#!/usr/bin/env bash
awk 'BEGIN { lean = 0 } /```/ { if (lean == 1) lean = 0; } { if (lean == 1) { sub(/# /, ""); print $0 } } /```lean/ && !/```lean,ignore/ { lean = 1 }' $1 | lean --stdin
awk 'BEGIN { lean = 0; idx = 0 } /```/ { if (lean == 1) lean = 0; } { if (lean == 1) { sub(/# /, ""); print $0 > out } } /```lean/ && !/```lean,ignore/ { lean = 1; idx = idx + 1; out = FILENAME "." idx ".lean" }' $1
for f in `ls $1.*.lean`; do
echo "testing $f"
if ! lean $f; then
echo "FAILED"
rm -f $1.*.lean
exit 1
fi
rm $f
done