From 67788344a3561318c6b94bf768c0fb5ef30e4b3e Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Mon, 13 Dec 2021 14:47:12 +0100
Subject: [PATCH] Restructuring tests of pipeline, using dune
---
.github/workflows/proof_tools.yml | 4 ++--
proofs/pipeline/examples/Makefile | 15 ---------------
proofs/pipeline/examples/hello/dune | 8 ++++++++
proofs/pipeline/examples/hello/encoding | 1 +
.../{run.expected => hello/hello.expected} | 0
proofs/pipeline/examples/{ => hello}/hello.log | 0
proofs/pipeline/examples/hello/hello.ml | 13 +++++++++++++
proofs/pipeline/examples/{ => hello}/hello.prf | 0
proofs/pipeline/examples/{ => hello}/hello.pvs | 0
proofs/pipeline/examples/hello/lambdapi.pkg | 1 +
proofs/pipeline/examples/hello/spec/main.lp | 3 +++
proofs/pipeline/examples/run.sh | 3 ---
12 files changed, 28 insertions(+), 20 deletions(-)
delete mode 100644 proofs/pipeline/examples/Makefile
create mode 100644 proofs/pipeline/examples/hello/dune
create mode 120000 proofs/pipeline/examples/hello/encoding
rename proofs/pipeline/examples/{run.expected => hello/hello.expected} (100%)
rename proofs/pipeline/examples/{ => hello}/hello.log (100%)
create mode 100644 proofs/pipeline/examples/hello/hello.ml
rename proofs/pipeline/examples/{ => hello}/hello.prf (100%)
rename proofs/pipeline/examples/{ => hello}/hello.pvs (100%)
create mode 120000 proofs/pipeline/examples/hello/lambdapi.pkg
create mode 100644 proofs/pipeline/examples/hello/spec/main.lp
delete mode 100644 proofs/pipeline/examples/run.sh
diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml
index 88e04f6..11baf1d 100644
--- a/.github/workflows/proof_tools.yml
+++ b/.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
diff --git a/proofs/pipeline/examples/Makefile b/proofs/pipeline/examples/Makefile
deleted file mode 100644
index d3b91a4..0000000
--- a/proofs/pipeline/examples/Makefile
+++ /dev/null
@@ -1,15 +0,0 @@
-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
-
diff --git a/proofs/pipeline/examples/hello/dune b/proofs/pipeline/examples/hello/dune
new file mode 100644
index 0000000..d4ad576
--- /dev/null
+++ b/proofs/pipeline/examples/hello/dune
@@ -0,0 +1,8 @@
+(test
+ (deps
+ hello.log
+ lambdapi.pkg
+ (glob_files encoding/*)
+ (glob_files spec/main.lp))
+ (name hello)
+ (libraries unix))
diff --git a/proofs/pipeline/examples/hello/encoding b/proofs/pipeline/examples/hello/encoding
new file mode 120000
index 0000000..efb722e
--- /dev/null
+++ b/proofs/pipeline/examples/hello/encoding
@@ -0,0 +1 @@
+../encoding/
\ No newline at end of file
diff --git a/proofs/pipeline/examples/run.expected b/proofs/pipeline/examples/hello/hello.expected
similarity index 100%
rename from proofs/pipeline/examples/run.expected
rename to proofs/pipeline/examples/hello/hello.expected
diff --git a/proofs/pipeline/examples/hello.log b/proofs/pipeline/examples/hello/hello.log
similarity index 100%
rename from proofs/pipeline/examples/hello.log
rename to proofs/pipeline/examples/hello/hello.log
diff --git a/proofs/pipeline/examples/hello/hello.ml b/proofs/pipeline/examples/hello/hello.ml
new file mode 100644
index 0000000..b57cf87
--- /dev/null
+++ b/proofs/pipeline/examples/hello/hello.ml
@@ -0,0 +1,13 @@
+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
diff --git a/proofs/pipeline/examples/hello.prf b/proofs/pipeline/examples/hello/hello.prf
similarity index 100%
rename from proofs/pipeline/examples/hello.prf
rename to proofs/pipeline/examples/hello/hello.prf
diff --git a/proofs/pipeline/examples/hello.pvs b/proofs/pipeline/examples/hello/hello.pvs
similarity index 100%
rename from proofs/pipeline/examples/hello.pvs
rename to proofs/pipeline/examples/hello/hello.pvs
diff --git a/proofs/pipeline/examples/hello/lambdapi.pkg b/proofs/pipeline/examples/hello/lambdapi.pkg
new file mode 120000
index 0000000..3b1336c
--- /dev/null
+++ b/proofs/pipeline/examples/hello/lambdapi.pkg
@@ -0,0 +1 @@
+../lambdapi.pkg
\ No newline at end of file
diff --git a/proofs/pipeline/examples/hello/spec/main.lp b/proofs/pipeline/examples/hello/spec/main.lp
new file mode 100644
index 0000000..c4cfc95
--- /dev/null
+++ b/proofs/pipeline/examples/hello/spec/main.lp
@@ -0,0 +1,3 @@
+require open qfo.encoding.lhol qfo.encoding.pvs_cert;
+symbol P: Prop;
+symbol Q: Prop;
diff --git a/proofs/pipeline/examples/run.sh b/proofs/pipeline/examples/run.sh
deleted file mode 100644
index 7f052f8..0000000
--- a/proofs/pipeline/examples/run.sh
+++ /dev/null
@@ -1,3 +0,0 @@
-#!/bin/sh
-set -euf
-opam exec -- psnj-pipe --qfo=encoding/qfo.json hello.log
--
GitLab