diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml
index 5fbf07db9bccc6405d00fcbb5f7dd157bb03f7fd..be40fbefeaa0d3c28c22ec9ed2e84ddf211bf121 100644
--- a/.github/workflows/proof_tools.yml
+++ b/.github/workflows/proof_tools.yml
@@ -30,38 +30,3 @@ jobs:
opam install . --deps-only --yes
opam exec -- dune build
opam exec -- dune test
-
- pipeline:
- strategy:
- fail-fast: false
- matrix:
- ocaml-compiler:
- - 4.13.x
- runs-on: ubuntu-latest
- steps:
- - uses: actions/checkout@v2
-
- - name: ocaml
- uses: ocaml/setup-ocaml@v2
- with:
- ocaml-compiler: ${{ matrix.ocaml-compiler }}
-
- - name: pin lambdapi
- run: opam pin add 'git://github.com/gabrielhdt/lambdapi#refiner'
-
- - name: install bmake
- run: sudo apt-get install bmake --yes
-
- - name: install tools
- run: |
- opam install yojson angstrom feather cmdliner ezjsonm
- cd proofs || exit 1
- opam install psnj_toolbox/
-
- - name: launch pipeline
- run: |
- cd proofs/pipeline || exit 1
- opam install . --deps-only --yes
- opam exec -- dune build
- opam exec -- dune test
-
diff --git a/proofs/pipeline/.gitignore b/proofs/pipeline/.gitignore
deleted file mode 100644
index 4fed5a39c9266175e14c48640dbd27ecafc3d17c..0000000000000000000000000000000000000000
--- a/proofs/pipeline/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-psnj-pipe
diff --git a/proofs/pipeline/.ocamlformat b/proofs/pipeline/.ocamlformat
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/proofs/pipeline/Makefile b/proofs/pipeline/Makefile
deleted file mode 100644
index 0f9eb4ef26648ed6ef5c9363adfc9ff8527c6f70..0000000000000000000000000000000000000000
--- a/proofs/pipeline/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-ROOT = pipe
-CMDLINER = true
-
-.include "../dune-exe.mk"
-.include "../tools.mk"
diff --git a/proofs/pipeline/dune b/proofs/pipeline/dune
deleted file mode 100644
index 3ed681780a065fd1136474bfbc82a9bbdf64b6f6..0000000000000000000000000000000000000000
--- a/proofs/pipeline/dune
+++ /dev/null
@@ -1,8 +0,0 @@
-(executable
- (name pipe)
- (libraries feather cmdliner ezjsonm))
-
-(install
- (section bin)
- (files
- (pipe.exe as psnj-pipe)))
diff --git a/proofs/pipeline/dune-project b/proofs/pipeline/dune-project
deleted file mode 100644
index d88365f1afbc3466bc573c900f8fe286a7a7b8a3..0000000000000000000000000000000000000000
--- a/proofs/pipeline/dune-project
+++ /dev/null
@@ -1,8 +0,0 @@
-(lang dune 2.9)
-(name psnj_pipe)
-(generate_opam_files true)
-
-(package
- (name psnj_pipe)
- (synopsis "Pipeline for personoj")
- (depends cmdliner feather ezjsonm))
diff --git a/proofs/pipeline/examples/.gitignore b/proofs/pipeline/examples/.gitignore
deleted file mode 100644
index 0b6fe6ca064caddb6875c34eef584bd7684c37ac..0000000000000000000000000000000000000000
--- a/proofs/pipeline/examples/.gitignore
+++ /dev/null
@@ -1,9 +0,0 @@
-*.log
-*~
-*.summary
-pvsbin/
-.pvscontext
-orphaned-proof.prf
-*.dep
-run.out
-PVSBIN
diff --git a/proofs/pipeline/psnj_pipe.opam b/proofs/pipeline/psnj_pipe.opam
deleted file mode 100644
index e094514dc849ab3ad4c7a7b2e4b87252487275aa..0000000000000000000000000000000000000000
--- a/proofs/pipeline/psnj_pipe.opam
+++ /dev/null
@@ -1,26 +0,0 @@
-# This file is generated by dune, edit dune-project instead
-opam-version: "2.0"
-synopsis: "Pipeline for personoj"
-depends: [
- "dune" {>= "2.9"}
- "cmdliner"
- "feather"
- "ezjsonm"
- "odoc" {with-doc}
-]
-build: [
- ["dune" "subst"] {dev}
- [
- "dune"
- "build"
- "-p"
- name
- "-j"
- jobs
- "--promote-install-files=false"
- "@install"
- "@runtest" {with-test}
- "@doc" {with-doc}
- ]
- ["dune" "install" "-p" name "--create-install-files" name]
-]
diff --git a/proofs/psnj_toolbox/bin/dune b/proofs/psnj_toolbox/bin/dune
index d833eff297caa60ebaa46d1bc55b2622a7911df6..82ef54036a84ab20845067d621fe62fe4019ac0c 100644
--- a/proofs/psnj_toolbox/bin/dune
+++ b/proofs/psnj_toolbox/bin/dune
@@ -1,8 +1,9 @@
(executable
(public_name psnj)
(name main)
- (modules main dopth chainprops appaxiom autosolve qfo group)
+ (modules main dopth chainprops appaxiom autosolve qfo group pipe)
(libraries
+ feather
ezjsonm
personoj
personoj.qfo
diff --git a/proofs/psnj_toolbox/bin/main.ml b/proofs/psnj_toolbox/bin/main.ml
index 539d914e70164e2e8cdd5f7cd29260b2eda1de83..74810c27b34990050f2dae864c4c64b050e1e5f5 100644
--- a/proofs/psnj_toolbox/bin/main.ml
+++ b/proofs/psnj_toolbox/bin/main.ml
@@ -13,6 +13,7 @@ let cmds =
Autosolve.cmd;
Qfo.cmd;
Group.cmd;
+ Pipe.cmd
]
let () = Term.(exit @@ eval_choice default_cmd cmds)
diff --git a/proofs/pipeline/pipe.ml b/proofs/psnj_toolbox/bin/pipe.ml
similarity index 97%
rename from proofs/pipeline/pipe.ml
rename to proofs/psnj_toolbox/bin/pipe.ml
index 541fef59d6e845cab3aaa111cd4befdb090af028..60e32304a61a4fc9b5f446cf37c9a5f79d24aeb3 100644
--- a/proofs/pipeline/pipe.ml
+++ b/proofs/psnj_toolbox/bin/pipe.ml
@@ -85,6 +85,4 @@ let cmd =
let doc = "Pipeline for personoj" in
let man = [] in
( Term.(const process $ proveit $ src $ qfo_conf),
- Term.(info "psnj-pipe" ~exits ~doc ~man) )
-
-let () = Term.(exit @@ eval cmd)
+ Term.(info "pipe" ~exits ~doc ~man) )
diff --git a/proofs/pipeline/dkproof.mk b/proofs/psnj_toolbox/dkproof.mk
similarity index 100%
rename from proofs/pipeline/dkproof.mk
rename to proofs/psnj_toolbox/dkproof.mk
diff --git a/proofs/psnj_toolbox/dune-project b/proofs/psnj_toolbox/dune-project
index 99e5a76d83fb7d1a19c9c004f32898b034cf5267..6d8e058fad5aed251bf59936695e61540c8992c2 100644
--- a/proofs/psnj_toolbox/dune-project
+++ b/proofs/psnj_toolbox/dune-project
@@ -7,4 +7,4 @@
(package
(name personoj)
(synopsis "todo")
- (depends cmdliner angstrom ezjsonm lambdapi))
+ (depends cmdliner angstrom ezjsonm lambdapi feather))
diff --git a/proofs/psnj_toolbox/personoj.opam b/proofs/psnj_toolbox/personoj.opam
index a4e32a3218bc30c6081803ef6e35962872d55186..7cce1977e9dfa15242cf4e2c740a67d0271c5eff 100644
--- a/proofs/psnj_toolbox/personoj.opam
+++ b/proofs/psnj_toolbox/personoj.opam
@@ -7,6 +7,7 @@ depends: [
"angstrom"
"ezjsonm"
"lambdapi"
+ "feather"
"odoc" {with-doc}
]
build: [
diff --git a/proofs/pipeline/examples/encoding/cpl.lp b/proofs/psnj_toolbox/pipe_tests/encoding/cpl.lp
similarity index 100%
rename from proofs/pipeline/examples/encoding/cpl.lp
rename to proofs/psnj_toolbox/pipe_tests/encoding/cpl.lp
diff --git a/proofs/pipeline/examples/encoding/lhol.lp b/proofs/psnj_toolbox/pipe_tests/encoding/lhol.lp
similarity index 100%
rename from proofs/pipeline/examples/encoding/lhol.lp
rename to proofs/psnj_toolbox/pipe_tests/encoding/lhol.lp
diff --git a/proofs/pipeline/examples/encoding/propositional_connectives.lp b/proofs/psnj_toolbox/pipe_tests/encoding/propositional_connectives.lp
similarity index 100%
rename from proofs/pipeline/examples/encoding/propositional_connectives.lp
rename to proofs/psnj_toolbox/pipe_tests/encoding/propositional_connectives.lp
diff --git a/proofs/pipeline/examples/encoding/pvs_cert.lp b/proofs/psnj_toolbox/pipe_tests/encoding/pvs_cert.lp
similarity index 100%
rename from proofs/pipeline/examples/encoding/pvs_cert.lp
rename to proofs/psnj_toolbox/pipe_tests/encoding/pvs_cert.lp
diff --git a/proofs/pipeline/examples/encoding/pvs_connectives.lp b/proofs/psnj_toolbox/pipe_tests/encoding/pvs_connectives.lp
similarity index 100%
rename from proofs/pipeline/examples/encoding/pvs_connectives.lp
rename to proofs/psnj_toolbox/pipe_tests/encoding/pvs_connectives.lp
diff --git a/proofs/pipeline/examples/encoding/qfo.json b/proofs/psnj_toolbox/pipe_tests/encoding/qfo.json
similarity index 100%
rename from proofs/pipeline/examples/encoding/qfo.json
rename to proofs/psnj_toolbox/pipe_tests/encoding/qfo.json
diff --git a/proofs/pipeline/examples/ex/dune b/proofs/psnj_toolbox/pipe_tests/ex/dune
similarity index 59%
rename from proofs/pipeline/examples/ex/dune
rename to proofs/psnj_toolbox/pipe_tests/ex/dune
index 7ddcfb93e9f7b232448fdadce4a7fbb0214045fc..a02c2cdf2b995f1d4c38bb8fc20de49151299146 100644
--- a/proofs/pipeline/examples/ex/dune
+++ b/proofs/psnj_toolbox/pipe_tests/ex/dune
@@ -1,8 +1,10 @@
(test
(name ex)
(deps
+ %{bin:psnj}
ex.log
lambdapi.pkg
(glob_files encoding/*)
(glob_files spec/main.lp))
- (libraries unix))
+ (libraries unix)
+ (action (run ./ex.exe %{bin:psnj})))
diff --git a/proofs/pipeline/examples/ex/encoding b/proofs/psnj_toolbox/pipe_tests/ex/encoding
similarity index 100%
rename from proofs/pipeline/examples/ex/encoding
rename to proofs/psnj_toolbox/pipe_tests/ex/encoding
diff --git a/proofs/pipeline/examples/ex/ex.expected b/proofs/psnj_toolbox/pipe_tests/ex/ex.expected
similarity index 100%
rename from proofs/pipeline/examples/ex/ex.expected
rename to proofs/psnj_toolbox/pipe_tests/ex/ex.expected
diff --git a/proofs/pipeline/examples/ex/ex.log b/proofs/psnj_toolbox/pipe_tests/ex/ex.log
similarity index 100%
rename from proofs/pipeline/examples/ex/ex.log
rename to proofs/psnj_toolbox/pipe_tests/ex/ex.log
diff --git a/proofs/pipeline/examples/ex/ex.ml b/proofs/psnj_toolbox/pipe_tests/ex/ex.ml
similarity index 75%
rename from proofs/pipeline/examples/ex/ex.ml
rename to proofs/psnj_toolbox/pipe_tests/ex/ex.ml
index 4e667f48bcdf1ff40b9a3b333b3d73d7ef6ec2cc..ff49298f935d79bd49cb8a9798a6fc5f01bdd6fa 100644
--- a/proofs/pipeline/examples/ex/ex.ml
+++ b/proofs/psnj_toolbox/pipe_tests/ex/ex.ml
@@ -1,8 +1,8 @@
let () =
match
Unix.system
- (Filename.quote_command "psnj-pipe"
- [ "--qfo"; "encoding/qfo.json"; "ex.log" ])
+ (Filename.quote_command Sys.argv.(1)
+ [ "pipe"; "--qfo"; "encoding/qfo.json"; "ex.log" ])
with
| Unix.WEXITED 0 ->
ignore @@ Unix.system (Filename.quote_command "cat" ["exi.lp"])
diff --git a/proofs/pipeline/examples/ex/ex.prf b/proofs/psnj_toolbox/pipe_tests/ex/ex.prf
similarity index 100%
rename from proofs/pipeline/examples/ex/ex.prf
rename to proofs/psnj_toolbox/pipe_tests/ex/ex.prf
diff --git a/proofs/pipeline/examples/ex/ex.pvs b/proofs/psnj_toolbox/pipe_tests/ex/ex.pvs
similarity index 100%
rename from proofs/pipeline/examples/ex/ex.pvs
rename to proofs/psnj_toolbox/pipe_tests/ex/ex.pvs
diff --git a/proofs/pipeline/examples/ex/lambdapi.pkg b/proofs/psnj_toolbox/pipe_tests/ex/lambdapi.pkg
similarity index 100%
rename from proofs/pipeline/examples/ex/lambdapi.pkg
rename to proofs/psnj_toolbox/pipe_tests/ex/lambdapi.pkg
diff --git a/proofs/pipeline/examples/ex/spec/main.lp b/proofs/psnj_toolbox/pipe_tests/ex/spec/main.lp
similarity index 100%
rename from proofs/pipeline/examples/ex/spec/main.lp
rename to proofs/psnj_toolbox/pipe_tests/ex/spec/main.lp
diff --git a/proofs/pipeline/examples/hello/dune b/proofs/psnj_toolbox/pipe_tests/hello/dune
similarity index 59%
rename from proofs/pipeline/examples/hello/dune
rename to proofs/psnj_toolbox/pipe_tests/hello/dune
index d4ad576487c93bf2fe6b49e3159b7d3ab8954a5d..cfaa9d62072efff6d5ba3e7c8db22d9739736940 100644
--- a/proofs/pipeline/examples/hello/dune
+++ b/proofs/psnj_toolbox/pipe_tests/hello/dune
@@ -1,8 +1,10 @@
(test
+ (name hello)
(deps
+ %{bin:psnj}
hello.log
lambdapi.pkg
(glob_files encoding/*)
(glob_files spec/main.lp))
- (name hello)
- (libraries unix))
+ (libraries unix)
+ (action (run ./hello.exe %{bin:psnj})))
diff --git a/proofs/pipeline/examples/hello/encoding b/proofs/psnj_toolbox/pipe_tests/hello/encoding
similarity index 100%
rename from proofs/pipeline/examples/hello/encoding
rename to proofs/psnj_toolbox/pipe_tests/hello/encoding
diff --git a/proofs/pipeline/examples/hello/hello.expected b/proofs/psnj_toolbox/pipe_tests/hello/hello.expected
similarity index 100%
rename from proofs/pipeline/examples/hello/hello.expected
rename to proofs/psnj_toolbox/pipe_tests/hello/hello.expected
diff --git a/proofs/pipeline/examples/hello/hello.log b/proofs/psnj_toolbox/pipe_tests/hello/hello.log
similarity index 100%
rename from proofs/pipeline/examples/hello/hello.log
rename to proofs/psnj_toolbox/pipe_tests/hello/hello.log
diff --git a/proofs/pipeline/examples/hello/hello.ml b/proofs/psnj_toolbox/pipe_tests/hello/hello.ml
similarity index 75%
rename from proofs/pipeline/examples/hello/hello.ml
rename to proofs/psnj_toolbox/pipe_tests/hello/hello.ml
index 23e33827099b491dad937fc17e6f97f81c25f5fd..0a64c40fb310b2014ae0c6171772eec4e7cc6767 100644
--- a/proofs/pipeline/examples/hello/hello.ml
+++ b/proofs/psnj_toolbox/pipe_tests/hello/hello.ml
@@ -1,8 +1,8 @@
let () =
match
Unix.system
- (Filename.quote_command "psnj-pipe"
- [ "--qfo"; "encoding/qfo.json"; "hello.log" ])
+ (Filename.quote_command Sys.argv.(1)
+ [ "pipe"; "--qfo"; "encoding/qfo.json"; "hello.log" ])
with
| Unix.WEXITED 0 ->
ignore (Unix.system (Filename.quote_command "cat" ["hello.lp"]))
diff --git a/proofs/pipeline/examples/hello/hello.prf b/proofs/psnj_toolbox/pipe_tests/hello/hello.prf
similarity index 100%
rename from proofs/pipeline/examples/hello/hello.prf
rename to proofs/psnj_toolbox/pipe_tests/hello/hello.prf
diff --git a/proofs/pipeline/examples/hello/hello.pvs b/proofs/psnj_toolbox/pipe_tests/hello/hello.pvs
similarity index 100%
rename from proofs/pipeline/examples/hello/hello.pvs
rename to proofs/psnj_toolbox/pipe_tests/hello/hello.pvs
diff --git a/proofs/pipeline/examples/hello/lambdapi.pkg b/proofs/psnj_toolbox/pipe_tests/hello/lambdapi.pkg
similarity index 100%
rename from proofs/pipeline/examples/hello/lambdapi.pkg
rename to proofs/psnj_toolbox/pipe_tests/hello/lambdapi.pkg
diff --git a/proofs/pipeline/examples/hello/spec/main.lp b/proofs/psnj_toolbox/pipe_tests/hello/spec/main.lp
similarity index 100%
rename from proofs/pipeline/examples/hello/spec/main.lp
rename to proofs/psnj_toolbox/pipe_tests/hello/spec/main.lp
diff --git a/proofs/pipeline/examples/lambdapi.pkg b/proofs/psnj_toolbox/pipe_tests/lambdapi.pkg
similarity index 100%
rename from proofs/pipeline/examples/lambdapi.pkg
rename to proofs/psnj_toolbox/pipe_tests/lambdapi.pkg
diff --git a/proofs/pipeline/examples/multiproofs/dune b/proofs/psnj_toolbox/pipe_tests/multiproofs/dune
similarity index 59%
rename from proofs/pipeline/examples/multiproofs/dune
rename to proofs/psnj_toolbox/pipe_tests/multiproofs/dune
index fd35c4d47e615dc13e032857b00942ae1fd3a4a4..f8b2749ab9f5d619dec376a04d660c54277fd7c0 100644
--- a/proofs/pipeline/examples/multiproofs/dune
+++ b/proofs/psnj_toolbox/pipe_tests/multiproofs/dune
@@ -1,8 +1,10 @@
(test
(name mp)
(deps
+ %{bin:psnj}
mp.log
lambdapi.pkg
(glob_files encoding/*)
(glob_files spec/main.lp))
- (libraries unix))
+ (libraries unix)
+ (action (run ./mp.exe %{bin:psnj})))
diff --git a/proofs/pipeline/examples/multiproofs/encoding b/proofs/psnj_toolbox/pipe_tests/multiproofs/encoding
similarity index 100%
rename from proofs/pipeline/examples/multiproofs/encoding
rename to proofs/psnj_toolbox/pipe_tests/multiproofs/encoding
diff --git a/proofs/pipeline/examples/multiproofs/lambdapi.pkg b/proofs/psnj_toolbox/pipe_tests/multiproofs/lambdapi.pkg
similarity index 100%
rename from proofs/pipeline/examples/multiproofs/lambdapi.pkg
rename to proofs/psnj_toolbox/pipe_tests/multiproofs/lambdapi.pkg
diff --git a/proofs/pipeline/examples/multiproofs/mp.expected b/proofs/psnj_toolbox/pipe_tests/multiproofs/mp.expected
similarity index 100%
rename from proofs/pipeline/examples/multiproofs/mp.expected
rename to proofs/psnj_toolbox/pipe_tests/multiproofs/mp.expected
diff --git a/proofs/pipeline/examples/multiproofs/mp.log b/proofs/psnj_toolbox/pipe_tests/multiproofs/mp.log
similarity index 100%
rename from proofs/pipeline/examples/multiproofs/mp.log
rename to proofs/psnj_toolbox/pipe_tests/multiproofs/mp.log
diff --git a/proofs/pipeline/examples/multiproofs/mp.ml b/proofs/psnj_toolbox/pipe_tests/multiproofs/mp.ml
similarity index 76%
rename from proofs/pipeline/examples/multiproofs/mp.ml
rename to proofs/psnj_toolbox/pipe_tests/multiproofs/mp.ml
index 377b74207ad28610eeb057ba1ad6183777629b09..b23483e8a002d7ba62646c2977320c1bd213fc59 100644
--- a/proofs/pipeline/examples/multiproofs/mp.ml
+++ b/proofs/psnj_toolbox/pipe_tests/multiproofs/mp.ml
@@ -1,7 +1,7 @@
let () =
let cmd =
- Filename.quote_command "psnj-pipe"
- [ "--qfo"; "encoding/qfo.json"; "mp.log" ]
+ Filename.quote_command Sys.argv.(1)
+ [ "pipe"; "--qfo"; "encoding/qfo.json"; "mp.log" ]
in
match Unix.system cmd with
| WEXITED 0 ->
diff --git a/proofs/pipeline/examples/multiproofs/mp.prf b/proofs/psnj_toolbox/pipe_tests/multiproofs/mp.prf
similarity index 100%
rename from proofs/pipeline/examples/multiproofs/mp.prf
rename to proofs/psnj_toolbox/pipe_tests/multiproofs/mp.prf
diff --git a/proofs/pipeline/examples/multiproofs/mp.pvs b/proofs/psnj_toolbox/pipe_tests/multiproofs/mp.pvs
similarity index 100%
rename from proofs/pipeline/examples/multiproofs/mp.pvs
rename to proofs/psnj_toolbox/pipe_tests/multiproofs/mp.pvs
diff --git a/proofs/psnj_toolbox/pipe_tests/multiproofs/mp.summary b/proofs/psnj_toolbox/pipe_tests/multiproofs/mp.summary
new file mode 100644
index 0000000000000000000000000000000000000000..9c22360af1562af7edf005a583037a0f893f9aad
--- /dev/null
+++ b/proofs/psnj_toolbox/pipe_tests/multiproofs/mp.summary
@@ -0,0 +1,10 @@
+***
+*** Processing mp.pvs (16:42:30 12/13/2021)
+*** Generated by proveit 7.1.0 (Nov 05, 2020)
+***
+ Proof summary for theory mp
+ lem1..................................proved - complete [shostak](0.02 s)
+ lem2..................................proved - complete [shostak](0.02 s)
+ Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.04 s)
+
+Grand Totals: 2 proofs, 2 attempted, 2 succeeded (0.04 s)
\ No newline at end of file
diff --git a/proofs/pipeline/examples/multiproofs/spec/main.lp b/proofs/psnj_toolbox/pipe_tests/multiproofs/spec/main.lp
similarity index 100%
rename from proofs/pipeline/examples/multiproofs/spec/main.lp
rename to proofs/psnj_toolbox/pipe_tests/multiproofs/spec/main.lp
diff --git a/proofs/pipeline/examples/spec/main.lp b/proofs/psnj_toolbox/pipe_tests/spec/main.lp
similarity index 100%
rename from proofs/pipeline/examples/spec/main.lp
rename to proofs/psnj_toolbox/pipe_tests/spec/main.lp