CN: Make run-cn.sh printing more consistent

The priniting is now in line with other CI test scripts, and run through
shellcheck to check for mistakes. An oddity is that the failing tests
could reflect either exit code 1 or 2, and passing arrays in bash is a
bit tricky, but this all seems to work.

.github/workflows/ci.yml

@@ -107,7 +107,6 @@ jobs:
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
         cd tests; USE_OPAM='' ./run-cn.sh
-        cd ..
 
     - name: Run CN Tutorial CI tests
       run: |

tests/run-cn.sh

@@ -1,78 +1,88 @@
-#!/bin/bash
+#!/usr/bin/env bash
 set -euo pipefail -o noclobber
 
 # copying from run-ci.sh
-export DYLD_LIBRARY_PATH="${DYLD_LIBRARY_PATH:-}:`ocamlfind query z3`"
-export LD_LIBRARY_PATH="${LD_LIBRARY_PATH:-}:`ocamlfind query z3`"
-CN=$OPAM_SWITCH_PREFIX/bin/cn
+Z3=$(ocamlfind query z3)
+export DYLD_LIBRARY_PATH="${DYLD_LIBRARY_PATH:-}:${Z3}"
+export LD_LIBRARY_PATH="${LD_LIBRARY_PATH:-}:${Z3}"
 
+USAGE="USAGE: $0 [-hl]"
 
-DIRNAME=$(dirname $0)
+function echo_and_err() {
+    printf "%s\n" "$1"
+    exit 1
+}
 
-SUCC=$(find $DIRNAME/cn -name '*.c' | grep -v '\.error\.c')
-FAIL=$(find $DIRNAME/cn -name '*.error.c')
+LEMMATA=0
 
-NUM_FAILED=0
-FAILED=''
+while getopts "hl" flag; do
+ case "$flag" in
+   h)
+   printf "%s\n" "${USAGE}"
+   exit 0
+   ;;
+   l)
+   LEMMATA=1
+   ;;
+   \?)
+   echo_and_err "${USAGE}"
+   ;;
+ esac
+done
 
+function exits_with_code() {
+  local action=$1
+  local file=$2
+  local -a expected_exit_codes=$3
 
-for TEST in $SUCC
-do
-  $CN verify $TEST
-  RET=$?
-  if [[ "$RET" = 0 ]]
-  then
-    echo "$TEST -- OK"
-  else
-    echo "$TEST -- Unexpected"
-    NUM_FAILED=$(( $NUM_FAILED + 1 ))
-    FAILED="$FAILED $TEST"
-  fi
-  echo
-done
+  printf "[$file]... "
+  timeout 20 ${action} "$file" &> /dev/null
+  local result=$?
+
+  for code in "${expected_exit_codes[@]}"; do
+    if [ $result -eq $code ]; then
+      printf "\033[32mPASS\033[0m\n"
+      return 0
+    fi
+  done
+
+  printf "\033[31mFAIL\033[0m (Unexpected return code: %d)\n" "$result"
+  return 1
+}
+
+DIRNAME=$(dirname "$0")
 
-for TEST in $FAIL
-do
-  $CN verify $TEST
-  RET=$?
-  if [[ "$RET" = 1 || "$RET" = 2 ]]
-  then
-    echo "$TEST -- OK"
-  else
-    echo "$TEST -- Unexpected"
-    NUM_FAILED=$(( $NUM_FAILED + 1 ))
-    FAILED="$FAILED $TEST"
+SUCC=$(find "${DIRNAME}"/cn -name '*.c' | grep -v '\.error\.c')
+FAIL=$(find "${DIRNAME}"/cn -name '*.error.c')
+
+FAILED=""
+
+for TEST in ${SUCC}; do
+  if ! exits_with_code "cn verify" "${TEST}" 0; then
+    FAILED+=" ${TEST}"
   fi
-  echo
 done
 
-COQ_LEMMAS=$(find $DIRNAME/cn -name 'coq_lemmas' -type d)
-
-for TEST in $COQ_LEMMAS
-do
-  if [ "${1:-}" == "--coq" ]
-  then
-    echo make -C $TEST
-    if ! make -C $TEST
-    then
-      NUM_FAILED=$(( $NUM_FAILED + 1 ))
-      FAILED="$FAILED $TEST"
-    fi
+for TEST in ${FAIL}; do
+  if ! exits_with_code "cn verify" "${TEST}" "(1 2)"; then
+    FAILED+=" ${TEST}"
   fi
 done
 
-echo
-echo 'Done running tests.'
-echo
+COQ_LEMMAS=$(find "${DIRNAME}"/cn -type d -name 'coq_lemmas')
 
-if [ -z "$FAILED" ]
-then
-  echo "All tests passed."
+if [ "${LEMMATA}" -eq 1 ]; then
+  for TEST in ${COQ_LEMMAS}; do
+      if ! exits_with_code "make -C" "${TEST}" 0; then
+        FAILED+=" ${TEST}"
+      fi
+  done
+fi
+
+if [ -z "${FAILED}" ]; then
   exit 0
 else
-  echo "$NUM_FAILED tests failed:"
-  echo "  $FAILED"
+  printf "\033[31mFAILED: %s\033[0m\n" "${FAILED}"
   exit 1
 fi
 
-