Commit 38ba379f authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' into gen_proofmode

parents f9fc75c6 6bb2f803
Pipeline #10093 passed with stage
in 35 minutes and 10 seconds
......@@ -21,23 +21,28 @@ For a version compatible with Coq 8.6, have a look at the
If you need to work with Coq 8.5, please check out the
[iris-3.0 branch](https://gitlab.mpi-sws.org/FP/iris-coq/tree/iris-3.0).
### Installing via opam
### Working *with* Iris
To obtain the latest stable release via opam (1.2.2 or newer), you have to add
the Coq opam repository:
To use Iris in your own proofs, we recommend you install Iris via opam (1.2.2 or
newer). To obtain the latest stable release, you have to add the Coq opam
repository:
opam repo add coq-released https://coq.inria.fr/opam/released
Then you can do `opam install coq-iris`.
To obtain a development version, add the Iris opam repository:
To obtain a development version, also add the Iris opam repository:
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
### Building from source
Either way, you can now do `opam install coq-iris`. To fetch updates later, run
`opam update && opam upgrade`. However, notice that we do not guarnatee
backwards-compatibility, so upgrading Iris may break your Iris-using
developments.
### Working *on* Iris
When building Iris from source, we recommend to use opam (1.2.2 or newer) for
installing Iris's dependencies. This requires the following two repositories:
To work on Iris itself, you need to install its build-dependencies. Again we
recommend you do that with opam (1.2.2 or newer). This requires the following
two repositories:
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
......
Subproject commit 8324acefba3ffef86b4c5eca3c961ce69dc4dd02
Subproject commit 1664067bf3f01bd7a081874d26c21e26ad2a3bbf
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