Commit 81926c5e authored by Heiko Becker's avatar Heiko Becker

Minor tweaks to regression test script

parent 078031b5
#!/bin/bash
HOLCOMMIT="$(cat ./hol4/.HOLCOMMIT)"
FLOVERDIR="$(pwd)"
#HOL4 regression tests
if [ ! -d "./HOL4" ];
then
echo "HOL4 not installed, starting to install HOL4 into current directory."
echo "If this is not intended, please abort with Ctrl-c"
sleep 5
git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4
cd HOL4
git checkout $HOLCOMMIT
poly < tools/smart-configure.sml
bin/build
export HOLDIR="$(pwd)"
cd ../
else
cd ./HOL4
export HOLDIR="$(pwd)"
git pull
CURRHOL="$(git rev-parse HEAD)"
if [[ "$CURRHOL" != "$HOLCOMMIT" ]];
then
echo "Updating HOL4 to latest version specified in .HOLCOMMIT"
git checkout $HOLCOMMIT
bin/build cleanAll
poly < tools/smart-configure.sml
bin/build
else
echo "HOL4 up-to-date"
fi
cd $FLOVERDIR
fi
eval `opam config env`
cd ./testcases/regression
......@@ -18,7 +53,7 @@ for fname in ./*.v; do
done
#HOL4 regression tests
HOLDIR=../../HOL4
$HOLDIR/bin/Holmake heap
for fname in ./*.sml; do
FILEPRE=${fname/Script.sml/}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment