.gitattributes

 *.v gitlab-language=coq
+
+# Convert to native line endings on checkout.
+*.ref text
+# Shell scripts need Linux line endings.
+*.sh eol=lf

.gitignore

@@ -4,7 +4,6 @@
 *.vio
 *.v.d
 .coqdeps.d
-.Makefile.coq.d
 *.glob
 *.cache
 *.aux
@@ -14,8 +13,15 @@
 *.bak
 .coqdeps.d
 .coq-native/
-build-dep/
-Makefile.coq
-Makefile.coq.conf
 *.crashcoqide
 .env
+builddep/
+_CoqProject.*
+Makefile.coq
+Makefile.coq.conf
+.Makefile.coq.d
+Makefile.package.*
+.Makefile.package.*
+_opam
+_build
+*.install

.gitlab-ci.yml

@@ -5,9 +5,29 @@ stages:
 
 variables:
   CPU_CORES: "10"
+  OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
+  # Avoid needlessly increasing our TCB with native_compute
+  COQEXTRAFLAGS: "-native-compiler no"
+
+.only_branches: &only_branches
+  only:
+  - /^master/@iris/iris
+  - /^ci/@iris/iris
+
+.only_mr: &only_mr
+  only:
+  - merge_requests
+
+.branches_and_mr: &branches_and_mr
+  only:
+  - /^master/@iris/iris
+  - /^ci/@iris/iris
+  - merge_requests
 
 .template: &template
+  <<: *only_branches
   stage: build
+  interruptible: true
   tags:
   - fp
   script:
@@ -17,9 +37,6 @@ variables:
     key: "$CI_JOB_NAME"
     paths:
     - _opam/
-  only:
-  - /^master/@iris/iris
-  - /^ci/@iris/iris
   except:
   - triggers
   - schedules
@@ -27,49 +44,49 @@ variables:
 
 ## Build jobs
 
-build-coq.dev:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version dev"
-
-build-coq.8.12.0:
+# The newest version runs with timing.
+build-coq.8.20.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.12.0"
+    OPAM_PINS: "coq version 8.20.1"
     DENY_WARNINGS: "1"
-    OPAM_PKG: "coq-iris"
+    MANGLE_NAMES: "1"
+    OPAM_PKG: "1"
     DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
     DOC_OPTS: "--external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp"
   tags:
   - fp-timing
+  interruptible: false
 
-build-coq.8.11.2:
+# The newest version also runs in MRs, without timing.
+build-coq.8.20.1-mr:
   <<: *template
+  <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.11.2"
+    OPAM_PINS: "coq version 8.20.1"
+    DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
 
-build-coq.8.10.2:
+# Also ensure Dune works.
+build-coq.8.20.1-dune:
   <<: *template
+  <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.10.2"
+    OPAM_PINS: "coq version 8.20.1   dune version 3.15.2"
+    MAKE_TARGET: "dune"
 
-# Nightly job with a known-to-work Coq version
-# (so failures must be caused by std++)
-build-stdpp.dev-coq.8.11.2:
+# The oldest version runs in MRs, without name mangling.
+build-coq.8.19.2:
   <<: *template
+  <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.11.2   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV"
-  except:
-  only:
-  - triggers
-  - schedules
-  - api
+    OPAM_PINS: "coq version 8.19.2"
 
-# Nightly job with latest Coq branch
-build-stdpp.dev-coq.8.12.dev:
+trigger-stdpp.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.12.dev   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV"
+    STDPP_REPO: "iris/stdpp"
+    OPAM_PINS: "coq version $NIGHTLY_COQ   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV"
     CI_COQCHK: "1"
   except:
   only:

.gitmodules

-[submodule "ci"]
-	path = ci
-	url = https://gitlab.mpi-sws.org/FP/iris-ci.git

CONTRIBUTING.md

@@ -5,21 +5,46 @@ 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 builddep` 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 builddep`.
+
 ## How to submit a merge request
 
-To contribute code, you need an [MPI-SWS GitLab account][account] (use the
-"Register" tab).  Please send your MPI-SWS GitLab username to [Ralf Jung][jung]
-to enable personal projects for your account.  Then you can fork the
+To contribute code, you need an MPI-SWS GitLab account as described on the
+[chat page](https://iris-project.org/chat.html).  Then you can fork the
 [Iris git repository][iris], make your changes in your fork, and create a merge
-request.
+request.  If forking fails with an error, please send your MPI-SWS GitLab
+username to [Ralf Jung][jung] to unlock forks for your account.
 
 Please do *not* use the master branch of your fork, that might confuse CI.  Use
 a feature branch instead.
 
-[account]: https://gitlab.mpi-sws.org/users/sign_in
 [jung]: https://gitlab.mpi-sws.org/jung
 [iris]: https://gitlab.mpi-sws.org/iris/iris
 
+We prefer small and self-contained merge requests that add a single feature
+over merge requests that add arbitrary collections of lemmas. Small merge
+requests are easier to review, and will typically be merged more quickly
+(because it avoids blocking the whole merge request on a single
+discussion).
+
+Please follow the coding style laid out in our [style
+guide](docs/style_guide.md).
+
 ## How to update the std++ dependency
 
 * Do the change in std++, push it.
@@ -28,7 +53,7 @@ a feature branch instead.
 * In Iris, change the `opam` file to depend on the new version.
   (In case you do not use opam yourself, you can see recently published versions
   [in this repository](https://gitlab.mpi-sws.org/iris/opam/commits/master).)
-* Run `make build-dep` (in Iris) to install the new version of std++.
+* Run `make builddep` (in Iris) to install the new version of std++.
   You may have to do `make clean` as Coq will likely complain about .vo file
   mismatches.
 
@@ -48,51 +73,60 @@ 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 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]
-or the [examples].  To do this, check out the respective project and change its
-`.gitlab-ci.yml` to contain only one build job, which should look like
+## 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 test effects on reverse dependencies
+
+The `iris-bot` script makes it easy to test the effect of a branch on reverse
+dependencies. It can start tests ensuring they all still build, and it can do
+comparative timing runs.
+
+If you have suitable permissions, you can trigger these builds yourself.
+But first, you need to do some setup: you need to create a GitLab access token
+and set the `GITLAB_TOKEN` environment variable to it. Go to
+<https://gitlab.mpi-sws.org/-/profile/personal_access_tokens>, pick a suitable
+name (such as "iris-bot"), select the "api" scope, and then click "Create
+personal access token". Copy the value it shows and store it in some suitable
+place; you will not be able to retrieve this value from GitLab in the future!
+For example, you could create a `.env` file in your Iris clone containing:
 ```
-build-iris.dev:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.9.0   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#yourname/feature"
-    TIMING_CONF: "coq-8.9.0"
-  tags:
-  - fp-timing
+export GITLAB_TOKEN=<your token here>
 ```
-You will have to adjust this a bit: you should use the same Coq version as
-whatever the master branch uses for its timing job, which you can determine by
-checking its `.gitlab-ci.yml`.  If you change the Coq version, remember to do it
-in both places (`OPAM_PINS` and `TIMING_CONF`).  You will also have to adjust
-the Iris branch being used, which is determined after the `#` in `OPAM_PINS`.
-If you are in doubt, ask on Mattermost *before* pushing your branch.  Please
-double-check that the job name is `build-iris.dev` to avoid polluting the caches
-of regular CI builds!  This way, you are going to share the cache with the
-nightly builds, which is fine.
-
-Once you are confident with your CI configuration, push this to a new branch
-whose name starts with `ci/`.  It should usually be of the form
-`ci/yourname/feature`.  You should see a pipeline running in GitLab with just a
-single job, and you can follow its progress there.
-
-When the job is done, you should be able to see it as a single dot on our
-[statistics server][coq-speed] after selecting the right project and branch.
-Click on "Coq-Speed" on the top-left corner to switch to another dashboard, and
-select "Coq-Compare".  Now you can select the project and the two measurements
-you want to compare, which would be the SHA of the commit you just created as
-"Commit 2", and the SHA of its parent as "Commit 1".  Don't forget to also
-select the right configuration for both of them.  The "Grouping" is a regular
-expression that you can use to switch between per-file, per-directory and
-per-project grouping of the measurements.
-
-If you changed your Iris branch and want to make another measurement, *do not*
-just "Retry" the CI job.  That will lead to an error, because you would end up
-with two measurements for the same commit.  Instead, create an empty commit in
-your branch of the to-be-measured project (`git commit --allow-empty -m
-"rerun"`), and push that.
-
-[lambda-rust]: https://gitlab.mpi-sws.org/iris/lambda-rust
+Then you can easily get the token back into the environment via `. .env`.
+
+Once that setup is done, you can now use `iris-bot`. Set at least one of
+`IRIS_REV` or `STDPP_REV` to control which branches of these projects to build
+against (they default to the default git branch). `IRIS_REPO` and `STDPP_REPO`
+can be used to control the repository in which the branch is situated. Setting
+`IRIS` to "user:branch" will use the given branch on that user's fork of Iris,
+and similar for `STDPP`.
+
+Supported commands:
+- `./iris-bot build [$filter]`: Builds all reverse dependencies against the
+  given branches. The optional `filter` argument only builds projects whose
+  names contains that string.
+- `./iris-bot time $project`: Measure the impact of this branch on the build
+  time of the given reverse dependency. Only Iris branches are supported for
+  now.
+
+Examples:
+- `IRIS_REV=myname/mybranch ./iris-bot build` builds *all* reverse dependencies
+  against `myname/mybranch` from the main Iris repository.
+- `IRIS=user:branch ./iris-bot build examples` builds the [examples] against
+  the `branch` in `user`'s fork of Iris.
+- `IRIS_REV=myname/mybranch ./iris-bot time examples` measures the timing impact
+  of `myname/mybranch` from the main Iris repository on the [examples].
+
 [examples]: https://gitlab.mpi-sws.org/iris/examples
-[coq-speed]: https://coq-speed.mpi-sws.org

Makefile

+# Default target
+all: Makefile.coq
+	+@$(MAKE) -f Makefile.coq all
+.PHONY: all
+
+# Build with dune.
+# This exists only for CI; you should just call `dune build` directly instead.
+dune:
+	@dune build --display=short
+.PHONY: dune
+
 # Permit local customization
 -include Makefile.local
 
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
-	+@make -f Makefile.coq $@
-
-all: Makefile.coq
-	+@make -f Makefile.coq all
-.PHONY: all
+	@#echo "Forwarding $@"
+	+@$(MAKE) -f Makefile.coq $@
+phony: ;
+.PHONY: phony
 
 clean: Makefile.coq
-	+@make -f Makefile.coq clean
-	find theories tests exercises solutions \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
-	rm -f Makefile.coq .lia.cache
+	+@$(MAKE) -f Makefile.coq clean
+	@# Make sure not to enter the `_opam` folder.
+	find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
+	rm -f Makefile.coq .lia.cache builddep/*
 .PHONY: clean
 
 # Create Coq Makefile.
@@ -20,27 +31,31 @@ Makefile.coq: _CoqProject Makefile
 	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
 
 # Install build-dependencies
-build-dep/opam: opam Makefile
-	@echo "# Creating build-dep package."
-	@mkdir -p build-dep
-	@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
-	@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
-
-build-dep: build-dep/opam phony
-	@# We want opam to not just instal the build-deps now, but to also keep satisfying these
+OPAMFILES=$(wildcard *.opam)
+BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
+
+builddep/%-builddep.opam: %.opam Makefile
+	@echo "# Creating builddep package for $<."
+	@mkdir -p builddep
+	@sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
+
+builddep-opamfiles: $(BUILDDEPFILES)
+.PHONY: builddep-opamfiles
+
+builddep: builddep-opamfiles
+	@# We want opam to not just install the build-deps now, but to also keep satisfying these
 	@# constraints.  Otherwise, `opam upgrade` may well update some packages to versions
 	@# that are incompatible with our build requirements.
 	@# To achieve this, we create a fake opam package that has our build-dependencies as
 	@# dependencies, but does not actually install anything itself.
-	@echo "# Installing build-dep package."
-	@opam install $(OPAMFLAGS) build-dep/
+	@echo "# Installing builddep packages."
+	@opam install $(OPAMFLAGS) $(BUILDDEPFILES)
+.PHONY: builddep
 
-# Some files that do *not* need to be forwarded to Makefile.coq
-Makefile: ;
-_CoqProject: ;
-opam: ;
-Makefile.local: ;
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
 
-# Phony wildcard targets
-phony: ;
-.PHONY: phony
+# Some files that do *not* need to be forwarded to Makefile.coq.
+# ("::" lets Makefile.local overwrite this.)
+Makefile Makefile.local _CoqProject $(OPAMFILES):: ;

Makefile.coq.local

@@ -4,23 +4,33 @@ NO_TEST:=
 # use MAKE_REF=1 to generate new reference files
 MAKE_REF:=
 
+# Only test reference output on known versions of Coq, to avoid blocking
+# Coq CI when they change the printing a little.
+# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
+COQ_REF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(20)\." -q && echo 1)
+
 # Run tests interleaved with main build.  They have to be in the same target for this.
-real-all: $(if $(NO_TEST),,test)
+real-all: style $(if $(NO_TEST),,test)
+
+style: $(VFILES) coq-lint.sh
+# Make sure everything imports the options, and some general linting.
+	$(SHOW)"COQLINT"
+	$(HIDE)for FILE in $(VFILES); do \
+	  if ! grep -F -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
+	  ./coq-lint.sh "$$FILE" || exit 1; \
+	done
+# Make sure main Iris does not import other Iris packages.
+	$(HIDE)if grep -E 'iris\.(heap_lang|deprecated|unstable)' --include "*.v" -R iris; then echo "ERROR: Iris may not import modules from other Iris packages (see above for violations)."; echo; exit 1; fi
+.PHONY: style
 
 # the test suite
-TESTFILES:=$(wildcard tests/*.v)
+TESTFILES:=$(shell find tests -name "*.v")
 NORMALIZER:=test-normalizer.sed
 
 test: $(TESTFILES:.v=.vo)
-# Make sure everything imports the options.
-	$(HIDE)for FILE in $(VFILES); do \
-	  if ! fgrep -q 'From iris Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi \
-	done
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-COQ_OLD:=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(7|8|9)\b" -q && echo 1)
-COQ_MINOR_VERSION:=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
@@ -30,24 +40,22 @@ tests/.coqdeps.d: $(TESTFILES)
 # Main test script (comments out-of-line because macOS otherwise barfs?!?)
 # - Determine reference file (`REF`).
 # - Print user-visible status line.
+# - unset env vars that change Coq's output
 # - Dump Coq output into a temporary file.
 # - Run `sed -i` on that file in a way that works on macOS.
 # - Either compare the result with the reference file, or move it over the reference file.
 # - Cleanup, and mark as done for make.
 $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
-	$(HIDE)TEST="$$(basename -s .v $<)" && \
-	  if test -f "tests/$$TEST.$(COQ_MINOR_VERSION).ref"; then \
-	    REF="tests/$$TEST.$(COQ_MINOR_VERSION).ref"; \
-	  else \
-	    REF="tests/$$TEST.ref"; \
-	  fi && \
-	  echo "COQTEST$(if $(COQ_OLD), [no ref],$(if $(MAKE_REF), [make ref],)) $<$(if $(COQ_OLD),, (ref: $$REF))" && \
+	$(HIDE)REF=$*".ref" && \
+	  echo "COQTEST$(if $(COQ_REF),$(if $(MAKE_REF), [make ref],), [ref ignored]) $< (ref: $$REF)" && \
 	  TMPFILE="$$(mktemp)" && \
+	  unset OCAMLRUNPARAM && \
 	  $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
-	  sed -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
+	  sed -E -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
 	  mv "$$TMPFILE".new "$$TMPFILE" && \
-	  $(if $(COQ_OLD),true, \
-	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff -u "$$REF" "$$TMPFILE") \
+	  $(if $(COQ_REF),\
+	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
+	    true \
 	  ) && \
 	  rm -f "$$TMPFILE" && \
 	  touch $@

ProofMode.md

-This file has [moved](docs/proof_mode.md).

README.md

-# IRIS COQ DEVELOPMENT [[coqdoc]](https://plv.mpi-sws.org/coqdoc/iris/)
+# Iris Coq Development [[coqdoc]](https://plv.mpi-sws.org/coqdoc/iris/)
 
 This is the Coq development of the [Iris Project](http://iris-project.org),
 which includes [MoSeL](http://iris-project.org/mosel/), a general proof mode
@@ -10,7 +10,7 @@ For using the Coq library, check out the
 For understanding the theory of Iris, a LaTeX version of the core logic
 definitions and some derived forms is available in
 [tex/iris.tex](tex/iris.tex).  A compiled PDF version of this document is
-[available online](http://plv.mpi-sws.org/iris/appendix-3.2.pdf).
+[available online](http://plv.mpi-sws.org/iris/appendix-3.4.pdf).
 
 ## Side-effects
 
@@ -30,13 +30,15 @@ Importing Iris has some side effects as the library sets some global options.
 
 This version is known to compile with:
 
- - Coq 8.10.2 / 8.11.2 / 8.12.0
+ - Coq 8.19.2 / 8.20.1
  - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
 
-If you need to work with Coq 8.7 or Coq 8.8, please check out the
-[iris-3.2 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.2).
-For Coq 8.9, you can use the
-[iris-3.3 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.3).
+Generally we always aim to support the last two stable Coq releases. Support for
+older versions will be dropped when it is convenient.
+
+If you need to work with older versions of Coq, you can check out the
+[tags](https://gitlab.mpi-sws.org/iris/iris/-/tags) for old Iris releases that
+still support them.
 
 ### Working *with* Iris
 
@@ -50,68 +52,96 @@ 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 guarnatee
-backwards-compatibility, so upgrading Iris may break your Iris-using
-developments.
+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.
 
-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
-notification group.
+To fetch updates later, run `opam update && opam upgrade`.
 
-### Working *on* Iris
+#### Be notified of breaking changes
 
-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:
+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.  Note that this excludes the "unstable" and "deprecated"
+packages (see below).
 
-    opam repo add coq-released https://coq.inria.fr/opam/released
-    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+#### Use of Iris in submitted artifacts
 
-Once you got opam set up, run `make build-dep` to install the right versions
-of the dependencies.
+If you are using Iris as part of an artifact submitted for publication with a
+paper, we recommend you make the artifact self-contained so that it can be built
+in the future without relying in any other server to still exist. However, if
+that is for some reason not possible, and if you are using opam to obtain the
+right version of Iris and you used a `dev.*` version, please let us know which
+exact Iris version you artifact relies on so that we can
+[add it to this wiki page](https://gitlab.mpi-sws.org/iris/iris/-/wikis/Pinned-Iris-package-versions)
+and avoid removing it from our opam repository in the future.
 
-Run `make -jN` to build the full development, where `N` is the number of your
-CPU cores.
+### Working *on* Iris
 
-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
 
-* The folder [algebra](theories/algebra) contains the COFE and CMRA
-  constructions as well as the solver for recursive domain equations.
-* The folder [base_logic](theories/base_logic) defines the Iris base logic and
-  the primitive connectives.  It also contains derived constructions that are
-  entirely independent of the choice of resources.
-  * The subfolder [lib](theories/base_logic/lib) contains some generally useful
-    derived constructions.  Most importantly, it defines composeable
-    dynamic resources and ownership of them; the other constructions depend
-    on this setup.
-* The folder [program_logic](theories/program_logic) specializes the base logic
-  to build Iris, the program logic.   This includes weakest preconditions that
-  are defined for any language satisfying some generic axioms, and some derived
-  constructions that work for any such language.
-* The folder [bi](theories/bi) contains the BI++ laws, as well as derived
-  connectives, laws and constructions that are applicable for general BIS.
-* The folder [proofmode](theories/proofmode) contains
-  [MoSeL](http://iris-project.org/mosel/), which extends Coq with contexts for
-  intuitionistic and spatial BI++ assertions. It also contains tactics for
-  interactive proofs. Documentation can be found in
-  [proof_mode.md](docs/proof_mode.md).
-* The folder [heap_lang](theories/heap_lang) defines the ML-like concurrent heap
-  language
-  * The subfolder [lib](theories/heap_lang/lib) contains a few derived
+Iris is structured into multiple *packages*, some of which contain multiple
+modules in separate folders.
+
+* The [iris](iris) package contains the language-independent parts of Iris.
+  + The folder [prelude](iris/prelude) contains modules imported everywhere in
+    Iris.
+  + The folder [algebra](iris/algebra) contains the COFE and CMRA
+    constructions as well as the solver for recursive domain equations.
+    - The subfolder [lib](iris/algebra/lib) contains some general derived RA
+      constructions.
+  + The folder [bi](iris/bi) contains the BI++ laws, as well as derived
+    connectives, laws and constructions that are applicable for general BIs.
+    - The subfolder [lib](iris/bi/lib) contains some general derived logical
+      constructions.
+  + The folder [proofmode](iris/proofmode) contains
+    [MoSeL](http://iris-project.org/mosel/), which extends Coq with contexts for
+    intuitionistic and spatial BI++ assertions. It also contains tactics for
+    interactive proofs. Documentation can be found in
+    [proof_mode.md](docs/proof_mode.md).
+  + The folder [base_logic](iris/base_logic) defines the Iris base logic and
+    the primitive connectives.  It also contains derived constructions that are
+    entirely independent of the choice of resources.
+    - The subfolder [lib](iris/base_logic/lib) contains some generally useful
+      derived constructions.  Most importantly, it defines composable
+      dynamic resources and ownership of them; the other constructions depend
+      on this setup.
+  + The folder [program_logic](iris/program_logic) specializes the base logic
+    to build Iris, the program logic.   This includes weakest preconditions that
+    are defined for any language satisfying some generic axioms, and some derived
+    constructions that work for any such language.
+  + The folder [si_logic](iris/si_logic) defines a "plain" step-indexed logic
+    and shows that it is an instance of the BI interface.
+* The [iris_heap_lang](iris_heap_lang) package defines the ML-like concurrent
+  language HeapLang and provides tactic support and proof mode integration.
+  + The subfolder [lib](iris_heap_lang/lib) contains a few derived
     constructions within this language, e.g., parallel composition.
     For more examples of using Iris and heap_lang, have a look at the
     [Iris Examples](https://gitlab.mpi-sws.org/iris/examples).
-* The folder [tests](theories/tests) contains modules we use to test our
-  infrastructure. Users of the Iris Coq library should *not* depend on these
-  modules; they may change or disappear without any notice.
-* The folder [si_logic](theories/si_logic) defines a "plain" step-indexed logic
-  and shows that it is an instance of the BI interface.
+* The [iris_unstable](iris_unstable) package contains libraries that are not yet
+  ready for inclusion in Iris proper. For each library, there is a corresponding
+  "tracking issue" in the Iris issue tracker (also linked from the library
+  itself) which tracks the work that still needs to be done before moving the
+  library to Iris. No stability guarantees whatsoever are made for this package.
+* The [iris_deprecated](iris_deprecated) package contains libraries that have been
+  removed from Iris proper, but are kept around to give users some more time to
+  switch to their intended replacements. The individual libraries come with comments
+  explaining the deprecation and making recommendations for what to use
+  instead. No stability guarantees whatsoever are made for this package.
+* The folder [tests](tests) contains modules we use to test our
+  infrastructure. These modules are not installed by `make install`, and should
+  not be imported.
+
+Note that the unstable and deprecated packages are not released, so they only
+exist in the development version of Iris.
 
 ## Case Studies
 
@@ -135,8 +165,12 @@ that should be compatible with this version:
 
 Getting along with Iris in Coq:
 
+* The coding style is documented in the [style guide](docs/style_guide.md).
 * Iris proof patterns and conventions are documented in the
   [proof guide](docs/proof_guide.md).
+* Various notions of equality and logical entailment in Iris and their Coq
+  interface are described in the
+  [equality docs](docs/equalities_and_entailments.md).
 * The Iris tactics are described in the
   [the Iris Proof Mode (IPM) / MoSeL documentation](docs/proof_mode.md) as well as the
   [HeapLang documentation](docs/heap_lang.md).
@@ -144,16 +178,13 @@ Getting along with Iris in Coq:
 
 Contacting the developers:
 
-* Discussion about the Iris Coq development happens on the mailing list
-  [iris-club@lists.mpi-sws.org](https://lists.mpi-sws.org/listinfo/iris-club)
-  and in the [Iris Chat](https://mattermost.mpi-sws.org/iris).  This is also the
-  right place to ask questions.  The chat requires an account at the
-  [MPI-SWS GitLab](https://gitlab.mpi-sws.org/users/sign_in) (use the "Register"
-  tab). If you have trouble joining the chat, please contact
-  [Ralf](https://gitlab.mpi-sws.org/jung).
+* Discussion about the Iris Coq development happens in the [Iris
+  Chat](https://iris-project.org/chat.html). This is also the right place to ask
+  questions.
 * If you want to report a bug, please use the
-  [issue tracker](https://gitlab.mpi-sws.org/iris/iris/issues), which also
-  requires an MPI-SWS GitLab account.
+  [issue tracker](https://gitlab.mpi-sws.org/iris/iris/issues), which requires
+  an MPI-SWS GitLab account. The [chat page](https://iris-project.org/chat.html)
+  describes how to create such an account.
 * To contribute to Iris itself, see the [contribution guide](CONTRIBUTING.md).
 
 Miscellaneous:

_CoqProject

--Q theories iris
+# Search paths for all packages. They must all match the regex
+# `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
+-Q iris/prelude iris.prelude
+-Q iris/algebra iris.algebra
+-Q iris/si_logic iris.si_logic
+-Q iris/bi iris.bi
+-Q iris/proofmode iris.proofmode
+-Q iris/base_logic iris.base_logic
+-Q iris/program_logic iris.program_logic
+-Q iris_heap_lang iris.heap_lang
+-Q iris_unstable iris.unstable
+-Q iris_deprecated iris.deprecated
+
+# Custom flags (to be kept in sync with the dune file at the root of the repo).
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
+# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-arg -w -arg -notation-incompatible-prefix
+# We can't do this migration yet until we require Coq 9.0
+-arg -w -arg -deprecated-from-Coq
+-arg -w -arg -deprecated-dirpath-Coq
+
+iris/prelude/options.v
+iris/prelude/prelude.v
+iris/algebra/stepindex.v
+iris/algebra/stepindex_finite.v
+iris/algebra/monoid.v
+iris/algebra/cmra.v
+iris/algebra/big_op.v
+iris/algebra/cmra_big_op.v
+iris/algebra/sts.v
+iris/algebra/numbers.v
+iris/algebra/view.v
+iris/algebra/auth.v
+iris/algebra/gmap.v
+iris/algebra/ofe.v
+iris/algebra/cofe_solver.v
+iris/algebra/agree.v
+iris/algebra/excl.v
+iris/algebra/functions.v
+iris/algebra/frac.v
+iris/algebra/dfrac.v
+iris/algebra/csum.v
+iris/algebra/list.v
+iris/algebra/vector.v
+iris/algebra/updates.v
+iris/algebra/local_updates.v
+iris/algebra/gset.v
+iris/algebra/gmultiset.v
+iris/algebra/coPset.v
+iris/algebra/proofmode_classes.v
+iris/algebra/ufrac.v
+iris/algebra/reservation_map.v
+iris/algebra/dyn_reservation_map.v
+iris/algebra/max_prefix_list.v
+iris/algebra/mra.v
+iris/algebra/lib/excl_auth.v
+iris/algebra/lib/frac_auth.v
+iris/algebra/lib/ufrac_auth.v
+iris/algebra/lib/dfrac_agree.v
+iris/algebra/lib/gmap_view.v
+iris/algebra/lib/mono_nat.v
+iris/algebra/lib/mono_Z.v
+iris/algebra/lib/mono_list.v
+iris/algebra/lib/gset_bij.v
+iris/si_logic/siprop.v
+iris/si_logic/bi.v
+iris/bi/notation.v
+iris/bi/interface.v
+iris/bi/derived_connectives.v
+iris/bi/extensions.v
+iris/bi/derived_laws.v
+iris/bi/derived_laws_later.v
+iris/bi/plainly.v
+iris/bi/internal_eq.v
+iris/bi/big_op.v
+iris/bi/updates.v
+iris/bi/ascii.v
+iris/bi/bi.v
+iris/bi/monpred.v
+iris/bi/embedding.v
+iris/bi/weakestpre.v
+iris/bi/telescopes.v
+iris/bi/lib/cmra.v
+iris/bi/lib/counterexamples.v
+iris/bi/lib/fixpoint_mono.v
+iris/bi/lib/fixpoint_banach.v
+iris/bi/lib/fractional.v
+iris/bi/lib/laterable.v
+iris/bi/lib/atomic.v
+iris/bi/lib/core.v
+iris/bi/lib/relations.v
+iris/base_logic/upred.v
+iris/base_logic/bi.v
+iris/base_logic/derived.v
+iris/base_logic/proofmode.v
+iris/base_logic/base_logic.v
+iris/base_logic/algebra.v
+iris/base_logic/bupd_alt.v
+iris/base_logic/lib/iprop.v
+iris/base_logic/lib/own.v
+iris/base_logic/lib/saved_prop.v
+iris/base_logic/lib/wsat.v
+iris/base_logic/lib/invariants.v
+iris/base_logic/lib/fancy_updates.v
+iris/base_logic/lib/boxes.v
+iris/base_logic/lib/na_invariants.v
+iris/base_logic/lib/cancelable_invariants.v
+iris/base_logic/lib/gen_heap.v
+iris/base_logic/lib/gen_inv_heap.v
+iris/base_logic/lib/fancy_updates_from_vs.v
+iris/base_logic/lib/proph_map.v
+iris/base_logic/lib/ghost_var.v
+iris/base_logic/lib/mono_nat.v
+iris/base_logic/lib/gset_bij.v
+iris/base_logic/lib/ghost_map.v
+iris/base_logic/lib/later_credits.v
+iris/base_logic/lib/token.v
+iris/program_logic/adequacy.v
+iris/program_logic/lifting.v
+iris/program_logic/weakestpre.v
+iris/program_logic/total_weakestpre.v
+iris/program_logic/total_adequacy.v
+iris/program_logic/language.v
+iris/program_logic/ectx_language.v
+iris/program_logic/ectxi_language.v
+iris/program_logic/ectx_lifting.v
+iris/program_logic/ownp.v
+iris/program_logic/total_lifting.v
+iris/program_logic/total_ectx_lifting.v
+iris/program_logic/atomic.v
+iris/proofmode/base.v
+iris/proofmode/ident_name.v
+iris/proofmode/string_ident.v
+iris/proofmode/tokens.v
+iris/proofmode/coq_tactics.v
+iris/proofmode/ltac_tactics.v
+iris/proofmode/environments.v
+iris/proofmode/reduction.v
+iris/proofmode/intro_patterns.v
+iris/proofmode/spec_patterns.v
+iris/proofmode/sel_patterns.v
+iris/proofmode/tactics.v
+iris/proofmode/notation.v
+iris/proofmode/classes.v
+iris/proofmode/classes_make.v
+iris/proofmode/class_instances.v
+iris/proofmode/class_instances_later.v
+iris/proofmode/class_instances_updates.v
+iris/proofmode/class_instances_embedding.v
+iris/proofmode/class_instances_plainly.v
+iris/proofmode/class_instances_internal_eq.v
+iris/proofmode/class_instances_frame.v
+iris/proofmode/class_instances_make.v
+iris/proofmode/monpred.v
+iris/proofmode/modalities.v
+iris/proofmode/modality_instances.v
+iris/proofmode/proofmode.v
+
+iris_heap_lang/locations.v
+iris_heap_lang/lang.v
+iris_heap_lang/class_instances.v
+iris_heap_lang/pretty.v
+iris_heap_lang/metatheory.v
+iris_heap_lang/tactics.v
+iris_heap_lang/primitive_laws.v
+iris_heap_lang/derived_laws.v
+iris_heap_lang/notation.v
+iris_heap_lang/proofmode.v
+iris_heap_lang/adequacy.v
+iris_heap_lang/total_adequacy.v
+iris_heap_lang/proph_erasure.v
+iris_heap_lang/lib/spawn.v
+iris_heap_lang/lib/par.v
+iris_heap_lang/lib/assert.v
+iris_heap_lang/lib/lock.v
+iris_heap_lang/lib/rw_lock.v
+iris_heap_lang/lib/spin_lock.v
+iris_heap_lang/lib/ticket_lock.v
+iris_heap_lang/lib/rw_spin_lock.v
+iris_heap_lang/lib/nondet_bool.v
+iris_heap_lang/lib/lazy_coin.v
+iris_heap_lang/lib/clairvoyant_coin.v
+iris_heap_lang/lib/counter.v
+iris_heap_lang/lib/atomic_heap.v
+iris_heap_lang/lib/increment.v
+iris_heap_lang/lib/diverge.v
+iris_heap_lang/lib/arith.v
+iris_heap_lang/lib/array.v
+iris_heap_lang/lib/logatom_lock.v
+
+iris_unstable/algebra/list.v
+iris_unstable/base_logic/algebra.v
+iris_unstable/base_logic/mono_list.v
+iris_unstable/heap_lang/interpreter.v
 
-theories/options.v
-theories/algebra/monoid.v
-theories/algebra/cmra.v
-theories/algebra/big_op.v
-theories/algebra/cmra_big_op.v
-theories/algebra/sts.v
-theories/algebra/numbers.v
-theories/algebra/auth.v
-theories/algebra/gmap.v
-theories/algebra/ofe.v
-theories/algebra/base.v
-theories/algebra/dra.v
-theories/algebra/cofe_solver.v
-theories/algebra/agree.v
-theories/algebra/excl.v
-theories/algebra/functions.v
-theories/algebra/frac.v
-theories/algebra/csum.v
-theories/algebra/list.v
-theories/algebra/vector.v
-theories/algebra/updates.v
-theories/algebra/local_updates.v
-theories/algebra/gset.v
-theories/algebra/gmultiset.v
-theories/algebra/coPset.v
-theories/algebra/proofmode_classes.v
-theories/algebra/ufrac.v
-theories/algebra/namespace_map.v
-theories/algebra/lib/excl_auth.v
-theories/algebra/lib/frac_auth.v
-theories/algebra/lib/ufrac_auth.v
-theories/algebra/lib/frac_agree.v
-theories/si_logic/siprop.v
-theories/si_logic/bi.v
-theories/bi/notation.v
-theories/bi/interface.v
-theories/bi/derived_connectives.v
-theories/bi/derived_laws.v
-theories/bi/derived_laws_later.v
-theories/bi/plainly.v
-theories/bi/internal_eq.v
-theories/bi/big_op.v
-theories/bi/updates.v
-theories/bi/ascii.v
-theories/bi/bi.v
-theories/bi/tactics.v
-theories/bi/monpred.v
-theories/bi/embedding.v
-theories/bi/weakestpre.v
-theories/bi/telescopes.v
-theories/bi/lib/counterexamples.v
-theories/bi/lib/fixpoint.v
-theories/bi/lib/fractional.v
-theories/bi/lib/laterable.v
-theories/bi/lib/atomic.v
-theories/bi/lib/core.v
-theories/bi/lib/relations.v
-theories/base_logic/upred.v
-theories/base_logic/bi.v
-theories/base_logic/derived.v
-theories/base_logic/proofmode.v
-theories/base_logic/base_logic.v
-theories/base_logic/bupd_alt.v
-theories/base_logic/lib/iprop.v
-theories/base_logic/lib/own.v
-theories/base_logic/lib/saved_prop.v
-theories/base_logic/lib/wsat.v
-theories/base_logic/lib/invariants.v
-theories/base_logic/lib/fancy_updates.v
-theories/base_logic/lib/viewshifts.v
-theories/base_logic/lib/auth.v
-theories/base_logic/lib/sts.v
-theories/base_logic/lib/boxes.v
-theories/base_logic/lib/na_invariants.v
-theories/base_logic/lib/cancelable_invariants.v
-theories/base_logic/lib/gen_heap.v
-theories/base_logic/lib/gen_inv_heap.v
-theories/base_logic/lib/fancy_updates_from_vs.v
-theories/base_logic/lib/proph_map.v
-theories/base_logic/lib/ghost_var.v
-theories/program_logic/adequacy.v
-theories/program_logic/lifting.v
-theories/program_logic/weakestpre.v
-theories/program_logic/total_weakestpre.v
-theories/program_logic/total_adequacy.v
-theories/program_logic/hoare.v
-theories/program_logic/language.v
-theories/program_logic/ectx_language.v
-theories/program_logic/ectxi_language.v
-theories/program_logic/ectx_lifting.v
-theories/program_logic/ownp.v
-theories/program_logic/total_lifting.v
-theories/program_logic/total_ectx_lifting.v
-theories/program_logic/atomic.v
-theories/heap_lang/locations.v
-theories/heap_lang/lang.v
-theories/heap_lang/metatheory.v
-theories/heap_lang/tactics.v
-theories/heap_lang/primitive_laws.v
-theories/heap_lang/derived_laws.v
-theories/heap_lang/notation.v
-theories/heap_lang/proofmode.v
-theories/heap_lang/adequacy.v
-theories/heap_lang/total_adequacy.v
-theories/heap_lang/proph_erasure.v
-theories/heap_lang/lib/spawn.v
-theories/heap_lang/lib/par.v
-theories/heap_lang/lib/assert.v
-theories/heap_lang/lib/lock.v
-theories/heap_lang/lib/spin_lock.v
-theories/heap_lang/lib/ticket_lock.v
-theories/heap_lang/lib/nondet_bool.v
-theories/heap_lang/lib/lazy_coin.v
-theories/heap_lang/lib/clairvoyant_coin.v
-theories/heap_lang/lib/counter.v
-theories/heap_lang/lib/atomic_heap.v
-theories/heap_lang/lib/increment.v
-theories/heap_lang/lib/diverge.v
-theories/heap_lang/lib/arith.v
-theories/heap_lang/lib/array.v
-theories/proofmode/base.v
-theories/proofmode/ident_name.v
-theories/proofmode/tokens.v
-theories/proofmode/coq_tactics.v
-theories/proofmode/ltac_tactics.v
-theories/proofmode/environments.v
-theories/proofmode/reduction.v
-theories/proofmode/intro_patterns.v
-theories/proofmode/spec_patterns.v
-theories/proofmode/sel_patterns.v
-theories/proofmode/tactics.v
-theories/proofmode/notation.v
-theories/proofmode/classes.v
-theories/proofmode/class_instances.v
-theories/proofmode/class_instances_later.v
-theories/proofmode/class_instances_updates.v
-theories/proofmode/class_instances_embedding.v
-theories/proofmode/class_instances_plainly.v
-theories/proofmode/class_instances_internal_eq.v
-theories/proofmode/frame_instances.v
-theories/proofmode/monpred.v
-theories/proofmode/modalities.v
-theories/proofmode/modality_instances.v
+iris_deprecated/base_logic/auth.v
+iris_deprecated/base_logic/sts.v
+iris_deprecated/base_logic/viewshifts.v
+iris_deprecated/program_logic/hoare.v

benchmark/.gitignore

-__pycache__
-build-times*
-gitlab-extract

benchmark/export.py

-#!/usr/bin/env python3
-import argparse, sys, pprint, itertools, subprocess
-import requests
-import parse_log
-
-# read command-line arguments
-parser = argparse.ArgumentParser(description='Export iris-coq build times to grafana')
-parser.add_argument("-f", "--file",
-                    dest="file", required=True,
-                    help="Filename to get the data from.")
-parser.add_argument("-c", "--commits",
-                    dest="commits",
-                    help="Restrict the graph to the given commits.")
-parser.add_argument("-p", "--project",
-                    dest="project", required=True,
-                    help="Project name sent to the server.")
-parser.add_argument("-b", "--branch",
-                    dest="branch", required=True,
-                    help="Branch name sent to the server.")
-parser.add_argument("--config",
-                    dest="config", required=True,
-                    help="The config string.")
-parser.add_argument("-s", "--server",
-                    dest="server", required=True,
-                    help="The server (URL) to send the data to.")
-parser.add_argument("-u", "--user",
-                    dest="user", required=True,
-                    help="Username for HTTP auth.")
-parser.add_argument("--password",
-                    dest="password", required=True,
-                    help="Password for HTTP auth.")
-args = parser.parse_args()
-pp = pprint.PrettyPrinter()
-log_file = sys.stdin if args.file == "-" else open(args.file, "r")
-
-results = parse_log.parse(log_file, parse_times = parse_log.PARSE_RAW)
-if args.commits:
-    commits = set(parse_log.parse_git_commits(args.commits))
-    results = filter(lambda r: r.commit in commits, results)
-results = list(results)
-
-for datapoint in results:
-    times = '\n'.join(datapoint.times)
-    commit = datapoint.commit
-    print("Sending {}...".format(commit), end='')
-    date = subprocess.check_output(['git', 'show', commit, '-s', '--pretty=%cI']).strip().decode('UTF-8')
-    headers = {'X-Project': args.project, 'X-Branch': args.branch, 'X-Commit': commit, 'X-Config': args.config, 'X-Date': date}
-    r = requests.post(args.server+"/build_times", data=times, headers=headers, auth=(args.user, args.password))
-    print(" {}".format(r.text.strip()))
-    r.raise_for_status()

benchmark/gitlab-extract.py

-#!/usr/bin/env python3
-import argparse, pprint, sys, glob, zipfile, subprocess
-import requests
-import parse_log
-
-def last(it):
-    r = None
-    for i in it:
-        r = i
-    return r
-
-def first(it):
-    for i in it:
-        return i
-    return None
-
-def req(path):
-    url = '%s/api/v3/%s' % (args.server, path)
-    r = requests.get(url, headers={'PRIVATE-TOKEN': args.private_token})
-    r.raise_for_status()
-    return r
-
-# read command-line arguments
-parser = argparse.ArgumentParser(description='Extract iris-coq build logs from GitLab')
-parser.add_argument("-t", "--private-token",
-                    dest="private_token", required=True,
-                    help="The private token used to authenticate access.")
-parser.add_argument("-s", "--server",
-                    dest="server", default="https://gitlab.mpi-sws.org/",
-                    help="The GitLab server to contact.")
-parser.add_argument("-p", "--project",
-                    dest="project", default="FP/iris-coq",
-                    help="The name of the project on GitLab.")
-parser.add_argument("-f", "--file",
-                    dest="file", required=True,
-                    help="Filename to store the load in.")
-parser.add_argument("-c", "--commits",
-                    dest="commits",
-                    help="The commits to fetch. Default is everything since the most recent entry in the log file.")
-parser.add_argument("-a", "--artifacts",
-                    dest="artifacts",
-                    help="Location of the artifacts (following GitLab's folder structure).  If not given (which should be the common case), the artifacts will be downloaded from GitLab.")
-parser.add_argument("-b", "--blacklist-branch",
-                    dest="blacklist_branch",
-                    help="Skip the commit if it is contained in the given branch.")
-args = parser.parse_args()
-log_file = sys.stdout if args.file == "-" else open(args.file, "a")
-
-# determine commit, if missing
-if args.commits is None:
-    if args.file == "-":
-        raise Exception("If you do not give explicit commits, you have to give a logfile so that we can determine the missing commits.")
-    last_result = last(parse_log.parse(open(args.file, "r"), parse_times = parse_log.PARSE_NOT))
-    args.commits = "{}..origin/master".format(last_result.commit)
-
-projects = req("projects?per_page=512")
-project = first(filter(lambda p: p['path_with_namespace'] == args.project, projects.json()))
-if project is None:
-    sys.stderr.write("Project not found.\n")
-    sys.exit(1)
-
-BREAK = False
-for commit in parse_log.parse_git_commits(args.commits):
-    if BREAK:
-        break
-    # test to skip the commit
-    if args.blacklist_branch is not None:
-        branches = subprocess.check_output(["git", "branch", "-r", "--contains", commit]).decode("utf-8")
-        if args.blacklist_branch in map(lambda x: x.strip(), branches.split('\n')):
-            continue
-    # Find out more about the commit
-    print("Fetching {}...".format(commit), end='')
-    commit_data = req("/projects/{}/repository/commits/{}".format(project['id'], commit))
-    if commit_data.status_code != 200:
-        raise Exception("Commit not found?")
-    builds = req("/projects/{}/repository/commits/{}/builds".format(project['id'], commit))
-    if builds.status_code != 200:
-        raise Exception("Build not found?")
-    # iterate over builds by decreasing ID, and look for the artifact
-    found_build = False
-    for build in builds.json():
-        if build['status'] in ('created', 'pending', 'running'):
-            # build still not yet done, don't fetch this or any later commit
-            BREAK = True
-            print(" build still in progress, aborting")
-            break
-        if build['status'] != 'success':
-            # build failed or cancelled, skip to next
-            continue
-        # now fetch the build times
-        if args.artifacts:
-            artifact_zip = glob.glob('{}/*/{}/{}/artifacts.zip'.format(args.artifacts, project['id'], build['id']))
-            if not artifact_zip:
-                # no artifact at this build, try another one
-                continue
-            assert len(artifact_zip) == 1, "Found too many artifacts"
-            artifact_zip = artifact_zip[0]
-            with zipfile.ZipFile(artifact_zip) as artifact:
-                with artifact.open('build-time.txt') as build_times:
-                    # Output into log file
-                    log_file.write("# {}\n".format(commit))
-                    log_file.write(build_times.read().decode('UTF-8'))
-                    log_file.flush()
-        else:
-            build_times = requests.get("{}/builds/{}/artifacts/raw/build-time.txt".format(project['web_url'], build['id']))
-            if build_times.status_code != 200:
-                # no artifact at this build, try another one
-                continue
-            # Output in the log file format
-            log_file.write("# {}\n".format(commit))
-            log_file.write(build_times.text)
-            log_file.flush()
-            # don't fetch another build
-            found_build = True
-            print(" success")
-            break
-    if not found_build and not BREAK:
-        print(" found no succeessful build")

benchmark/parse_log.py

-import re, subprocess
-
-class Result:
-    def __init__(self, commit, times):
-        self.commit = commit
-        self.times = times
-
-PARSE_NOT  = 0
-PARSE_RAW  = 1
-PARSE_FULL = 2
-
-def parse(file, parse_times = PARSE_FULL):
-    '''[file] should be a file-like object, an iterator over the lines.
-       yields a list of Result objects.'''
-    commit_re = re.compile("^# ([a-z0-9]+)$")
-    time_re = re.compile("^([a-zA-Z0-9_/-]+) \((real|user): ([0-9.]+).* mem: ([0-9]+) ko\)$")
-    commit = None
-    times = None
-    for line in file:
-        line = line.strip()
-        # next commit?
-        m = commit_re.match(line)
-        if m is not None:
-            # previous commit, if any, is done now
-            if commit is not None:
-                yield Result(commit, times)
-            # start recording next commit
-            commit = m.group(1)
-            if parse_times != PARSE_NOT:
-                times = [] if parse_times == PARSE_RAW else {} # reset the recorded times
-            continue
-        # next file time?
-        m = time_re.match(line)
-        if m is not None:
-            if times is not None:
-                if parse_times == PARSE_RAW:
-                    times.append(line)
-                else:
-                    name = m.group(1)
-                    time = float(m.group(2))
-                    times[name] = time
-            continue
-        # nothing else we know about, ignore
-        print("Ignoring line",line,"(in commit {})".format(commit))
-    # end of file. previous commit, if any, is done now.
-    if commit is not None:
-        yield Result(commit, times)
-
-def parse_git_commits(commits):
-    '''Returns an iterable of SHA1s'''
-    if commits.find('..') >= 0:
-        # a range of commits
-        commits = subprocess.check_output(["git", "rev-list", commits])
-    else:
-        # a single commit
-        commits = subprocess.check_output(["git", "rev-parse", commits])
-    output = commits.decode("utf-8").strip()
-    if not output: # empty output
-        return []
-    return reversed(output.split('\n'))

benchmark/visualize.py

-#!/usr/bin/env python3
-import argparse, sys, pprint, itertools
-import matplotlib.pyplot as plt
-import parse_log
-
-markers = itertools.cycle([(3, 0), (3, 0, 180), (4, 0), (4, 0, 45), (8, 0)])
-
-# read command-line arguments
-parser = argparse.ArgumentParser(description='Visualize iris-coq build times')
-parser.add_argument("-f", "--file",
-                    dest="file", required=True,
-                    help="Filename to get the data from.")
-parser.add_argument("-t", "--timings", nargs='+',
-                    dest="timings",
-                    help="The names of the Coq files (with or without the extension) whose timings should be extracted")
-parser.add_argument("-c", "--commits",
-                    dest="commits",
-                    help="Restrict the graph to the given commits.")
-args = parser.parse_args()
-pp = pprint.PrettyPrinter()
-log_file = sys.stdin if args.file == "-" else open(args.file, "r")
-
-results = parse_log.parse(log_file, parse_times = parse_log.PARSE_FULL)
-if args.commits:
-    commits = set(parse_log.parse_git_commits(args.commits))
-    results = filter(lambda r: r.commit in commits, results)
-results = list(results)
-
-timings = list(map(lambda t: t[:-2] if t.endswith(".v") else t, args.timings))
-for timing in timings:
-    plt.plot(list(map(lambda r: r.times.get(timing), results)), marker=next(markers), markersize=8)
-plt.legend(timings, loc = 'upper left', bbox_to_anchor=(1.05, 1.0))
-plt.xticks(range(len(results)), list(map(lambda r: r.commit[:7], results)), rotation=70)
-plt.subplots_adjust(bottom=0.2, right=0.7) # more space for the commit labels and legend
-
-plt.xlabel('Commit')
-plt.ylabel('Time (s)')
-plt.title('Time to compile files')
-plt.grid(True)
-plt.show()

build-all

-#!/usr/bin/python3
-import sys, os
-import requests
-
-# A script to build Iris' reverse-dependencies (the one that usually get built every night against Iris master)
-# against a branch of your choice.
-# Set the GITLAB_TOKEN environment variable to a GitLab access token.
-# Set at least one of IRIS_REV or STDPP_REV to control which branches of these projects to build against
-# (default to `master`).
-
-if not "GITLAB_TOKEN" in os.environ:
-    print("You need to set the GITLAB_TOKEN environment variable to a GitLab access token.")
-    print("You can create such tokens at <https://gitlab.mpi-sws.org/profile/personal_access_tokens>.")
-    print("Make sure you grant access to the 'api' scope.")
-    sys.exit(1)
-if not "IRIS_REV" in os.environ:
-    print("Please set IRIS_REV, STDPP_REV, ORC11_REV and GPFSL_REV environment variables to the branch/tag/commit of the respective project that you want to use.")
-    print("Only IRIS_REV is mandatory, the rest defaults to 'master'.")
-    sys.exit(1)
-
-GITLAB_TOKEN = os.environ["GITLAB_TOKEN"]
-PROJECTS = [
-    { 'name': 'lambda-rust', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
-    { 'name': 'lambda-rust', 'branch': 'masters/weak_mem', 'vars': ['STDPP_REV', 'IRIS_REV', 'ORC11_REV', 'GPFSL_REV'] }, # covers GPFSL and ORC11
-    { 'name': 'examples', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
-    { 'name': 'iron', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
-    { 'name': 'reloc', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
-    { 'name': 'c', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
-    { 'name': 'spygame', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
-    { 'name': 'time-credits', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
-    { 'name': 'actris', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
-    { 'name': 'ora', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
-    { 'name': 'tutorial-popl18', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
-]
-
-for project in PROJECTS:
-    print("Triggering build for {}{}...".format(project['name'], '' if project['branch'] == 'master' else ':'+project['branch']))
-    id = str(project['id']) if 'id' in project else "iris%2F{}".format(project['name'])
-    url = "https://gitlab.mpi-sws.org/api/v4/projects/{}/pipeline".format(id)
-    json = {
-        'ref': project['branch'],
-        'variables': list(map(lambda var: { 'key': var, 'value': os.environ.get(var, "master") }, project['vars'])),
-    }
-    r = requests.post(url, headers={'PRIVATE-TOKEN': GITLAB_TOKEN}, json=json)
-    r.raise_for_status()
-    print("    Pipeline running at {}".format(r.json()['web_url']))

opam → coq-iris-deprecated.opam

 opam-version: "2.0"
-name: "coq-iris"
 maintainer: "Ralf Jung <jung@mpi-sws.org>"
 authors: "The Iris Team"
 license: "BSD-3-Clause"
 homepage: "https://iris-project.org/"
 bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+version: "dev"
 
-synopsis: "Iris is a Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
+synopsis: "Deprecated Iris libraries"
+description: """
+This package contains libraries that have been deprecated from Iris, and are planned to be
+entirely removed at some point.
+"""
 
 depends: [
-  "coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2020-09-15.0.f4a2763b") | (= "dev") }
+  "coq-iris" {= version}
 ]
 
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+build: ["./make-package" "iris_deprecated" "-j%{jobs}%"]
+install: ["./make-package" "iris_deprecated" "install"]

coq-iris-heap-lang.opam

+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+version: "dev"
+
+synopsis: "The canonical example language for Iris"
+description: """
+This package defines HeapLang, a concurrent lambda calculus with references, and
+uses Iris to build a program logic for HeapLang programs.
+"""
+tags: [
+  "logpath:iris.heap_lang"
+]
+
+depends: [
+  "coq-iris" {= version}
+]
+
+build: ["./make-package" "iris_heap_lang" "-j%{jobs}%"]
+install: ["./make-package" "iris_heap_lang" "install"]

coq-iris-unstable.opam

+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+version: "dev"
+
+synopsis: "Unfinished Iris libraries"
+description: """
+This package contains libraries that have been proposed for inclusion in Iris, but more
+work is needed before they are ready for this.
+"""
+
+depends: [
+  "coq-iris" {= version}
+  "coq-iris-heap-lang" {= version}
+]
+
+build: ["./make-package" "iris_unstable" "-j%{jobs}%"]
+install: ["./make-package" "iris_unstable" "install"]