.gitattributes

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

.gitignore

 *.vo
+*.vos
+*.vok
 *.vio
 *.v.d
 .coqdeps.d
@@ -11,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:
@@ -16,10 +36,7 @@ variables:
   cache:
     key: "$CI_JOB_NAME"
     paths:
-    - opamroot/
-  only:
-  - master
-  - /^ci/
+    - _opam/
   except:
   - triggers
   - schedules
@@ -27,42 +44,52 @@ variables:
 
 ## Build jobs
 
-build-coq.dev:
+# The newest version runs with timing.
+build-coq.8.20.1:
   <<: *template
   variables:
-    OCAML: "ocaml-base-compiler.4.07.0"
-    OPAM_PINS: "coq version dev"
-    CI_COQCHK: "1"
-
-build-coq.8.10.1:
-  <<: *template
-  variables:
-    OCAML: "ocaml-base-compiler.4.07.0"
-    OPAM_PINS: "coq version 8.10.1"
+    OPAM_PINS: "coq version 8.20.1"
+    DENY_WARNINGS: "1"
+    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.10.0:
+# The newest version also runs in MRs, without timing.
+build-coq.8.20.1-mr:
   <<: *template
+  <<: *only_mr
   variables:
-    OCAML: "ocaml-base-compiler.4.07.0"
-    OPAM_PINS: "coq version 8.10.0"
+    OPAM_PINS: "coq version 8.20.1"
+    DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
 
-build-coq.8.9.1:
+# Also ensure Dune works.
+build-coq.8.20.1-dune:
   <<: *template
+  <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.9.1"
+    OPAM_PINS: "coq version 8.20.1   dune version 3.15.2"
+    MAKE_TARGET: "dune"
 
-build-coq.8.9.0:
+# The oldest version runs in MRs, without name mangling.
+build-coq.8.19.2:
   <<: *template
+  <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.9.0"
-    OPAM_PKG: "coq-iris"
-    DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
-    DOC_OPTS: "--external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp"
-    TIMING_CONF: "coq-8.9.0"
-  tags:
-  - fp-timing
+    OPAM_PINS: "coq version 8.19.2"
 
-build-coq.8.8.2:
+trigger-stdpp.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.8.2"
+    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:
+  - triggers
+  - schedules
+  - api

.gitmodules

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

CONTRIBUTING.md

 # Contributing to the Iris Coq Development
 
 Here you can find some how-tos for various thing sthat might come up when doing
-Iris development.
+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.
 * Wait for CI to publish a new std++ version on the opam archive, then run
   `opam update iris-dev`.
 * In Iris, change the `opam` file to depend on the new version.
-* Run `make build-dep` (in Iris) to install the new version of std++.
+  (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 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.
 
@@ -42,51 +71,62 @@ Some test cases have per-Coq-version `.ref` files (e.g., `atomic.8.8.ref` is a
 Coq-8.8-specific `.ref` file).  If you change one of these, remember to update
 *all* the `.ref` files.
 
-## How to measure the timing effect on a reverse dependency
+If you want to compile without tests run `make NO_TEST=1`.
 
-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

LICENSE

-The source code (i.e., everything except for files in the docs/ folder) in this
-development is licensed under the terms of the BSD license, while the
-documentation (i.e., everything inside the docs/ folder) is licensed under the
-terms of the CC-BY 4.0 license.  Fur further details, see LICENSE-CODE and
-LICENSE-DOCS, respectively.
+The source code (i.e., everything except for files in the docs/ and tex/
+folders) in this development is licensed under the terms of the BSD license,
+while the documentation (i.e., everything inside the docs/ and tex/ folders) is
+licensed under the terms of the CC-BY 4.0 license.  Fur further details, see
+LICENSE-CODE and LICENSE-DOCS, respectively.

LICENSE-CODE

-All files in this development, excluding those in docs/, are distributed
-under the terms of the BSD license, included below.
+All files in this development, excluding those in docs/ and tex/, are
+distributed under the terms of the 3-clause BSD license
+(https://opensource.org/licenses/BSD-3-Clause), included below.
 
-------------------------------------------------------------------------------
+Copyright: Iris developers and contributors
 
-                            BSD LICENCE
+------------------------------------------------------------------------------
 
 Redistribution and use in source and binary forms, with or without
 modification, are permitted provided that the following conditions are met:
@@ -12,17 +13,17 @@ modification, are permitted provided that the following conditions are met:
     * Redistributions in binary form must reproduce the above copyright
       notice, this list of conditions and the following disclaimer in the
       documentation and/or other materials provided with the distribution.
-    * Neither the name of the <organization> nor the
-      names of its contributors may be used to endorse or promote products
-      derived from this software without specific prior written permission.
+    * Neither the name of the copyright holder nor the names of its contributors
+      may be used to endorse or promote products derived from this software
+      without specific prior written permission.
 
 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
 ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY
-DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
-LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
-ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

LICENSE-DOCS

-All files in the docs/ folder of this development are distributed
+All files in the docs/ and tex/ folders of this development are distributed
 under the terms of the CC-BY 4.0 license <https://creativecommons.org/licenses/by/4.0/>.
 
 For your convenience, a plain-text version of the license is included below.

Makefile

-# Forward most targets to Coq makefile (with some trick to make this phony)
-%: Makefile.coq phony
-	+@make -f Makefile.coq $@
-
+# Default target
 all: Makefile.coq
-	+@make -f Makefile.coq all
+	+@$(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
+	@#echo "Forwarding $@"
+	+@$(MAKE) -f Makefile.coq $@
+phony: ;
+.PHONY: phony
+
 clean: Makefile.coq
-	+@make -f Makefile.coq clean
-	find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
-	rm -f Makefile.coq
+	+@$(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.
 Makefile.coq: _CoqProject Makefile
-	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
+	"$(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 "# Pinning build-dep package." && \
-	  if opam --version | grep "^1\." -q; then \
-	    BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
-	    opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
-	    opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
-	  else \
-	    opam install $(OPAMFLAGS) build-dep/; \
-	  fi
-
-# Some files that do *not* need to be forwarded to Makefile.coq
-Makefile: ;
-_CoqProject: ;
-opam: ;
-
-# Phony wildcard targets
-phony: ;
-.PHONY: phony
+	@echo "# Installing builddep packages."
+	@opam install $(OPAMFLAGS) $(BUILDDEPFILES)
+.PHONY: builddep
+
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
+
+# 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

+# use NO_TEST=1 to skip the tests
+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)
-NORMALIZER=test-normalizer.sed
+TESTFILES:=$(shell find tests -name "*.v")
+NORMALIZER:=test-normalizer.sed
 
 test: $(TESTFILES:.v=.vo)
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(7|8)\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'
@@ -20,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 $@

ProofGuide.md

-# Iris Proof Guide
-
-This work-in-progress document serves to explain how Iris proofs are typically
-carried out in Coq: what are the common patterns, what are the common pitfalls.
-This complements the tactic documentation for the [proof mode](ProofMode.md) and
-[HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in
-the [style guide](StyleGuide.md).
-
-## Order of `Requires`
-
-In Coq, declarations in modules imported later may override the
-previous definition. Therefore, in order to make sure the most
-relevant declarations and notations always take priority, we recommend
-importing dependencies from the furthest to the closest.
-
-In particular, when importing Iris, Stdpp and Coq stdlib modules, we
-recommend importing in the following order:
-- Coq
-- stdpp
-- iris.bi
-- iris.proofmode
-- iris.algebra
-- iris.base_logic
-- iris.program_logic
-- iris.heap_lang
-
-## Combinators for functors
-
-In Iris, the type of propositions [iProp] is described by the solution to the
-recursive domain equation:
-
-```
-iProp ≅ uPred (F (iProp))
-```
-
-Here, `F` is a user-chosen locally contractive bifunctor from COFEs to unital
-Camaras (a step-indexed generalization of unital resource algebras). To make it
-convenient to construct such functors out of smaller pieces, we provide a number
-of abstractions:
-
-- [`cFunctor`](theories/algebra/ofe.v): bifunctors from COFEs to OFEs.
-- [`rFunctor`](theories/algebra/cmra.v): bifunctors from COFEs to cameras.
-- [`urFunctor`](theories/algebra/cmra.v): bifunctors from COFEs to unital
-  cameras.
-
-Besides, there are the classes `cFunctorContractive`, `rFunctorContractive`, and
-`urFunctorContractive` which describe the subset of the above functors that
-are contractive.
-
-To compose these functors, we provide a number of combinators, e.g.:
-
-- `constCF (A : ofeT) : cFunctor           := λ (B,B⁻), A `
-- `idCF : cFunctor                         := λ (B,B⁻), B`
-- `prodCF (F1 F2 : cFunctor) : cFunctor    := λ (B,B⁻), F1 (B,B⁻) * F2 (B,B⁻)`
-- `ofe_morCF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B⁻,B) -n> F2 (B,B⁻)`
-- `laterCF (F : cFunctor) : cFunctor       := λ (B,B⁻), later (F (B,B⁻))`
-- `agreeRF (F : cFunctor) : rFunctor       := λ (B,B⁻), agree (F (B,B⁻))`
-- `gmapURF K (F : rFunctor) : urFunctor    := λ (B,B⁻), gmap K (F (B,B⁻))`
-
-Using these combinators, one can easily construct bigger functors in point-free
-style, e.g:
-
-```
-F := gmapURF K (agreeRF (prodCF (constCF natC) (laterCF idCF)))
-```
-
-which effectively defines `F := λ (B,B⁻), gmap K (agree (nat * later B))`.
-
-Furthermore, for functors written using these combinators like the functor `F`
-above, Coq can automatically `urFunctorContractive F`.
-
-To make it a little bit more convenient to write down such functors, we make
-the constant functors (`constCF`, `constRF`, and `constURF`) a coercion, and
-provide the usual notation for products, etc. So the above functor can be
-written as follows (which is similar to the effective definition of `F` above):
-
-```
-F := gmapURF K (agreeRF (natC * ▶ ∙))
-```
-
-## Resource algebra management
-
-When using ghost state in Iris, you have to make sure that the resource algebras
-you need are actually available.  Every Iris proof is carried out using a
-universally quantified list `Σ: gFunctors` defining which resource algebras are
-available.  The `Σ` is the *global* list of resources that the entire proof can
-use.  We keep the `Σ` universally quantified to enable composition of proofs.
-
-You can think of this as a list of resource algebras, though in reality it is a
-list of locally contractive functors from COFEs to Cameras.  This list is used
-to define the parameter `F` of Iris mentioned in the previous section. The
-formal side of this is described in §7.4 of
-[The Iris Documentation](http://plv.mpi-sws.org/iris/appendix-3.1.pdf); here we
-describe the user-side Coq aspects of this approach.
-
-The assumptions that an Iris proof makes are collected in a type class called
-`somethingG`.  The most common kind of assumptions is `inG`, which says that a
-particular resource algebra is available for ghost state.  For example, in the
-[one-shot example](tests/one_shot.v):
-```
-Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
-```
-The `:>` means that the projection `one_shot_inG` is automatically registered as
-an instance for type-class resolution.  If you need several resource algebras,
-just add more `inG` fields.  If you are using another module as part of yours,
-add a field like `one_shot_other :> otherG Σ`.
-
-Having defined the type class, we need to provide a way to instantiate it.  This
-is an important step, as not every resource algebra can actually be used: if
-your resource algebra refers to `Σ`, the definition becomes recursive.  That is
-actually legal under some conditions (which is why the global list `Σ` contains
-functors and not just resource algebras), but for the purpose of this guide we
-will ignore that case.  We have to define a list that contains all the resource
-algebras we need:
-```
-Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
-```
-This time, there is no `Σ` in the context, so we cannot accidentally introduce a
-bad dependency.  If you are using another module as part of yours, add their
-`somethingΣ` to yours, as in `#[GFunctor one_shotR; somethingΣ]`.  (The
-`#[F1; F2; ...]` syntax *appends* the functor lists `F1`, `F2`, ... to each
-other; together with a coercion from a single functor to a singleton list, this
-means lists can be nested arbitrarily.)
-
-Now we can define the one and only instance that our type class will ever need:
-```
-Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
-Proof. solve_inG. Qed.
-```
-The `subG` assumption here says that the list `one_shotΣ` is a sublist of the
-global list `Σ`.  Typically, this should be the only assumption your instance
-needs, showing that the assumptions of the module (and all the modules it
-uses internally) can trivially be satisfied by picking the right `Σ`.
-
-Now you can add `one_shotG` as an assumption to all your module definitions and
-proofs.  We typically use a section for this:
-```
-Section proof.
-Context `{!heapG Σ, !one_shotG Σ}.
-```
-Notice that besides our own assumptions `one_shotG`, we also assume `heapG`,
-which are assumptions that every HeapLang proof makes (they are related to
-defining the `↦` connective as well as the basic Iris infrastructure for
-invariants and WP).  For this purpose, `heapG` contains not only assumptions
-about `Σ`, it also contains some ghost names to refer to particular ghost state
-(see "global ghost state instances" below).
-
-The backtic (`` ` ``) is used to make anonymous assumptions and to automatically
-generalize the `Σ`.  When adding assumptions with backtic, you should most of
-the time also add a `!` in front of every assumption.  If you do not then Coq
-will also automatically generalize all indices of type-classes that you are
-assuming.  This can easily lead to making more assumptions than you are aware
-of, and often it leads to duplicate assumptions which breaks type class
-resolutions.
-
-### Obtaining a closed proof
-
-To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
-`inG`, you have to assemble a list of functors of all the involved modules,
-and if your proof relies on some singleton (most do, at least indirectly; also
-see the next section), you have to call the respective initialization or
-adequacy lemma.  [For example](tests/one_shot.v):
-```
-Section client.
-  Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
-
-  Lemma client_safe : WP client {{ _, True }}%I.
-  (* ... *)
-End client.
-
-(** Assemble all functors needed by the [client_safe] proof. *)
-Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
-
-(** Apply [heap_adequacy] with this list of all functors. *)
-Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
-Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
-```
-
-### Advanced topic: Ghost state singletons
-
-Some Iris modules involve a form of "global state".  For example, defining the
-`↦` for HeapLang involves a piece of ghost state that matches the current
-physical heap.  The `gname` of that ghost state must be picked once when the
-proof starts, and then globally known everywhere.  Hence it is added to
-`gen_heapG`, the type class for the generalized heap module:
-```
-Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
-  gen_heap_name : gname
-}.
-```
-
-Such modules always need some kind of "initialization" to create an instance
-of their type class.  For example, the initialization for `heapG` is happening
-as part of [`heap_adequacy`](theories/heap_lang/adequacy.v); this in turn uses
-the initialization lemma for `gen_heapG` from
-[`gen_heap_init`](theories/base_logic/lib/gen_heap.v):
-```
-Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
-  (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
-```
-These lemmas themselves only make assumptions the way normal modules (those
-without global state) do, which are typically collected in a `somethingPreG`
-type class (such as `gen_heapPreG`):
-```
-Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V))
-}.
-```
-Just like in the normal case, `somethingPreG` type classes have an `Instance`
-showing that a `subG` is enough to instantiate them:
-```
-Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
-  subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
-Proof. solve_inG. Qed.
-```
-The initialization lemma then shows that the `somethingPreG` type class is
-enough to create an instance of the main `somethingG` class *below a view
-shift*.  This is written with an existential quantifier in the lemma because the
-statement after the view shift (`gen_heap_ctx σ` in this case) depends on having
-an instance of `gen_heapG` in the context.
-
-Given that these global ghost state instances are singletons, they must be
-assumed explicitly everywhere.  Bundling `heapG` in a module type class like
-`one_shotG` would lose track of the fact that there exists just one `heapG`
-instance that is shared by everyone.
-
-### Advanced topic: Additional module assumptions
-
-Some modules need additional assumptions.  For example, the STS module is
-parameterized by an STS and assumes that the STS state space is inhabited:
-```
-Class stsG Σ (sts : stsT) := {
-  sts_inG :> inG Σ (stsR sts);
-  sts_inhabited :> Inhabited (sts.state sts);
-}.
-```
-In this rather exceptional case, the `Instance` for this class has more than
-just a `subG` assumption:
-```
-Instance subG_stsΣ Σ sts :
-  subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
-```
-If users of this module follow the pattern described above, their own type class
-instance will check these additional assumption.  But this is one more reason
-why it is important for every module to have an instance for its `somethingG`:
-to make sure that it does not accidentally make more assumptions than it intends
-to.
-
-Another subtle detail here is that the `subG` assumption comes first in
-`subG_stsΣ`, i.e., it appears before the `Inhabited`.  This is important because
-otherwise, `sts_inhabited` and `subG_stsΣ` form an instance cycle that makes
-type class search diverge.
-
-## Canonical structures and type classes
-
-In Iris, we use both canonical structures and type classes, and some careful
-tweaking is necessary to make the two work together properly.  The details of
-this still need to be written up properly, but here is some background material:
-
-* [Type Classes for Mathematics in Type Theory](http://www.eelis.net/research/math-classes/mscs.pdf)
-* [Canonical Structures for the working Coq user](https://hal.inria.fr/hal-00816703v1/document)

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
@@ -9,8 +9,20 @@ 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
-[docs/iris.tex](docs/iris.tex).  A compiled PDF version of this document is
-[available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
+[tex/iris.tex](tex/iris.tex).  A compiled PDF version of this document is
+[available online](http://plv.mpi-sws.org/iris/appendix-3.4.pdf).
+
+## Side-effects
+
+Importing Iris has some side effects as the library sets some global options.
+
+* First of all, Iris imports std++, so the
+  [std++ side-effects](https://gitlab.mpi-sws.org/iris/stdpp/#side-effects)
+  apply.
+* On top of that, Iris imports ssreflect, which replaces the default `rewrite`
+  tactic with the ssreflect version. However, `done` is overwritten to keep
+  using the std++ version of the tactic.  We also set `SsrOldRewriteGoalsOrder`
+  and re-open `general_if_scope` to un-do some effects of ssreflect.
 
 ## Building Iris
 
@@ -18,17 +30,19 @@ definitions and some derived forms is available in
 
 This version is known to compile with:
 
- - Coq 8.8.2 / 8.9.0 / 8.9.1 / 8.10.0 / 8.10.1
+ - Coq 8.19.2 / 8.20.1
  - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
 
-For a version compatible with Coq 8.6, have a look at the
-[iris-3.1 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.1).
-If you need to work with Coq 8.5, please check out the
-[iris-3.0 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.0).
+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
 
-To use Iris in your own proofs, we recommend you install Iris via opam (1.2.2 or
+To use Iris in your own proofs, we recommend you install Iris via opam (2.0.0 or
 newer).  To obtain the latest stable release, you have to add the Coq opam
 repository:
 
@@ -38,61 +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.
 
-### Working *on* Iris
+To fetch updates later, run `opam update && opam upgrade`.
 
-To work on Iris itself, you need to install its build-dependencies.  Again we
-recommend you do that with opam (1.2.2 or newer).  This requires the following
-two repositories:
+#### Be notified of breaking changes
 
-    opam repo add coq-released https://coq.inria.fr/opam/released
-    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+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).
 
-Once you got opam set up, run `make build-dep` to install the right versions
-of the dependencies.
+#### Use of Iris in submitted artifacts
 
-Run `make -jN` to build the full development, where `N` is the number of your
-CPU cores.
+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.
+
+### 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
-  [ProofMode.md](ProofMode.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 [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
 
@@ -108,36 +157,40 @@ that should be compatible with this version:
 * [Iron](https://gitlab.mpi-sws.org/iris/iron) is a linear separation logic
   built on top of Iris for precise reasoning about resources (such as making
   sure there are no memory leaks).
+* [Actris](https://gitlab.mpi-sws.org/iris/actris) is a separation logic
+  built on top of Iris for session-type based reasoning of message-passing
+  programs.
 
 ## Further Resources
 
 Getting along with Iris in Coq:
 
-* Iris proof patterns are documented in the [proof guide](ProofGuide.md).
-* Syntactic conventions are described in the [style guide](StyleGuide.md).
+* 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](ProofMode.md) as well as the
-  [HeapLang documentation](HeapLang.md).
+  [the Iris Proof Mode (IPM) / MoSeL documentation](docs/proof_mode.md) as well as the
+  [HeapLang documentation](docs/heap_lang.md).
 * The generated coqdoc is [available online](https://plv.mpi-sws.org/coqdoc/iris/).
 
 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:
 
 * Information on how to set up your editor for unicode input and output is
-  collected in [Editor.md](Editor.md).
+  collected in [editor.md](docs/editor.md).
 * If you are writing a paper that uses Iris in one way or another, you could use
-  the [Iris LaTeX macros](docs/iris.sty) for typesetting the various Iris
+  the [Iris LaTeX macros](tex/iris.sty) for typesetting the various Iris
   connectives.

StyleGuide.md

-# Iris Style Guide
-
-This document lays down syntactic conventions about how we usually write our
-Iris proofs in Coq.  It is a work-in-progress.  This complements the tactic
-documentation for the [proof mode](ProofMode.md) and [HeapLang](HeapLang.md) as
-well as the [proof guide](ProofGuide.md).
-
-## Implicit generalization
-
-We often use the implicit generalization feature of Coq, triggered by a backtic:
-`` `{!term A B}`` means that an implicit argument of type `term A B` is added,
-and if any of the identifiers that are used here is not yet bound, it gets added
-as well.  Usually, `term` will be some existing type class or similar, and we
-use this syntax to also generalize over `A` and `B`; then the above is
-equivalent to `{A B} {Hterm: term A B}`.  The `!` in front of the term disables
-an even stronger form of generalization, where if `term` is a type class then
-all missing arguments get implicitly generalized as well.  This is sometimes
-useful, e.g. we can write `` `{Countable C}`` instead of `` `{!EqDecision C,
-!Countable C}``.  However, generally it is more important to be aware of the
-assumptions you are making, so implicit generalization without `!` should be
-avoided.
-
-## Type class resolution control
-
-When you are writing a module that exports some Iris term for others to use
-(e.g., `join_handle` in the [spawn module](theories/heap_lang/lib/spawn.v)), be
-sure to mark these terms as opaque for type class search at the *end* of your
-module (and outside any section):
-```
-Typeclasses Opaque join_handle.
-```
-This makes sure that the proof mode does not "look into" your definition when it
-is used by clients.
-
-## Naming conventions for variables/arguments/hypotheses
-
-### small letters
-
-* a : A = cmraT or ofeT
-* b : B = cmraT or ofeT
-* c
-* d
-* e : expr = expressions
-* f = some generic function
-* g = some generic function
-* h : heap
-* i
-* j
-* k
-* l
-* m : iGst = ghost state
-* m* = prefix for option
-* n
-* o
-* p
-* q
-* r : iRes = resources
-* s = state (STSs)
-* s = stuckness bits
-* t
-* u
-* v : val = values of language
-* w
-* x
-* y
-* z 
-
-### capital letters
-
-* A : Type, cmraT or ofeT
-* B : Type, cmraT or ofeT
-* C
-* D   
-* E : coPset = Viewshift masks
-* F = a functor
-* G
-* H = hypotheses
-* I = indexing sets
-* J
-* K : ectx = evaluation contexts
-* K = keys of a map
-* L
-* M = maps / global CMRA
-* N : namespace
-* O 
-* P : uPred, iProp or Prop
-* Q : uPred, iProp or Prop
-* R : uPred, iProp or Prop
-* S : set state = state sets in STSs
-* T : set token = token sets in STSs
-* U
-* V : abstraction of value type in frame shift assertions
-* W
-* X : sets
-* Y : sets
-* Z : sets
-
-### small greek letters
-
-* γ : gname
-* σ : state = state of language
-* φ : interpretation of STS/Auth
-
-### capital greek letters
-
-* Φ : general predicate (over uPred, iProp or Prop)
-* Ψ : general predicate (over uPred, iProp or Prop)
-
-## Naming conventions for algebraic classes
-
-### Suffixes
-
-* O: OFEs
-* R: cameras
-* UR: unital cameras or resources algebras
-* F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
-* G: global camera functor management (typeclass; see `ProofGuide.md`)
-* I: bunched implication logic (of type `bi`)
-* SI: step-indexed bunched implication logic (of type `sbi`)
-* T: canonical structures for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
-* Σ: global camera functor management (`gFunctors`; see `ProofGuide.md`)

_CoqProject

--Q theories iris
-# We sometimes want to locally override notation (e.g. in proofmode/base.v, bi/embedding.v), and there
-# is no good way to do that with scopes.
+# 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
-# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
+# Cannot use non-canonical projections as it causes massive unification failures
+# (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
-# change_no_check does not exist yet in 8.9.
--arg -w -arg -convert_concl_no_check
-# "Declare Scope" does not exist yet in 8.9.
--arg -w -arg -undeclared-scope
-# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
--arg -w -arg -ambiguous-paths
+# 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/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/algebra/monoid.v
-theories/algebra/cmra.v
-theories/algebra/big_op.v
-theories/algebra/cmra_big_op.v
-theories/algebra/sts.v
-theories/algebra/auth.v
-theories/algebra/frac_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/deprecated.v
-theories/algebra/proofmode_classes.v
-theories/algebra/ufrac.v
-theories/algebra/namespace_map.v
-theories/algebra/ufrac_auth.v
-theories/bi/notation.v
-theories/bi/interface.v
-theories/bi/derived_connectives.v
-theories/bi/derived_laws_bi.v
-theories/bi/derived_laws_sbi.v
-theories/bi/plainly.v
-theories/bi/big_op.v
-theories/bi/updates.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/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/fancy_updates_from_vs.v
-theories/base_logic/lib/proph_map.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/lifting.v
-theories/heap_lang/array.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/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/proofmode/base.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_bi.v
-theories/proofmode/class_instances_sbi.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()