From 1ccf8b9c1a928fedf6b3e4cc3a1ba45ee732208c Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Fri, 3 Dec 2021 15:25:24 +0100
Subject: [PATCH] add pipeline
---
.gitignore | 2 ++
proofs/appaxiom/.gitignore | 1 +
proofs/pipeline/.gitignore | 1 +
proofs/pipeline/.ocamlformat | 0
proofs/pipeline/Makefile | 5 ++++
proofs/{ => pipeline}/dkproof.mk | 0
proofs/pipeline/dune | 3 ++
proofs/pipeline/dune-project | 8 +++++
proofs/pipeline/pipe.ml | 50 ++++++++++++++++++++++++++++++++
proofs/pipeline/psnj_pipe.opam | 25 ++++++++++++++++
specs/tools/prelude/.gitignore | 2 ++
11 files changed, 97 insertions(+)
create mode 100644 proofs/appaxiom/.gitignore
create mode 100644 proofs/pipeline/.gitignore
create mode 100644 proofs/pipeline/.ocamlformat
create mode 100644 proofs/pipeline/Makefile
rename proofs/{ => pipeline}/dkproof.mk (100%)
create mode 100644 proofs/pipeline/dune
create mode 100644 proofs/pipeline/dune-project
create mode 100644 proofs/pipeline/pipe.ml
create mode 100644 proofs/pipeline/psnj_pipe.opam
create mode 100644 specs/tools/prelude/.gitignore
diff --git a/.gitignore b/.gitignore
index e51be4e..ac80ddd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,5 @@
*.lpo
log-lp.txt
log-lsp.txt
+_build/
+_opam/
diff --git a/proofs/appaxiom/.gitignore b/proofs/appaxiom/.gitignore
new file mode 100644
index 0000000..27d8084
--- /dev/null
+++ b/proofs/appaxiom/.gitignore
@@ -0,0 +1 @@
+psnj-appaxiom
diff --git a/proofs/pipeline/.gitignore b/proofs/pipeline/.gitignore
new file mode 100644
index 0000000..4fed5a3
--- /dev/null
+++ b/proofs/pipeline/.gitignore
@@ -0,0 +1 @@
+psnj-pipe
diff --git a/proofs/pipeline/.ocamlformat b/proofs/pipeline/.ocamlformat
new file mode 100644
index 0000000..e69de29
diff --git a/proofs/pipeline/Makefile b/proofs/pipeline/Makefile
new file mode 100644
index 0000000..0f9eb4e
--- /dev/null
+++ b/proofs/pipeline/Makefile
@@ -0,0 +1,5 @@
+ROOT = pipe
+CMDLINER = true
+
+.include "../dune-exe.mk"
+.include "../tools.mk"
diff --git a/proofs/dkproof.mk b/proofs/pipeline/dkproof.mk
similarity index 100%
rename from proofs/dkproof.mk
rename to proofs/pipeline/dkproof.mk
diff --git a/proofs/pipeline/dune b/proofs/pipeline/dune
new file mode 100644
index 0000000..147e7be
--- /dev/null
+++ b/proofs/pipeline/dune
@@ -0,0 +1,3 @@
+(executable
+ (name pipe)
+ (libraries feather cmdliner))
diff --git a/proofs/pipeline/dune-project b/proofs/pipeline/dune-project
new file mode 100644
index 0000000..66612c7
--- /dev/null
+++ b/proofs/pipeline/dune-project
@@ -0,0 +1,8 @@
+(lang dune 2.9)
+(name psnj_pipe)
+(generate_opam_files true)
+
+(package
+ (name psnj_pipe)
+ (synopsis "Pipeline for personoj")
+ (depends cmdliner feather))
diff --git a/proofs/pipeline/pipe.ml b/proofs/pipeline/pipe.ml
new file mode 100644
index 0000000..7204242
--- /dev/null
+++ b/proofs/pipeline/pipe.ml
@@ -0,0 +1,50 @@
+open Feather
+open Feather.Infix
+
+let process src proveit qfo_conf =
+ (* Define commands *)
+ let proveit = process proveit [ "--traces"; "-l"; src ]
+ and keepjson = process "perl" [ "-ne"; "print if /^\\{.*\\}$/" ]
+ and mkprops =
+ process "jq"
+ [
+ "-r";
+ {d|"symbol {|" + .name + "!" + (.incr | tostring) + "|}: " + .dk + ";"|d};
+ ]
+ and mkdeps =
+ process "jq" [ "-r"; {|(.name + "!" + (.incr | tostring)), .path|} ]
+ and dopth = process "dopth" []
+ and chainprops depfile = process "psnj-chainprops" [ depfile ]
+ and foise = process "psnj-qfo" [qfo_conf] in
+ let logfile = Filename.remove_extension src ^ ".log" in
+ let depfile = Filename.(temp_file (remove_extension src) ".dep") in
+ (* Run commands *)
+ run (proveit > "/dev/null");
+ let json = collect stdout (cat logfile |. keepjson) in
+ run (echo json |. mkdeps |. dopth > depfile);
+ let propositions =
+ collect stdout (echo json |. mkprops |. chainprops depfile |. foise)
+ in
+ Format.printf "%s" propositions
+
+open Cmdliner
+
+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)
+
+let cmd =
+ let exits = Term.default_exits in
+ let doc = "Pipeline for personoj" in
+ ( Term.(const process $ src $ proveit $ qfo_conf),
+ Term.(info "psnj-pipe" ~exits ~doc) )
+
+let () = Term.(exit @@ eval cmd)
diff --git a/proofs/pipeline/psnj_pipe.opam b/proofs/pipeline/psnj_pipe.opam
new file mode 100644
index 0000000..860fe2a
--- /dev/null
+++ b/proofs/pipeline/psnj_pipe.opam
@@ -0,0 +1,25 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Pipeline for personoj"
+depends: [
+ "dune" {>= "2.9"}
+ "cmdliner"
+ "feather"
+ "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/specs/tools/prelude/.gitignore b/specs/tools/prelude/.gitignore
new file mode 100644
index 0000000..f4f1766
--- /dev/null
+++ b/specs/tools/prelude/.gitignore
@@ -0,0 +1,2 @@
+number_fields.lp.orig
+number_fields.lp.rej
--
GitLab