Merge branch 'master' of https://github.com/rems-project/cerberus

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

cn.opam

@@ -3,8 +3,23 @@ synopsis: "The CN type system"
 description: "The CN type system"
 maintainer: ["Christopher Pulte <cp526@cl.cam.ac.uk>"]
 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}
+ ]
+]