formatting

.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

proofs/appaxiom/tests/dune

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

proofs/chainprops/dune

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

proofs/chainprops/test/dune

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

proofs/dopth/tests/dune

 (cram
- (deps
-  ../dopth.exe
-  example.plain))
+ (deps ../dopth.exe example.plain))

proofs/qfo/.ocamlformat

+break-separators=before
+break-sequences=false
+break-struct=natural
+module-item-spacing=compact
+

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