From d2d9f01ce960209838f02af27a75d2d628e4094b Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 9 Dec 2022 10:40:27 -0500 Subject: [PATCH] Install entree-specs as a Coq dependency This updates the CI to build a particular `entree-specs` commit before building the Coq support libraries. This also updates the instructions in the `saw-core-coq` `README` accordingly. Note that this requires limiting the Coq support window to 8.15 for now, as `entree-specs` requires 8.15 as the minimum. In particular, `entree-specs` does not yet support 8.16 (see GaloisInc/entree-specs#1), so we now require Coq 8.15 exactly. --- .github/workflows/ci.yml | 8 ++++++-- saw-core-coq/README.md | 18 +++++++++++++----- 2 files changed, 19 insertions(+), 7 deletions(-) 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