From c71618cf5c455c574c8c1d718647e67db50efad0 Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Wed, 1 Dec 2021 11:44:28 +0100
Subject: [PATCH] Fix tests, run test in ci
---
.github/workflows/proof_tools.yml | 9 ++++++++-
proofs/dune-exe.mk | 1 +
proofs/qfo/Makefile | 11 +++++++----
proofs/qfo/bin/qfo.ml | 11 ++++++++---
proofs/qfo/dune-project | 10 +++++++++-
proofs/qfo/lpvs.opam | 0
proofs/qfo/pvs_lp_qfo.opam | 27 +++++++++++++++++++++++++++
7 files changed, 60 insertions(+), 9 deletions(-)
delete mode 100644 proofs/qfo/lpvs.opam
create mode 100644 proofs/qfo/pvs_lp_qfo.opam
diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml
index 82d4701..2ac6f49 100644
--- a/.github/workflows/proof_tools.yml
+++ b/.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
diff --git a/proofs/dune-exe.mk b/proofs/dune-exe.mk
index bc595aa..a7c746f 100644
--- a/proofs/dune-exe.mk
+++ b/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}
diff --git a/proofs/qfo/Makefile b/proofs/qfo/Makefile
index 0dc2357..2109686 100644
--- a/proofs/qfo/Makefile
+++ b/proofs/qfo/Makefile
@@ -1,12 +1,11 @@
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
diff --git a/proofs/qfo/bin/qfo.ml b/proofs/qfo/bin/qfo.ml
index 24c4283..625cb4b 100644
--- a/proofs/qfo/bin/qfo.ml
+++ b/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 \
diff --git a/proofs/qfo/dune-project b/proofs/qfo/dune-project
index 478cf89..9c0c240 100644
--- a/proofs/qfo/dune-project
+++ b/proofs/qfo/dune-project
@@ -1,3 +1,11 @@
(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))
diff --git a/proofs/qfo/lpvs.opam b/proofs/qfo/lpvs.opam
deleted file mode 100644
index e69de29..0000000
diff --git a/proofs/qfo/pvs_lp_qfo.opam b/proofs/qfo/pvs_lp_qfo.opam
new file mode 100644
index 0000000..9e35437
--- /dev/null
+++ b/proofs/qfo/pvs_lp_qfo.opam
@@ -0,0 +1,27 @@
+# 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]
+]
--
GitLab