new script

HanielB · Oct 26, 2022 · 6751c64 · 6751c64
1 parent 37d5542
commit 6751c64
Showing 1 changed file with 13 additions and 1 deletion.
diff --git a/lean-proof.sh b/lean-proof.sh
@@ -1,3 +1,15 @@
 #!/bin/bash
 
-~/cvc/wt-leanPrinter/prod/bin/cvc5 $@ | tail -n +2
+tfile="$(mktemp /tmp/foo.XXXXXXXXX)" || exit 1
+outfile="$(mktemp /tmp/foo.XXXXXXXXX)" || exit 1
+
+./prod/bin/cvc5 --dump-proofs --proof-format=lean --proof-granularity=theory-rewrite --dag-thresh=0 $@ | tail -n +2 > $tfile
+
+cd ~/lean-smt
+lean --load-dynlib=/home/hbarbosa/lean-smt/build/lib/libSmt.so $tfile > $outfile
+cd - > /dev/null
+if ! grep -q "error" $outfile; then
+  echo "SUCCESS"
+else
+  echo "ERROR-LEAN"
+fi