add compile and clean up scripts for coq

.gitignore

@@ -20,6 +20,15 @@ dist/
 build/
 testdata/tmp
 
+# coq source files
+coq-proof/coq-source
+coq-proof/V8.8.0.tar.gz
+
+# coq proof output files
+coq-proof/*.aux
+coq-proof/*.vo
+coq-proof/*.glob
+
 # corpus
 corpus/
 worked-benchmarks/
@@ -48,7 +57,3 @@ manual-tests/insertionTest
 
 # temp files
 manual-tests/unused*
-
-# coq files
-coq-proof/coq-source
-coq-proof/V8.8.0.tar.gz

coq-proof/cleanup.sh

@@ -0,0 +1,5 @@
+#!/bin/bash
+
+rm .*.aux
+rm *.vo
+rm *.glob

coq-proof/compile.sh

@@ -0,0 +1,53 @@
+#!/bin/bash
+
+# Fail the whole script if any command fails
+set -e
+
+myDir="`dirname $0`"
+case `uname -s` in
+    CYGWIN*)
+      myDir=`cygpath -m $mydir`
+      ;;
+esac
+
+if [ "$myDir" = "" ];
+then
+    myDir="."
+fi
+
+ROOT=$(cd ${myDir} && pwd)
+
+# use system installed coqc if available
+if [[ $(command -v coqc) ]] && [[ $(coqc -v | grep 8.8.0) ]] ; then
+    COQC=$(command -v coqc)
+fi
+if [ -z "$COQC" ] && [ -e $ROOT/coq-source/bin/coqc ] ; then
+    COQC="$ROOT/coq-source/bin/coqc"
+fi
+echo "Using coqc at $COQC"
+$COQC -v
+
+# Compile options
+COQC="$COQC -opt"
+
+$COQC TacticalLemmas.v
+$COQC IDDefs.v
+$COQC MapsDefs.v
+
+$COQC UnitsDefs.v
+
+$COQC ValueDefs.v
+$COQC GammaDefs.v
+$COQC HeapDefs.v
+$COQC SubtypingDefs.v
+$COQC GammaHeapCorrespondence.v
+
+$COQC UnitsArithmetics.v
+
+$COQC FieldsDefs.v
+$COQC ExpressionsDefs.v
+$COQC StatementDefs.v
+$COQC ProgramDefs.v
+$COQC UnitsSoundness.v
+
+echo "Compilation complete."