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

@@ -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

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