diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml
index 2ac6f49c73d4de7fd49fc96f08fbffe314aebd10..3e39502a6afd1cab3404de6195a4d5f9f71df703 100644
--- a/.github/workflows/proof_tools.yml
+++ b/.github/workflows/proof_tools.yml
@@ -31,6 +31,8 @@ jobs:
cd "${GITHUB_WORKSPACE}"/personoj/proofs/dopth || exit 1
opam install dune --yes
opam exec -- dune build
+ opam install ocamlformat
+ opam exec -- dune build @fmt
opam exec -- dune runtest
- name: chainprops
@@ -38,6 +40,8 @@ jobs:
cd "${GITHUB_WORKSPACE}"/personoj/proofs/chainprops || exit 1
opam install . --deps-only --yes
opam exec -- dune build
+ opam install ocamlformat
+ opam exec -- dune build @fmt
opam exec -- dune runtest
- name: appaxiom
@@ -45,6 +49,8 @@ jobs:
cd "${GITHUB_WORKSPACE}"/personoj/proofs/appaxiom || exit 1
opam install . --deps-only --yes
opam exec -- dune build
+ opam install ocamlformat
+ opam exec -- dune build @fmt
opam exec -- dune runtest
- name: qfo
@@ -52,4 +58,6 @@ jobs:
cd "${GITHUB_WORKSPACE}"/personoj/proofs/qfo || exit 1
opam install . --deps-only --yes
opam exec -- dune build
+ opam install ocamlformat
+ opam exec -- dune build @fmt
opam exec -- dune runtest
diff --git a/proofs/appaxiom/tests/dune b/proofs/appaxiom/tests/dune
index 3dc07d15f2d624f8d79d74eb45cc4104b44551aa..3ffdfab4131b5a0fdd1fda0a9334813cee73042d 100644
--- a/proofs/appaxiom/tests/dune
+++ b/proofs/appaxiom/tests/dune
@@ -1,3 +1,2 @@
(cram
- (deps
- ../appaxiom.exe))
+ (deps ../appaxiom.exe))
diff --git a/proofs/chainprops/dune b/proofs/chainprops/dune
index beb7fb13a9905c575399eec93388191567ac19ec..fc6bf90c2a7f0348c4cab9a31e7ef89cf223b2fd 100644
--- a/proofs/chainprops/dune
+++ b/proofs/chainprops/dune
@@ -1,4 +1,3 @@
(executable
(name chainprops)
- (libraries angstrom cmdliner
- lambdapi.common lambdapi.parsing))
+ (libraries angstrom cmdliner lambdapi.common lambdapi.parsing))
diff --git a/proofs/chainprops/test/dune b/proofs/chainprops/test/dune
index 4b0acc71d9b4d3b2b445628f4a04212b7e3bd893..dfa5154a06c2b555b45c9fe51fc6e26be62dc298 100644
--- a/proofs/chainprops/test/dune
+++ b/proofs/chainprops/test/dune
@@ -1,7 +1,2 @@
(cram
- (deps
- ../chainprops.exe
- example.lp
- example.dep
- foo.lp
- foo.dep))
+ (deps ../chainprops.exe example.lp example.dep foo.lp foo.dep))
diff --git a/proofs/dopth/tests/dune b/proofs/dopth/tests/dune
index 792f222562bbcd160e2b5e56de8610c6b19a5d54..4188c17b72c4842cdeeb4767ab73fdfc0c23a1f1 100644
--- a/proofs/dopth/tests/dune
+++ b/proofs/dopth/tests/dune
@@ -1,4 +1,2 @@
(cram
- (deps
- ../dopth.exe
- example.plain))
+ (deps ../dopth.exe example.plain))
diff --git a/proofs/qfo/.ocamlformat b/proofs/qfo/.ocamlformat
new file mode 100644
index 0000000000000000000000000000000000000000..42e44b125e415b03c85ff79fe6f79b950e3b022f
--- /dev/null
+++ b/proofs/qfo/.ocamlformat
@@ -0,0 +1,5 @@
+break-separators=before
+break-sequences=false
+break-struct=natural
+module-item-spacing=compact
+
diff --git a/proofs/qfo/bin/qfo.ml b/proofs/qfo/bin/qfo.ml
index 625cb4bca467a6191fd9c65a411bf3e3cd2f39ff..7c2a94128d95775f522c91599bb999b23119f64d 100644
--- a/proofs/qfo/bin/qfo.ml
+++ b/proofs/qfo/bin/qfo.ml
@@ -53,59 +53,60 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
Console.State.push ();
(* Try to find lambdapi pkgs from current working directory, and do
nothing if it fails *)
- try
+ 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
- let pcert_ss =
- let ast =
- Parser.parse_string "lpvs"
- "require open lpvs.encoding.lhol lpvs.encoding.pcert \
- lpvs.encoding.depconnectives;"
+ 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
+ let pcert_ss =
+ let ast =
+ Parser.parse_string "lpvs"
+ "require open lpvs.encoding.lhol lpvs.encoding.pcert \
+ lpvs.encoding.depconnectives;"
+ in
+ compile_ast ss ast
in
- compile_ast ss ast
- in
- let module Pcert = (val PvsLp.Encodings.mkpcert pcertmap pcert_ss) in
- Console.out 1 "Loaded PVS-Cert encoding";
- let module DepConn =
- (val let dep_conn_ss =
- let ast =
- (* WARNING: [open] is used because the [require open] of the
- previous command has some side effects which records that it
- has been required. *)
- Parser.parse_string "lpvs"
- "open lpvs.encoding.lhol; open lpvs.encoding.depconnectives;"
+ let module Pcert = (val PvsLp.Encodings.mkpcert pcertmap pcert_ss) in
+ Console.out 1 "Loaded PVS-Cert encoding";
+ let module DepConn =
+ (val let dep_conn_ss =
+ let ast =
+ (* WARNING: [open] is used because the [require open] of the
+ previous command has some side effects which records that it
+ has been required. *)
+ Parser.parse_string "lpvs"
+ "open lpvs.encoding.lhol; open lpvs.encoding.depconnectives;"
+ in
+ compile_ast ss ast
in
- compile_ast ss ast
- in
- PvsLp.Encodings.mkconnectors depconnectives dep_conn_ss)
- in
- let prop_calc_ss =
- let ast =
- Parser.parse_string "lpvs"
- "open lpvs.encoding.lhol;require open lpvs.encoding.connectives;"
+ PvsLp.Encodings.mkconnectors depconnectives dep_conn_ss)
in
- compile_ast ss ast
- in
- let module Propc =
- (val PvsLp.Encodings.mkconnectors connectives prop_calc_ss)
- in
- Console.out 1 "Loaded classical propositional calculus";
- let module Tran = PvsLp.LpCert.PropOfPcert (Pcert) (DepConn) (Propc) in
- let ast = Parser.parse stdin in
- let _ss = compile_ast pcert_ss ast in
- let syms = get_symbols sign in
- let tr_pp name (ty, _) =
- try
- let propty = Tran.f ty in
- Format.printf "@[symbol %s:@ %a;@]@." name Print.pp_term propty
- with Tran.CannotTranslate t ->
- Format.eprintf "Cannot translate %a@." Print.pp_term t
- in
- StrMap.iter tr_pp syms
+ let prop_calc_ss =
+ let ast =
+ Parser.parse_string "lpvs"
+ "open lpvs.encoding.lhol;require open lpvs.encoding.connectives;"
+ in
+ compile_ast ss ast
+ in
+ let module Propc =
+ (val PvsLp.Encodings.mkconnectors connectives prop_calc_ss)
+ in
+ Console.out 1 "Loaded classical propositional calculus";
+ let module Tran = PvsLp.LpCert.PropOfPcert (Pcert) (DepConn) (Propc) in
+ let ast = Parser.parse stdin in
+ let _ss = compile_ast pcert_ss ast in
+ let syms = get_symbols sign in
+ let tr_pp name (ty, _) =
+ try
+ let propty = Tran.f ty in
+ Format.printf "@[symbol %s:@ %a;@]@." name Print.pp_term propty
+ with Tran.CannotTranslate t ->
+ Format.eprintf "Cannot translate %a@." Print.pp_term t
+ in
+ StrMap.iter tr_pp syms
open Cmdliner
@@ -137,9 +138,9 @@ let cmd =
[
`S Manpage.s_description
; `P
- "$(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."
+ "$(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 \
encoding. The mapping allows to indicate the name of such symbols. \