diff --git a/CHANGELOG.md b/CHANGELOG.md
index 93c63457d4938ee0cf79099e96d621bc207f2810..75e420e68e2629617ccfa636f720bce5a8fdb2db 100644
--- a/CHANGELOG.md
+++ b/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`,
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 67eef817ff135946e050e0ed2e2544af05b7ace0..39e074c325fae1e95a3a51a0cd7b9d16cad7f2cc 100644
--- a/CONTRIBUTING.md
+++ b/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]
diff --git a/README.md b/README.md
index bb35b8274154d10963fdd8f8612cb9233c48d163..3b38ae5c476bf7e1631d07d141560f8639c0eaf5 100644
--- a/README.md
+++ b/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
diff --git a/coq-iris-heap-lang.opam b/coq-iris-heap-lang.opam
index d0cfb0627062291ef9926ee0ca53cc4483c91370..7c98a1d3afad868222e43256f99aae58d5f1856a 100644
--- a/coq-iris-heap-lang.opam
+++ b/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}
diff --git a/coq-iris.opam b/coq-iris.opam
index b4c61440f9e687ec068801faa78470664f6e8599..ec65b98decdb9eef1e82809c57b359861d6e151b 100644
--- a/coq-iris.opam
+++ b/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") }
diff --git a/make-package b/make-package
index 028220c0da730662560948cdf7f36e6ad0ce1908..55c051a9f6b9b3d25936782b46e6b55dc35fa4ab 100755
--- a/make-package
+++ b/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.