From 166d4014d7ff44946f899acab71d263cfebaabe3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Nov 2020 10:13:07 +0100
Subject: [PATCH] update docs, also to account for multi-package
---
CHANGELOG.md | 3 +++
CONTRIBUTING.md | 31 +++++++++++++++++++++++++++++++
README.md | 38 ++++++++++++++------------------------
coq-iris-heap-lang.opam | 3 +++
coq-iris.opam | 4 ++++
make-package | 5 +++++
6 files changed, 60 insertions(+), 24 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 93c63457d..75e420e68 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 67eef817f..39e074c32 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 bb35b8274..3b38ae5c4 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 d0cfb0627..7c98a1d3a 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 b4c61440f..ec65b98de 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 028220c0d..55c051a9f 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.
--
GitLab