update docs, also to account for multi-package

CHANGELOG.md

@@ -7,6 +7,9 @@ lemma.
 
 With this release, we dropped support for Coq 8.9.
 
+We also split Iris into multiple opam packages: `coq-iris` no longer contains
+HeapLang, which is now in a separate package `coq-iris-heap-lang`.
+
 **Changes in `algebra`:**
 
 * Rename `agree_op_inv'` to `to_agree_op_inv`,

CONTRIBUTING.md

@@ -5,6 +5,23 @@ Iris development.  This is for contributing to Iris itself; see
 [the README](README.md#further-resources) for resources helpful for all Iris
 users.
 
+To work on Iris itself, you need to install its build-dependencies.  Again we
+recommend you do that with opam (2.0.0 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/iris/opam.git
+
+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`.
+
 ## How to submit a merge request
 
 To contribute code, you need an [MPI-SWS GitLab account][account] (use the
@@ -48,6 +65,20 @@ Coq-8.8-specific `.ref` file).  If you change one of these, remember to update
 
 If you want to compile without tests run `make NO_TEST=1`.
 
+## How to build/install only one package
+
+Iris is split into multiple packages that can be installed separately via opam.
+You can invoke the Makefile of a particular package by doing `./make-package
+$PACKAGE $MAKE_ARGS`, where `$MAKE_ARGS` are passed to `make` (so you can use
+the usual `-jN`, `install`, ...).  This should only rarely be necessary. For
+example, if you are not using opam and you want to install only the `iris`
+package (without HeapLang, to avoid waiting on that part of the build), you can
+do `./make-package iris install`.  (If you are using opam, you can achieve the
+same by pinning `coq-iris` to your Iris checkout.)
+
+Note that `./make-package` will never run the test suite, so please always do a
+regular `make -jN` before submitting an MR.
+
 ## How to measure the timing effect on a reverse dependency
 
 So say you did a change in Iris, and want to know how it affects [lambda-rust]

README.md

@@ -50,34 +50,24 @@ To obtain a development version, also add the Iris opam repository:
 
     opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
 
-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 guarantee
-backwards-compatibility, so upgrading Iris may break your Iris-using
-developments.
-
-The development version of Iris is regularly subject to breaking changes.  If
-you want to be notified of such changes, please let us know your account name on
-the [MPI-SWS GitLab](https://gitlab.mpi-sws.org/) so we can add you to the
+Either way, you can now install Iris:
+- `opam install coq-iris` will install the libraries making up the Iris logic,
+  but leave it up to you to instantiate the `program_logic.language` interface
+  to define a programming language for Iris to reason about.
+- `opam install coq-iris-heap-lang` will additionally install HeapLang, the
+  default language used by various Iris projects.
+
+To fetch updates later, run `opam update && opam upgrade`.  However, notice that
+we do not guarantee backwards-compatibility, so upgrading Iris may break your
+Iris-using developments.  If you want to be notified of breaking changes, please
+let us know your account name on the
+[MPI-SWS GitLab](https://gitlab.mpi-sws.org/) so we can add you to the
 notification group.
 
 ### Working *on* Iris
 
-To work on Iris itself, you need to install its build-dependencies.  Again we
-recommend you do that with opam (2.0.0 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/iris/opam.git
-
-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`.
+See the [contribution guide](CONTRIBUTING.md) for information on how to work on
+the Iris development itself.
 
 ## Directory Structure
 

coq-iris-heap-lang.opam

@@ -7,6 +7,9 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
 
 synopsis: "HeapLang is the canonical example language for Iris"
+description: """
+This package provides the iris.heap_lang Coq module.
+"""
 
 depends: [
   "coq-iris" {= version}

coq-iris.opam

@@ -7,6 +7,10 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
 
 synopsis: "Iris is a Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
+description: """
+This package provides the following Coq modules:
+iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_logic, iris.program_logic.
+"""
 
 depends: [
   "coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }

make-package

@@ -9,6 +9,11 @@ shift
 COQFILE="_CoqProject.$PROJECT"
 MAKEFILE="Makefile.package.$PROJECT"
 
+if ! egrep -q "^$PROJECT/" _CoqProject; then
+    echo "No files in $PROJECT/ found in _CoqProject; this does not seem to be a valid project name."
+    exit 1
+fi
+
 # Generate _CoqProject file and Makefile
 rm -f "$COQFILE"
 # Get the right "-Q" line.