From c53ec25f563b3b3226b2de6f0aa729926589254a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 18 Dec 2017 13:22:53 +0100
Subject: [PATCH] update README
---
README.md | 29 ++++++++++++++++++++---------
1 file changed, 20 insertions(+), 9 deletions(-)
diff --git a/README.md b/README.md
index f08263023..df1fbcd4a 100644
--- a/README.md
+++ b/README.md
@@ -13,26 +13,37 @@ This version is known to compile with:
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).
-The easiest way to install the correct versions of the dependencies is through
-opam. You will need the Coq and Iris opam repositories:
+## Installing via opam
+
+To obtain the latest stable release via opam, 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:
+
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
-Once you got opam set up, run `make build-dep` to install the right versions
-of the dependencies.
+## Building from source
-## Updating
+When building Iris from source, we recommend to use opam for installing Iris's dependencies.
+This requires the following two repositories:
-After doing `git pull`, the development may fail to compile because of outdated
-dependencies. To fix that, please run `opam update` followed by
-`make build-dep`.
+ 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
-## Building
+Once you got opam set up, run `make build-dep` to install the right versions
+of the dependencies.
Run `make -jN` to build the full development, where `N` is the number of your
CPU cores.
+To update Iris, do `git pull`. After an update, the development may fail to
+compile because of outdated dependencies. To fix that, please run `opam update`
+followed by `make build-dep`.
+
## Directory Structure
* The folder [algebra](theories/algebra) contains the COFE and CMRA
--
GitLab