diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml index be40fbefeaa0d3c28c22ec9ed2e84ddf211bf121..d067d83fec6ae3b79f8f6bb81397aa0cb78f968a 100644 --- a/.github/workflows/proof_tools.yml +++ b/.github/workflows/proof_tools.yml @@ -28,5 +28,7 @@ jobs: run: | cd proofs/psnj_toolbox || exit 1 opam install . --deps-only --yes + opam install ocamlformat + opam exec -- dune build @fmt opam exec -- dune build opam exec -- dune test diff --git a/proofs/psnj_toolbox/bin/main.ml b/proofs/psnj_toolbox/bin/main.ml index 74810c27b34990050f2dae864c4c64b050e1e5f5..ccf1814f2812a92fed45c2487ac004da70b16059 100644 --- a/proofs/psnj_toolbox/bin/main.ml +++ b/proofs/psnj_toolbox/bin/main.ml @@ -13,7 +13,7 @@ let cmds = Autosolve.cmd; Qfo.cmd; Group.cmd; - Pipe.cmd + Pipe.cmd; ] let () = Term.(exit @@ eval_choice default_cmd cmds) diff --git a/proofs/psnj_toolbox/pipe_tests/ex/dune b/proofs/psnj_toolbox/pipe_tests/ex/dune index a02c2cdf2b995f1d4c38bb8fc20de49151299146..ae001bce2537d5eaf7f0dc8d85461db4228bd13a 100644 --- a/proofs/psnj_toolbox/pipe_tests/ex/dune +++ b/proofs/psnj_toolbox/pipe_tests/ex/dune @@ -7,4 +7,5 @@ (glob_files encoding/*) (glob_files spec/main.lp)) (libraries unix) - (action (run ./ex.exe %{bin:psnj}))) + (action + (run ./ex.exe %{bin:psnj}))) diff --git a/proofs/psnj_toolbox/pipe_tests/ex/ex.ml b/proofs/psnj_toolbox/pipe_tests/ex/ex.ml index ff49298f935d79bd49cb8a9798a6fc5f01bdd6fa..cb263ff4c2065a6e1f9004640099c5d6807acf0b 100644 --- a/proofs/psnj_toolbox/pipe_tests/ex/ex.ml +++ b/proofs/psnj_toolbox/pipe_tests/ex/ex.ml @@ -4,8 +4,8 @@ let () = (Filename.quote_command Sys.argv.(1) [ "pipe"; "--qfo"; "encoding/qfo.json"; "ex.log" ]) with - | Unix.WEXITED 0 -> - ignore @@ Unix.system (Filename.quote_command "cat" ["exi.lp"]) + | Unix.WEXITED 0 -> + ignore @@ Unix.system (Filename.quote_command "cat" [ "exi.lp" ]) | Unix.WEXITED n -> Format.eprintf "Command exited with code %d@." n; exit 1 diff --git a/proofs/psnj_toolbox/pipe_tests/hello/dune b/proofs/psnj_toolbox/pipe_tests/hello/dune index cfaa9d62072efff6d5ba3e7c8db22d9739736940..507c94ef98086cf16b96788845b220a537a0c419 100644 --- a/proofs/psnj_toolbox/pipe_tests/hello/dune +++ b/proofs/psnj_toolbox/pipe_tests/hello/dune @@ -7,4 +7,5 @@ (glob_files encoding/*) (glob_files spec/main.lp)) (libraries unix) - (action (run ./hello.exe %{bin:psnj}))) + (action + (run ./hello.exe %{bin:psnj}))) diff --git a/proofs/psnj_toolbox/pipe_tests/hello/hello.ml b/proofs/psnj_toolbox/pipe_tests/hello/hello.ml index 0a64c40fb310b2014ae0c6171772eec4e7cc6767..939fe02f6bd81f03b1aceebc27f966c828a0f3fd 100644 --- a/proofs/psnj_toolbox/pipe_tests/hello/hello.ml +++ b/proofs/psnj_toolbox/pipe_tests/hello/hello.ml @@ -5,7 +5,7 @@ let () = [ "pipe"; "--qfo"; "encoding/qfo.json"; "hello.log" ]) with | Unix.WEXITED 0 -> - ignore (Unix.system (Filename.quote_command "cat" ["hello.lp"])) + ignore (Unix.system (Filename.quote_command "cat" [ "hello.lp" ])) | Unix.WEXITED n -> Format.eprintf "Command exited with code %d@." n; exit 1 diff --git a/proofs/psnj_toolbox/pipe_tests/multiproofs/dune b/proofs/psnj_toolbox/pipe_tests/multiproofs/dune index f8b2749ab9f5d619dec376a04d660c54277fd7c0..3d197662d8bb3132b98f103210e02da6f48e8d02 100644 --- a/proofs/psnj_toolbox/pipe_tests/multiproofs/dune +++ b/proofs/psnj_toolbox/pipe_tests/multiproofs/dune @@ -7,4 +7,5 @@ (glob_files encoding/*) (glob_files spec/main.lp)) (libraries unix) - (action (run ./mp.exe %{bin:psnj}))) + (action + (run ./mp.exe %{bin:psnj})))