add pipeline

.gitignore

 *.lpo
 log-lp.txt
 log-lsp.txt
+_build/
+_opam/

proofs/appaxiom/.gitignore

+psnj-appaxiom

proofs/pipeline/.gitignore

+psnj-pipe

proofs/pipeline/Makefile

+ROOT     = pipe
+CMDLINER = true
+
+.include "../dune-exe.mk"
+.include "../tools.mk"

proofs/pipeline/dune

+(executable
+ (name pipe)
+ (libraries feather cmdliner))

proofs/pipeline/dune-project

+(lang dune 2.9)
+(name psnj_pipe)
+(generate_opam_files true)
+
+(package
+ (name psnj_pipe)
+ (synopsis "Pipeline for personoj")
+ (depends cmdliner feather))

proofs/pipeline/pipe.ml

+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)

proofs/pipeline/psnj_pipe.opam

+# 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]
+]

specs/tools/prelude/.gitignore

+number_fields.lp.orig
+number_fields.lp.rej