Commit 96d324f6 authored by Ralf Jung's avatar Ralf Jung

update README, stop testing Coq 8.6

parent 54be60b6
...@@ -35,8 +35,3 @@ build-coq.8.7.2: ...@@ -35,8 +35,3 @@ build-coq.8.7.2:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.7.2 coq-mathcomp-ssreflect version 1.7.0" OPAM_PINS: "coq version 8.7.2 coq-mathcomp-ssreflect version 1.7.0"
build-coq.8.6.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.6.1 coq-mathcomp-ssreflect version 1.7.0"
...@@ -9,10 +9,8 @@ This tutorial comes in two versions: ...@@ -9,10 +9,8 @@ This tutorial comes in two versions:
For the tutorial material you need to have the following dependencies installed: For the tutorial material you need to have the following dependencies installed:
- Coq 8.6.1 / 8.7.2 / 8.8.2 - Coq 8.7.2 / 8.8.2
- Ssreflect 1.7.0 - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
- Coq-std++ 1.1
- Iris (latest version)
*Note:* the tutorial material will not work with earlier versions of Iris, it *Note:* the tutorial material will not work with earlier versions of Iris, it
is important to install the exact versions as given above. is important to install the exact versions as given above.
...@@ -25,19 +23,9 @@ opam repository and the Iris development repository (if you have not already ...@@ -25,19 +23,9 @@ opam repository and the Iris development repository (if you have not already
done so earlier): done so earlier):
opam repo add coq-released https://coq.inria.fr/opam/released opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Then you can do `opam install coq-iris`. Then you can do `make build-dep` to install exactly the right version of Iris.
## Installing Iris from source
If you are unable to use opam, you can also build Iris from source. For this,
run `make; make install` for all of:
* ssreflect: <https://github.com/math-comp/math-comp/archive/mathcomp-1.7.0.tar.gz>
(`cd mathcomp/ssreflect` to only compile and install what is needed)
* std++: <https://gitlab.mpi-sws.org/iris/stdpp/repository/coq-stdpp-1.1.0/archive.tar.gz>
* Iris: <https://gitlab.mpi-sws.org/FP/iris-coq/repository/iris-3.1.0/archive.tar.gz>
## Compiling the exercises ## Compiling the exercises
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment