diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml
index 3e39502a6afd1cab3404de6195a4d5f9f71df703..3247eb2167f58905e92b0e40d6fd6c8d93910f41 100644
--- a/.github/workflows/proof_tools.yml
+++ b/.github/workflows/proof_tools.yml
@@ -3,7 +3,7 @@ name: proof_tools
on: [push]
jobs:
- build:
+ tools:
strategy:
fail-fast: false
matrix:
@@ -61,3 +61,43 @@ jobs:
opam install ocamlformat
opam exec -- dune build @fmt
opam exec -- dune runtest
+
+ pipeline:
+ strategy:
+ fail-fast: false
+ matrix:
+ ocaml-compiler:
+ - 4.13.x
+ runs-on: ubuntu-latest
+ steps:
+ - uses: actions/checkout@v2
+ with:
+ path: personoj
+
+ - 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 asciidoc --yes
+
+ - name: install tools
+ run: |
+ opam install yojson angstrom feather cmdliner
+ cd "${GITHUB_WORKSPACE}"/personoj/proofs || exit 1
+ (cd appaxiom && bmake && sudo bmake install)
+ (cd chainprops && bmake && sudo bmake install)
+ (cd dopth && bmake && sudo bmake install)
+ (cd qfo && bmake && sudo bmake install)
+ (cd split && bmake && sudo bmake install)
+ (cd pipeline && bmake && sudo bmake install)
+
+ - name: launch pipeline
+ run: |
+ cd "${GITHUB_WORKSPACE}"/personoj/proofs/pipeline || exit 1
+ bmake tests
+
diff --git a/proofs/appaxiom/appaxiom.ml b/proofs/appaxiom/appaxiom.ml
index 9db14c06b2fbadc427ac9730cddeb2c2ff896491..70951f2d42b069d09f33d205d8141dcc3e4ef5ea 100644
--- a/proofs/appaxiom/appaxiom.ml
+++ b/proofs/appaxiom/appaxiom.ml
@@ -13,6 +13,8 @@ let map_sym_typ (f : S.p_term -> S.p_term) : S.p_command -> S.p_command =
let appaxiom sym =
let ast = Parser.parse stdin in
+ (* Set geometry to have terminal independent output *)
+ Format.set_geometry ~max_indent:8 ~margin:72;
let app typ = S.P.appl (S.P.iden sym) typ in
let process cmd =
let open Format in
@@ -40,7 +42,7 @@ let cmd =
`S Manpage.s_bugs;
`P
"$(tname) operates a syntactic transformation. If a symbol has a \
- definition, it won't be change, so the type of the definition will \
+ definition, it won't be changed, so the type of the definition will \
surely not match the declared type. To change definitions based on \
their type, coercions are needed.";
]
diff --git a/proofs/pipeline/Makefile b/proofs/pipeline/Makefile
index 0f9eb4ef26648ed6ef5c9363adfc9ff8527c6f70..c6d8571c857838e0272552abf0a2e3ca35287a40 100644
--- a/proofs/pipeline/Makefile
+++ b/proofs/pipeline/Makefile
@@ -1,5 +1,11 @@
ROOT = pipe
CMDLINER = true
+.PHONY: _tests
+_tests:
+ (cd examples && ${MAKE})
+
+tests: _tests
+
.include "../dune-exe.mk"
.include "../tools.mk"
diff --git a/proofs/pipeline/examples/.gitignore b/proofs/pipeline/examples/.gitignore
index 3c28b2158dadf3ff4e0bf585a515d3dcd18fcc4e..3ce418edd55daaeb3dca0aff5246f09168a0d724 100644
--- a/proofs/pipeline/examples/.gitignore
+++ b/proofs/pipeline/examples/.gitignore
@@ -5,3 +5,4 @@ pvsbin/
.pvscontext
orphaned-proof.prf
*.dep
+run.out
diff --git a/proofs/pipeline/examples/Makefile b/proofs/pipeline/examples/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..d3b91a482d0de8ad0aaeb40f5e80b56c657315ed
--- /dev/null
+++ b/proofs/pipeline/examples/Makefile
@@ -0,0 +1,15 @@
+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.log b/proofs/pipeline/examples/hello.log
new file mode 100644
index 0000000000000000000000000000000000000000..febe1998394633177c734f5ce3ffd40237a94eb0
--- /dev/null
+++ b/proofs/pipeline/examples/hello.log
@@ -0,0 +1,144 @@
+International Allegro CL Enterprise Edition
+10.1 [64-bit Linux (x86-64)] (Nov 14, 2020 18:29)
+Copyright (C) 1985-2017, Franz Inc., Oakland, CA, USA. All Rights Reserved.
+
+This dynamic runtime copy of Allegro CL was built by:
+ [TC21720] SRI International
+
+;; Optimization settings: safety 1, space 1, speed 3, debug 1.
+;; For a complete description of all compiler switches given the
+;; current optimization settings evaluate (explain-compiler-settings).
+;;---
+;; Current reader case mode: :case-sensitive-lower
+Warning: Ignoring declaration of unrecognized ftype:
+ (function (some-pvs-type some-pvs-type) *)
+Warning: The type subform of the ftype declaration must be a subtype of
+ function:
+ (ftype (function (some-pvs-type some-pvs-type) *)
+ some-pvs-type-eq)
+Warning: Ignoring declaration of unrecognized ftype:
+ (function (signature stream) *)
+Warning: The type subform of the ftype declaration must be a subtype of
+ function: (ftype (function (signature stream) *) dump)
+Warning: Ignoring declaration of unrecognized ftype:
+ (function (stream * expr * type-expr) *)
+Warning: The type subform of the ftype declaration must be a subtype of
+ function:
+ (ftype (function (stream * expr * type-expr) *) pp-dk-recursor)
+Warning: Ignoring declaration of unrecognized ftype:
+ (function (stream symbol expr name type-expr) *)
+Warning: The type subform of the ftype declaration must be a subtype of
+ function:
+ (ftype (function (stream symbol expr name type-expr) *)
+ pp-nat-recursor)
+Warning: Ignoring declaration of unrecognized ftype:
+ (function (syntax string) *)
+Warning: The type subform of the ftype declaration must be a subtype of
+ function: (ftype (function (syntax string) *) to-dk3)
+Warning: Ignoring declaration of unrecognized ftype:
+ (function (var-decl) *)
+Warning: The type subform of the ftype declaration must be a subtype of
+ function: (ftype (function (var-decl) *) handle-var-decl)
+Warning: Ignoring declaration of unrecognized ftype:
+ (function (stream * &optional boolean boolean) *)
+Warning: The type subform of the ftype declaration must be a subtype of
+ function:
+ (ftype (function (stream * &optional boolean boolean) *)
+ pp-type)
+Warning: Ignoring declaration of unrecognized ftype:
+ (function (binding stream &optional boolean) *)
+Warning: The type subform of the ftype declaration must be a subtype of
+ function:
+ (ftype (function (binding stream &optional boolean) *)
+ pprint-binding)
+Warning: Ignoring declaration of unrecognized ftype:
+ (function (* list list stream &key (wrap boolean)) *)
+Warning: The type subform of the ftype declaration must be a subtype of
+ function:
+ (ftype (function (* list list stream &key (wrap boolean)) *)
+ pprint-formals)
+Warning: Ignoring declaration of unrecognized ftype:
+ (function (symbol stream string) *)
+Warning: The type subform of the ftype declaration must be a subtype of
+ function:
+ (ftype (function (symbol stream string) *) pprint-reqopen)
+Warning: Ignoring declaration of unrecognized ftype:
+ (function (list stream) *)
+Warning: The type subform of the ftype declaration must be a subtype of
+ function: (ftype (function (list stream) *) pprint-telescope)
+Warning: Ignoring declaration of unrecognized ftype:
+ (function (symbol (or type-expr null) stream &key (mod-id *)
+ (actuals list) (wrap boolean))
+ *)
+Warning: The type subform of the ftype declaration must be a subtype of
+ function:
+ (ftype
+ (function (symbol (or type-expr null) stream &key (mod-id *)
+ (actuals list) (wrap boolean))
+ *)
+ pprint-name)
+Warning: Ignoring declaration of unrecognized ftype:
+ (function (string string) *)
+Warning: The type subform of the ftype declaration must be a subtype of
+ function:
+ (ftype (function (string string) *) prettyprint-dedukti)
+
+***
+*** Processing hello.pvs (12:17:49 12/7/2021)
+*** Generated by proveit 7.1.0 (Nov 05, 2020)
+***
+Installing rewrite rule sets.singleton_rew (all instances)
+hello :
+
+ |-------
+{1} P IMPLIES Q IMPLIES P AND Q
+{"name":"hello","incr":1,"path":"root","dk":"P \u21d2 (\u03bb _v0: Prf P,Q \u21d2 (\u03bb _v1: Prf Q,P \u2227 (\u03bb _v2: Prf P, Q)))","tac":null}
+Rerunning step: (flatten)
+{"name":"hello","incr":2,"path":"root","dk":"P \u21d2 (\u03bb _v3: Prf P,Q \u21d2 (\u03bb _v4: Prf Q,P \u2227 (\u03bb _v5: Prf P, Q)))","tac":null}
+{"name":"hello","incr":3,"path":"0","dk":"(\u00ac P) \u2228 (\u03bb _v6: Prf (\u00ac (\u00ac P)),(\u00ac Q) \u2228 (\u03bb _v7: Prf (\u00ac (\u00ac Q)),P \u2227 (\u03bb _v8: Prf P, Q)))","tac":null}
+Applying disjunctive simplification to flatten sequent,
+this simplifies to:
+hello :
+
+{-1} P
+{-2} Q
+ |-------
+{1} P AND Q
+{"name":"hello","incr":4,"path":"0","dk":"(\u00ac P) \u2228 (\u03bb _v9: Prf (\u00ac (\u00ac P)),(\u00ac Q) \u2228 (\u03bb _va: Prf (\u00ac (\u00ac Q)),P \u2227 (\u03bb _vb: Prf P, Q)))","tac":null}
+Rerunning step: (split)
+Splitting conjunctions,
+this yields 2 subgoals:
+hello.1 :
+
+[-1] P
+[-2] Q
+ |-------
+{1} P
+{"name":"hello","incr":5,"path":"0.0","dk":"P \u2228 (\u03bb _vc: Prf (\u00ac P),(\u00ac P) \u2228 (\u03bb _vd: Prf (\u00ac (\u00ac P)),\u00ac Q))","tac":["propax"]}
+which is trivially true.
+
+This completes the proof of hello.1.
+
+hello.2 :
+
+[-1] P
+[-2] Q
+ |-------
+{1} Q
+{"name":"hello","incr":6,"path":"0.1","dk":"Q \u2228 (\u03bb _ve: Prf (\u00ac Q),(\u00ac P) \u2228 (\u03bb _vf: Prf (\u00ac (\u00ac P)),\u00ac Q))","tac":["propax"]}
+which is trivially true.
+
+This completes the proof of hello.2.
+
+Q.E.D.
+
+
+Run time = 0.04 secs.
+Real time = 0.06 secs.
+
+
+ Proof summary for theory hello
+ hello.................................proved - complete [shostak](0.04 s)
+ Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.04 s)
+
+Grand Totals: 1 proofs, 1 attempted, 1 succeeded (0.04 s)
\ No newline at end of file
diff --git a/proofs/pipeline/examples/run.expected b/proofs/pipeline/examples/run.expected
new file mode 100644
index 0000000000000000000000000000000000000000..2c1c0eac2a0f6e92b7cd5cde66636f6b1154cbcf
--- /dev/null
+++ b/proofs/pipeline/examples/run.expected
@@ -0,0 +1,6 @@
+symbol hello!1 : @Prf (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (imp spec.main.P (imp spec.main.Q (conj spec.main.P spec.main.Q)))));
+symbol hello!2 : @Prf (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (imp spec.main.P (imp spec.main.Q (conj spec.main.P spec.main.Q)))));
+symbol hello!3 : @Prf (@imp (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q))) (@imp (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q))) (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q)))));
+symbol hello!4 : @Prf (@imp (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q))) (@imp (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q))) (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q)))));
+symbol hello!5 : @Prf (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q)));
+symbol hello!6 : @Prf (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q)));
\ No newline at end of file
diff --git a/proofs/pipeline/examples/run.sh b/proofs/pipeline/examples/run.sh
index 4b62b60caa292be817a293c942084e5a51a107e2..4ca8b020e1df6e7899f70e8368752fe507ec148c 100644
--- a/proofs/pipeline/examples/run.sh
+++ b/proofs/pipeline/examples/run.sh
@@ -1,5 +1,3 @@
#!/bin/sh
-
-set -eu
-PROVEIT="${1:-}"
-psnj-pipe --proveit=$PROVEIT --qfo=encoding/qfo.json hello.pvs encoding/ spec/
+set -euf
+opam exec -- psnj-pipe --qfo=encoding/qfo.json hello.log encoding/ spec/
diff --git a/proofs/pipeline/pipe.ml b/proofs/pipeline/pipe.ml
index 799858ae1e1d0fb1346ae6a494f82c00a28daca2..d0aca845c8b5ed52f49e8b5b4f5762f27491d5e6 100644
--- a/proofs/pipeline/pipe.ml
+++ b/proofs/pipeline/pipe.ml
@@ -1,9 +1,10 @@
open Feather
open Feather.Infix
-let process src proveit qfo_conf encoding specification =
+let process proveit src qfo_conf encoding specification =
(* Define commands *)
- let proveit = process proveit [ "--traces"; "-l"; src ]
+ let proveit =
+ Option.map (fun p -> process p [ "--traces"; "-l"; src ]) proveit
and keepjson = process "perl" [ "-ne"; "print if /^\\{.*\\}$/" ]
and mkprops =
process "jq"
@@ -29,15 +30,16 @@ let process src proveit qfo_conf encoding specification =
and appaxiom = process "psnj-appaxiom" [ "-a"; "Prf" ] in
(* Set some file names *)
let logfile =
- (* File produced by proveit *)
- Filename.remove_extension src ^ ".log"
+ (* File produced by proveit if proveit is provided, src otherwise *)
+ match proveit with
+ | Some _ -> Filename.remove_extension src ^ ".log"
+ | None -> src
in
let depfile =
Filename.(temp_file (remove_extension src |> basename) ".dep")
in
(* Run commands *)
- debug := true;
- run (proveit > "/dev/null");
+ Option.iter (fun proveit -> run (proveit > "/dev/null")) proveit;
let json = collect stdout (cat logfile |. keepjson) in
run (echo json |. mkdeps |. dopth > depfile);
let sttprops =
@@ -52,10 +54,6 @@ let src =
let doc = "Rerun proofs of file $(docv) and record log" in
Arg.(required & pos 0 (some string) None & info [] ~doc ~docv:"PVS")
-let proveit =
- let doc = "Path to the proveit script" in
- Arg.(value & opt string "proveit" & info [ "proveit" ] ~doc)
-
let qfo_conf =
let doc = "Configuration for QFO" in
Arg.(value & opt string "qfo.json" & info [ "qfo" ] ~doc)
@@ -70,10 +68,15 @@ let specification =
let doc = "Open module $(docv).main to translate propositions" in
Arg.(required & pos 2 (some dir) None & info [] ~doc ~docv:"MOD")
+let proveit =
+ let doc = "Execute $(docv) to obtain a log file with proof information" in
+ Arg.(value & opt (some string) None & info [ "proveit" ] ~doc ~docv:"FILE")
+
let cmd =
let exits = Term.default_exits in
let doc = "Pipeline for personoj" in
- ( Term.(const process $ src $ proveit $ qfo_conf $ encoding $ specification),
- Term.(info "psnj-pipe" ~exits ~doc) )
+ let man = [] in
+ ( Term.(const process $ proveit $ src $ qfo_conf $ encoding $ specification),
+ Term.(info "psnj-pipe" ~exits ~doc ~man) )
let () = Term.(exit @@ eval cmd)