Fix tests, run test in ci

.github/workflows/proof_tools.yml

@@ -8,7 +8,7 @@ jobs:
       fail-fast: false
       matrix:
         ocaml-compiler:
-          - 4.08.x
+          - 4.11.x
           - 4.13.x
 
     runs-on: ubuntu-latest
@@ -46,3 +46,10 @@ jobs:
         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

proofs/dune-exe.mk

@@ -16,6 +16,7 @@ psnj-${ROOT}: _build/default/${ROOT}.exe
 
 tests: _build/default/${ROOT}.exe
 	@${OPAM} exec -- ${DUNE} runtest
+	@echo 'Success'
 
 .if ${CMDLINER}
 ${EXE}.1: ${EXE}

proofs/qfo/Makefile

 PREFIX ?= /usr/local
-dune ?= dune
 
 _EXE = _build/default/bin/qfo.exe
 
 all: psnj-qfo psnj-qfo.1
 
 ${_EXE}:
-	@dune build
+	@opam exec dune build
 	
 psnj-qfo: ${_EXE}
 	@ln -sf ${_EXE} $@
@@ -24,6 +23,10 @@ uninstall:
 
 clean:
 	rm -f psnj-qfo psnj-qfo.1
-	dune clean
+	opam exec -- dune clean
 
-.PHONY: install uninstall clean
+tests:
+	@opam exec -- dune runtest
+	@echo 'Success'
+
+.PHONY: install uninstall clean tests

proofs/qfo/bin/qfo.ml

@@ -51,7 +51,12 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
   Library.set_lib_root lib_root;
   List.iter Library.add_mapping map_dir;
   Console.State.push ();
-  Package.apply_config (Sys.getcwd ());
+  (* Try to find lambdapi pkgs from current working directory, and do
+     nothing if it fails *)
+  try 
+    Package.apply_config (Sys.getcwd ());
+    Format.eprintf "Loaded package file from \"%s\"@." (Sys.getcwd ());
+  with Error.Fatal _ -> ();
   let mp = [ "<stdin>" ] in
   let sign = Sig_state.create_sign mp in
   let ss = Sig_state.of_sign sign in
@@ -132,8 +137,8 @@ let cmd =
     [
       `S Manpage.s_description
     ; `P
-        "$(tname) is a filter that transforms Dedukti files containing alist \
-         of axioms expressed in PVS-Cert into a list of axioms expressed in \
+        "$(tname) is a filter that transforms a list of Dedukti axioms \
+         encoded in PVS-Cert with dependent logical connectives into a list of axioms expressed in \
          something close to first order logic."
     ; `P
         "To convert files, the program needs identify the symbols of the \

proofs/qfo/dune-project

 (lang dune 2.9)
-(name lpvs)
+(name pvs_lp_qfo)
 (cram enable)
+
+(generate_opam_files true)
+(maintainers "dedukti-dev@inria.fr")
+
+(package
+ (name pvs_lp_qfo)
+ (synopsis "Transform PVS-Cert encoded lambdapi to solver friendly encodings")
+ (depends cmdliner yojson lambdapi))

proofs/qfo/pvs_lp_qfo.opam

+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Transform PVS-Cert encoded lambdapi to solver friendly encodings"
+maintainer: ["dedukti-dev@inria.fr"]
+depends: [
+  "dune" {>= "2.9"}
+  "cmdliner"
+  "yojson"
+  "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]
+]