diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d78f1eabf..e9a93dd52 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -33,6 +33,14 @@ jobs: run: | opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }} opam install --deps-only --yes ./cerberus-lib.opam + opam switch create with_coq ${{ matrix.version }} + eval $(opam env --switch=with_coq) + opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released + opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git + opam repo add --yes --this-switch iris-dev https://gitlab.mpi-sws.org/iris/opam.git + opam pin --yes -n coq-sail https://github.com/rems-project/coq-sail.git + opam pin --yes -n coq-cheri-capabilities https://github.com/rems-project/coq-cheri-capabilities.git + opam install --deps-only --yes ./cerberus-lib.opam ./cerberus-cheri.opam - name: Save cached opam if: steps.cache-opam-restore.outputs.cache-hit != 'true' @@ -44,12 +52,37 @@ jobs: - name: Install Cerberus run: | - eval $(opam env) + opam switch ${{ matrix.version }} + eval $(opam env --switch=${{ matrix.version }}) opam pin --yes --no-action add cerberus-lib . opam pin --yes --no-action add cerberus . opam install --yes cerberus - name: Run Cerberus CI tests run: | - eval $(opam env) - cd tests; USE_OPAM='' ./run-ci.sh \ No newline at end of file + opam switch ${{ matrix.version }} + eval $(opam env --switch=${{ matrix.version }}) + cd tests; USE_OPAM='' ./run-ci.sh + cd .. + + - name: Install CN + run: | + opam switch ${{ matrix.version }} + eval $(opam env --switch=${{ matrix.version }}) + opam pin --yes --no-action add cn . + opam install --yes cn + + - name: Install Cerberus-CHERI + if: ${{ matrix.version == '4.14.1' }} + run: | + opam switch with_coq + eval $(opam env --switch=with_coq) + opam pin --yes --no-action add cerberus-lib . + opam pin --yes --no-action add cerberus-cheri . + opam install --yes cerberus-cheri + + # - name: Run Cerberus-CHRI tests + # if: ${{ matrix.version == '4.14.1' }} + # run: | + # eval $(opam env --switch=with_coq) + # make cheri-test diff --git a/cn.opam b/cn.opam index deec1a63f..8636fc873 100644 --- a/cn.opam +++ b/cn.opam @@ -3,8 +3,23 @@ synopsis: "The CN type system" description: "The CN type system" maintainer: ["Christopher Pulte "] depends: [ + "cerberus-lib" "ppx_tools" "monomorphic" "ppx_deriving" "z3" {>= "4.8.14"} ] +build: [ + ["dune" "subst"] {pinned} + ["dune" + "build" + "-p" + name + "--profile=release" + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] \ No newline at end of file