One binary only

appaxiom, autosolve, dopth and chainprops are accessed by
psnj CMD instead of a binary psnj-CMD

.github/workflows/proof_tools.yml

@@ -26,40 +26,12 @@ jobs:
     - name: Pin lambdapi
       run: opam pin add 'git://github.com/gabrielhdt/lambdapi#refiner'
 
-    - name: dopth
+    - name: toolbox
       run: |
-        cd "${GITHUB_WORKSPACE}"/personoj/proofs/dopth || exit 1
-        opam install dune --yes
-        opam exec -- dune build
-        opam exec -- dune runtest
-
-    - name: chainprops
-      run: |
-        cd "${GITHUB_WORKSPACE}"/personoj/proofs/chainprops || exit 1
-        opam install . --deps-only --yes
-        opam exec -- dune build
-        opam exec -- dune runtest
-
-    - name: appaxiom
-      run: |
-        cd "${GITHUB_WORKSPACE}"/personoj/proofs/appaxiom || exit 1
+        cd "${GITHUB_WORKSPACE}"/personoj/proofs/psnj_toolbox || exit 1
         opam install . --deps-only --yes
         opam exec -- dune build
-        opam exec -- dune runtest
-
-    - name: qfo
-      run: |
-        cd "${GITHUB_WORKSPACE}"/personoj/proofs/qfo || exit 1
-        opam install . --deps-only --yes
-        opam exec -- dune build
-        opam exec -- dune runtest
-
-    - name: autosolve
-      run: |
-        cd "${GITHUB_WORKSPACE}"/personoj/proofs/autosolve || exit 1
-        opam install cmdliner --yes
-        opam exec -- dune build
-        opam exec -- dune runtest
+        opam exe -- dune runtest
 
   pipeline:
     strategy:
@@ -88,13 +60,9 @@ jobs:
       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)
-        (cd autosolve && bmake && sudo bmake install)
+        (cd psnj_toolbox && make && sudo make install)
 
     - name: launch pipeline
       run: |

proofs/appaxiom/.gitignore

-psnj-appaxiom

proofs/appaxiom/Makefile

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

proofs/appaxiom/dune

-(executable
- (name appaxiom)
- (libraries cmdliner lambdapi.parsing lambdapi.common))

proofs/appaxiom/tests/appaxiom.t

-  $ echo 'symbol true : imp P P;' | ../appaxiom.exe
-  symbol true : @Prf (imp P P);

proofs/appaxiom/tests/dune

-(cram
- (deps ../appaxiom.exe))

proofs/autosolve/.gitignore

-psnj-autosolve
-_build

proofs/autosolve/Makefile

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

proofs/autosolve/dune

-(executable
- (name autosolve)
- (libraries cmdliner lambdapi.parsing lambdapi.common))

proofs/autosolve/dune-project

-(lang dune 2.9)
-(cram enable)

proofs/autosolve/tests/dune

-(cram
- (deps ../autosolve.exe))

proofs/chainprops/.gitignore

-_opam
-_build
-psnj-chainprops
-*.1

proofs/chainprops/Makefile

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

proofs/chainprops/chainprops.opam

-# This file is generated by dune, edit dune-project instead
-opam-version: "2.0"
-synopsis: "Make inference steps out of Dedukti propositions"
-maintainer: ["dedukti-dev@inria.fr"]
-depends: [
-  "dune" {>= "2.9"}
-  "cmdliner"
-  "angstrom"
-  "lambdapi"
-  "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/chainprops/dune

-(executable
- (name chainprops)
- (libraries angstrom cmdliner lambdapi.common lambdapi.parsing))

proofs/chainprops/dune-project

-(lang dune 2.9)
-(name chainprops)
-(cram enable)
-
-(generate_opam_files true)
-(maintainers "dedukti-dev@inria.fr")
-
-(package
- (name chainprops)
- (synopsis "Make inference steps out of Dedukti propositions")
- (depends
-  cmdliner angstrom lambdapi))

proofs/chainprops/test/dune

-(cram
- (deps ../chainprops.exe example.lp example.dep foo.lp foo.dep))

proofs/dopth/.gitignore

-psnj-dopth.1
-psnj-dopth
-_build/
-_opam/
-