tests: add a corres proof phase

cogent/tests/phases/corres_proof.sh

@@ -0,0 +1,92 @@
+#!/usr/bin/env bash
+
+#
+# type-proof COGENT_FILE
+#
+# Expects the env vars
+#   COGENT_PATH
+#
+
+echo $(pwd)
+
+if [ $# -ne 1 ]; then
+  echo "USAGE:"
+  echo "  type_proof.sh COGENT_FILE"
+  exit 1
+fi
+
+if [ ! -z "$COGENT_REPO" ]; then
+  if [ ! -d "$COGENT_REPO" ]; then
+    echo "error: '$COGENT_REPO' is not a directory"
+    exit 1
+  fi
+else
+  echo "type_proof.sh requires COGENT_REPO"
+  exit 1
+fi
+
+COGENT_REPO=${COGENT_REPO%/}
+
+COGENT=$COGENT_REPO/cogent/.cabal-sandbox/bin/cogent
+ISABELLE=$COGENT_REPO/isabelle/bin/isabelle
+AC_DIR=$COGENT_REPO/autocorres
+
+if [ ! -f "$COGENT" ]; then
+  echo "error: could not find cogent"
+  exit 1
+fi
+if [ ! -f "$ISABELLE" ]; then
+  echo "error: could not find isabelle"
+  exit 1
+fi
+if [ ! -d "$AC_DIR" ]; then
+  echo "error: could not find autocorres"
+  exit 1
+fi
+if [ -z "$TEST_DIST_DIR" ]; then
+  TEST_DIST_DIR=testing_tmp
+fi
+
+FILE=$1
+TEST_NAME_BASE=Test
+
+$COGENT \
+  -o $TEST_NAME_BASE \
+  --dist-dir $TEST_DIST_DIR \
+  --corres-proof --corres-setup \
+  --ac-install --type-proof \
+  --table-c-types \
+  --fake-header-dir="$COGENT_REPO/cogent/lib/" \
+  -g \
+  $FILE
+
+#sed 'N a new_C_include_dir'
+
+if [ ! $? ]; then
+  echo "error: cogent failed!"
+  exit 1
+fi
+
+cat > $TEST_DIST_DIR/ROOT <<EOF
+session Test_TypeProof = CogentCRefinement +
+  theories
+    "Test_TypeProof"
+
+session Test_ACInstall = Test_TypeProof +
+  theories
+    "Test_ACInstall"
+
+session Test_CorresSetup = Test_ACInstall +
+  theories
+    "Test_CorresSetup"
+
+session Test_CorresProof = Test_CorresSetup +
+  theories
+    "Test_CorresProof"
+EOF
+
+if [ -z $L4V_ARCH ]; then
+  export L4V_ARCH=ARM
+fi
+
+$ISABELLE build -d $COGENT_REPO -d $AC_DIR -d $TEST_DIST_DIR ${TEST_NAME_BASE}_CorresProof