diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml index 9b94bccb0cd3d29e6fcfa2b1cf84dc5ef1bdcc41..88e04f6193ad92ab76c62c3720edbd0f6ebe9065 100644 --- a/.github/workflows/proof_tools.yml +++ b/.github/workflows/proof_tools.yml @@ -15,8 +15,6 @@ jobs: steps: - uses: actions/checkout@v2 - with: - path: personoj - name: Use ocaml uses: ocaml/setup-ocaml@v2 @@ -28,7 +26,7 @@ jobs: - name: toolbox run: | - cd "${GITHUB_WORKSPACE}"/personoj/proofs/psnj_toolbox || exit 1 + cd proofs/psnj_toolbox || exit 1 opam install . --deps-only --yes opam exec -- dune build opam exe -- dune runtest @@ -42,8 +40,6 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v2 - with: - path: personoj - name: ocaml uses: ocaml/setup-ocaml@v2 @@ -59,13 +55,13 @@ jobs: - name: install tools run: | opam install yojson angstrom feather cmdliner - cd "${GITHUB_WORKSPACE}"/personoj/proofs || exit 1 + cd proofs || exit 1 (cd split && bmake && sudo bmake install) (cd pipeline && bmake && sudo bmake install) (cd psnj_toolbox && make && sudo make install) - name: launch pipeline run: | - cd "${GITHUB_WORKSPACE}"/personoj/proofs/pipeline || exit 1 + cd proofs/pipeline || exit 1 bmake tests diff --git a/proofs/psnj_toolbox/personoj.opam.locked b/proofs/psnj_toolbox/personoj.opam.locked new file mode 100644 index 0000000000000000000000000000000000000000..6aa761bd5665610a74ee5445505a650b31dfb0f6 --- /dev/null +++ b/proofs/psnj_toolbox/personoj.opam.locked @@ -0,0 +1,67 @@ +opam-version: "2.0" +name: "personoj" +version: "~dev" +synopsis: "todo" +depends: [ + "angstrom" {= "0.15.0"} + "base" {= "v0.14.2"} + "base-bigarray" {= "base"} + "base-bytes" {= "base"} + "base-threads" {= "base"} + "base-unix" {= "base"} + "bigarray-compat" {= "1.0.0"} + "bigstringaf" {= "0.8.0"} + "bindlib" {= "5.0.1"} + "biniou" {= "1.2.1"} + "cmdliner" {= "1.0.4"} + "conf-pkg-config" {= "2"} + "cppo" {= "1.6.8"} + "csexp" {= "1.5.1"} + "dune" {= "2.9.1"} + "dune-configurator" {= "2.9.1"} + "easy-format" {= "1.3.2"} + "gen" {= "0.5.3"} + "lambdapi" {= "1.0"} + "menhir" {= "20211128"} + "menhirLib" {= "20211128"} + "menhirSdk" {= "20211128"} + "num" {= "1.4"} + "ocaml" {= "4.11.1"} + "ocaml-compiler-libs" {= "v0.12.4"} + "ocaml-config" {= "1"} + "ocaml-syntax-shims" {= "1.0.0"} + "ocaml-system" {= "4.11.1"} + "ocamlbuild" {= "0.14.0"} + "ocamlfind" {= "1.9.1"} + "ppx_derivers" {= "1.2.1"} + "ppx_sexp_conv" {= "v0.14.3"} + "ppxlib" {= "0.23.0"} + "pratter" {= "1.2"} + "re" {= "1.10.3"} + "result" {= "1.5"} + "sedlex" {= "2.5"} + "seq" {= "base"} + "sexplib0" {= "v0.14.0"} + "stdlib-shims" {= "0.3.0"} + "timed" {= "1.0"} + "uchar" {= "0.0.2"} + "why3" {= "1.4.0"} + "yojson" {= "1.7.0"} +] +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] +] +pin-depends: ["lambdapi.1.0" "git://github.com/gabrielhdt/lambdapi#refiner"] \ No newline at end of file