Restructuring tests of pipeline, using dune

.github/workflows/proof_tools.yml

@@ -57,11 +57,11 @@ jobs:
         opam install yojson angstrom feather cmdliner
         cd proofs || exit 1
         (cd split && bmake && sudo bmake install)
-        (cd pipeline && bmake && sudo bmake install)
         (cd psnj_toolbox && make && sudo make install)
+        (cd pipeline && bmake && sudo bmake install)
 
     - name: launch pipeline
       run: |
         cd proofs/pipeline || exit 1
-        bmake tests
+        opam exec -- dune runtest
 

proofs/pipeline/examples/Makefile

-all: test
-	
-run.out: run.sh
-	sh run.sh > run.out
-
-test: run.out run.expected
-	@diff run.expected run.out
-
-promote:
-	cp run.out run.expected
-
-clean: run.out
-
-.PHONY: test diff promote clean all
-

proofs/pipeline/examples/hello/dune

+(test
+ (deps
+  hello.log
+  lambdapi.pkg
+  (glob_files encoding/*)
+  (glob_files spec/main.lp))
+ (name hello)
+ (libraries unix))

proofs/pipeline/examples/hello/encoding

+../encoding/
\ No newline at end of file

proofs/pipeline/examples/hello/hello.ml

+let () =
+  match
+    Unix.system
+      (Filename.quote_command "psnj-pipe"
+         [ "--qfo"; "encoding/qfo.json"; "hello.log" ])
+  with
+  | Unix.WEXITED 0 -> exit 0
+  | Unix.WEXITED n ->
+      Format.eprintf "Command exited with code %d@." n;
+      exit 1
+  | Unix.WSIGNALED _ | Unix.WSTOPPED _ ->
+      Format.eprintf "Command stopped by signal";
+      exit 2

proofs/pipeline/examples/hello/lambdapi.pkg

+../lambdapi.pkg
\ No newline at end of file

proofs/pipeline/examples/hello/spec/main.lp

+require open qfo.encoding.lhol qfo.encoding.pvs_cert;
+symbol P: Prop;
+symbol Q: Prop;

proofs/pipeline/examples/run.sh

-#!/bin/sh
-set -euf
-opam exec -- psnj-pipe --qfo=encoding/qfo.json hello.log