Merged pipeline into toolbox

and provide path to psnj to tests

.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
-

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 ezjsonm))
-
-(install
- (section bin)
- (files
-  (pipe.exe as psnj-pipe)))

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

proofs/pipeline/examples/.gitignore

-*.log
-*~
-*.summary
-pvsbin/
-.pvscontext
-orphaned-proof.prf
-*.dep
-run.out
-PVSBIN

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"
-  "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]
-]

proofs/psnj_toolbox/bin/dune

 (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

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)

proofs/pipeline/pipe.ml → 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) )

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

proofs/psnj_toolbox/personoj.opam

@@ -7,6 +7,7 @@ depends: [
   "angstrom"
   "ezjsonm"
   "lambdapi"
+  "feather"
   "odoc" {with-doc}
 ]
 build: [