diff options
| author | Brian Campbell | 2020-06-10 21:33:09 +0100 |
|---|---|---|
| committer | Brian Campbell | 2020-06-10 21:38:06 +0100 |
| commit | d2b4a7a1d654cf8f315e2471b1470506255f3d68 (patch) | |
| tree | 607a709d4912b80a7eb3966ad88a25d7b7bd159c /test | |
| parent | 18719e6801e804c4f5302745bb7cfb6dfe3a6c98 (diff) | |
Prepare Coq library for packaging
- rename files to get rid of prefix
- use -Q to get package name right
- add Base.v to make package imports simpler
- add opam file for coq package
Diffstat (limited to 'test')
| -rwxr-xr-x | test/coq/run_tests.sh | 12 | ||||
| -rw-r--r-- | test/coq/skip | 4 |
2 files changed, 13 insertions, 3 deletions
diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh index da6bce69..c31b1475 100755 --- a/test/coq/run_tests.sh +++ b/test/coq/run_tests.sh @@ -5,7 +5,13 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" SAILDIR="$DIR/../.." TYPECHECKTESTSDIR="$DIR/../typecheck/pass" EXTRATESTSDIR="$DIR/pass" -BBVDIR="$DIR/../../../bbv/src/bbv" + +if [ -z "$BBVDIR" ] || opam config var coq-bbv:share >/dev/null 2>/dev/null; then + COQOPTS="-Q $SAILDIR/lib/coq Sail" +else + BBVDIR="$DIR/../../../bbv/src/bbv" + COQOPTS="-Q $SAILDIR/lib/coq Sail -Q $BBVDIR bbv" +fi RED='\033[0;31m' GREEN='\033[0;32m' @@ -56,8 +62,8 @@ function check_tests_dir { do if $SAILDIR/sail -coq -dcoq_undef_axioms -o out $TESTSDIR/$i &>/dev/null; then - if coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out_types.v &>/dev/null && - coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out.v &>/dev/null; + if coqc $COQOPTS out_types.v &>/dev/null && + coqc $COQOPTS out.v &>/dev/null; then green "tested $i expecting pass" "pass" else diff --git a/test/coq/skip b/test/coq/skip index b99c87ad..7a233ddc 100644 --- a/test/coq/skip +++ b/test/coq/skip @@ -35,5 +35,9 @@ while_MM.sail while_MP.sail while_PM.sail while_PP.sail +XXXXX Non-terminating loop that's only really useful for the type checking tests +repeat_constraint.sail XXXXX Not yet - haven't decided whether to support register reads in measures while_MM_terminating.sail +XXXXX TODO, add termination measure +floor_pow2.sail |