Lisp testing

.github/workflows/pvs_prelude.yml

@@ -44,6 +44,7 @@ jobs:
         LP_FLAGS='-w --gen-obj'
         PVSPATH="${HOME}"/pvs-7.1.0
         export PVSPATH PERSONOJPATH LISP LP_FLAGS
+        ${LISP} --load ../tools.lisp --eval '(theory-select "theories.json" :enabled)' --quit
         opam exec -- bmake
         # For archiving
         mkdir /tmp/prelude-lp /tmp/prelude-lpo

.github/workflows/translator.yml

@@ -24,4 +24,4 @@ jobs:
         cd tests/thy_translation || exit 1
         export PVSPATH="${HOME}"/pvs-7.1.0
         export PERSONOJPATH="${GITHUB_WORKSPACE}"
-        bmake tests
+        ${PVSPATH}/pvs -raw -L test.lisp -E '(runall)' -E '(uiop:quit)'

tests/thy_translation/Makefile

-PVSPATH ?=
-PVS      = ${PVSPATH}/pvs -raw
-
-# We cannot internalise everything in lisp yet until the translation is "pure"
-# (i.e. no variable is changed at the end of the translation)
-
-THEORIES =
-THEORIES += naturals
-THEORIES += simple
-THEORIES += eqtype
-THEORIES += decvar
-THEORIES += import
-THEORIES += call_import
-THEORIES += prenex
-THEORIES += thyp_val
-THEORIES += thyp_type_val
-THEORIES += mixedup
-THEORIES += apply_theories
-THEORIES += subtypethy
-THEORIES += NatArray
-THEORIES += vector
-THEORIES += tuples
-THEORIES += tup_patmatch
-THEORIES += linear_form
-THEORIES += tfrom
-THEORIES += instantiate_subtype_formal
-THEORIES += constant_param
-THEORIES += exprastype
-THEORIES += depsubtype
-THEORIES += expandeddefs
-THEORIES += letin
-
-all: ${THEORIES:C/$/.lp/}
-
-tests: ${THEORIES:C/^/test-/}
-
-promote: ${THEORIES:C/^/promote-/}
-
-.for th in ${THEORIES}
-${th}.lp: simple.pvs
-	@${PVS} -L test.lisp -E '(runtest "${.TARGET:R}")' -E '(uiop:quit)'
-.endfor
-
-.for th in ${THEORIES}
-.PHONY: promote-${th}
-promote-${th}: ${th}.lp
-	@cp -f ${th}.lp ${th}.lp.expected
-.endfor
-
-clean:
-	rm -f *.lp
-
-.PHONY: clean

tests/thy_translation/test.lisp

+(defparameter *theories*
+  '("naturals"
+    "simple"
+    "eqtype"
+    "decvar"
+    "import"
+    "call_import"
+    "prenex"
+    "thyp_val"
+    "thyp_type_val"
+    "mixedup"
+    "apply_theories"
+    "subtypethy"
+    "NatArray"
+    "vector"
+    "tuples"
+    "tup_patmatch"
+    "linear_form"
+    "tfrom"
+    "instantiate_subtype_formal"
+    "constant_param"
+    "exprastype"
+    "depsubtype"
+    "expandeddefs"
+    "letin"))
+
 (defun promote (theory)
   (let ((out (format nil "~a.lp" theory))
         (expected (format nil "~a.lp.expected" theory)))
@@ -10,9 +36,15 @@
          (out (format nil "~a.lp" theory))
          (expected (format nil "~a.lp.expected" theory)))
     (prettyprint-dedukti thyref out t)
-    (handler-bind ((uiop:subprocess-error
-                     (lambda (err)
-                       (declare (ignore err))
-                       (invoke-restart-interactively 'promote))))
-      (uiop:run-program `("diff" "-u" "--color=always" ,expected ,out)
-                        :output t :error-output t))))
+    (handler-case
+        (uiop:run-program `("diff" "-u" "--color=always" ,expected ,out)
+                          :output t :error-output t)
+      (uiop:subprocess-error (err)
+        (declare (ignore err))
+        (unless non-interactive-p
+          (uiop:quit 1))
+        (when (y-or-n-p "Promote ~S?" out)
+          (promote theory))))))
+
+(defun runall (&key (theories *theories*) non-interactive-p)
+  (mapc #'runtest theories))