diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 81a2148ee3..816aee7e2f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -277,11 +277,15 @@ jobs: - uses: ocaml/setup-ocaml@v2 with: - ocaml-compiler: 4.12.x + ocaml-compiler: 4.14.x - run: opam repo add coq-released https://coq.inria.fr/opam/released - - run: opam install -y coq=8.13.2 coq-bits=1.1.0 + - run: opam install -y coq=8.15.2 coq-bits=1.1.0 + + # If you change the entree-specs commit below, make sure you update the + # documentation in saw-core-coq/README.md accordingly. + - run: opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#b011f29680fdde87489bc06ae98bfff0f97795b3 # FIXME: the following steps generate Coq libraries for the SAW core to # Coq translator and builds them; if we do other Coq tests, these steps diff --git a/saw-core-coq/README.md b/saw-core-coq/README.md index be4f53af03..e229b500df 100644 --- a/saw-core-coq/README.md +++ b/saw-core-coq/README.md @@ -30,17 +30,25 @@ version of Coq needed for those libraries: sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) opam init opam repo add coq-released https://coq.inria.fr/opam/released -opam install coq-bits +opam install -y coq-bits +opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#b011f29680fdde87489bc06ae98bfff0f97795b3 +``` + +We have pinned the `entree-specs` dependency's commit to ensure that it points +to a known working version. If you are an advanced user who wishes to use the +latest `entree-specs commit, you can ommit the commit hash: + +``` +opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git ``` If you run into any issue that is probably due to the version mismatch between the `ocamlc` and the `ocaml` base system installed on your machine and it can be fixed as explained [here](https://github.com/ocaml/opam/issues/3708). -Currently, the Coq support libraries for `saw-core-coq` requires Coq 8.13 or -later. In particular, they are known to build with Coq 8.13, 8.15, and 8.16, -but *not* 8.14 (see [this -issue](https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Code.20typechecks.20in.20Coq.208.2E13.2C.20but.20not.20in.208.2E14)). +Currently, the Coq support libraries for `saw-core-coq` requires Coq 8.15. +Note that the `entree-specs` dependency does not currently build with Coq 8.16 +(see [this issue](https://github.com/GaloisInc/entree-specs/issues/1)). ## Building the and Using the Coq Support Libraries