.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,7 +13,15 @@
 *.bak
 .coqdeps.d
 .coq-native/
-build-dep/
+*.crashcoqide
+.env
+builddep/
+_CoqProject.*
 Makefile.coq
 Makefile.coq.conf
-*.crashcoqide
+.Makefile.coq.d
+Makefile.package.*
+.Makefile.package.*
+_opam
+_build
+*.install

.gitlab-ci.yml

@@ -5,70 +5,91 @@ 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:
-  - git clone https://gitlab.mpi-sws.org/FP/iris-ci.git ci -b opam2
+  - git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
   - ci/buildjob
   cache:
     key: "$CI_JOB_NAME"
     paths:
-    - opamroot/
-  only:
-  - master
-  - /^ci/
+    - _opam/
   except:
   - triggers
   - schedules
+  - api
 
 ## 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"
-    VALIDATE: "1"
-
-build-coq.8.9.dev:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.9.dev"
-    TIMING_PROJECT: "iris"
-    TIMING_CONF: "coq-8.9.dev"
+    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.8.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.8.2"
+    OPAM_PINS: "coq version 8.20.1"
+    DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
 
-build-coq.8.8.1:
+# Also ensure Dune works.
+build-coq.8.20.1-dune:
   <<: *template
+  <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.8.1"
+    OPAM_PINS: "coq version 8.20.1   dune version 3.15.2"
+    MAKE_TARGET: "dune"
 
-build-coq.8.8.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.8.0"
-    OPAM_PKG: "coq-iris"
-    DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
-    TIMING_PROJECT: "iris"
-    TIMING_CONF: "coq-8.8.0"
-  tags:
-  - fp-timing
-
-build-coq.8.7.2:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.7.2"
+    OPAM_PINS: "coq version 8.19.2"
 
-build-coq.8.7.1:
+trigger-stdpp.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.7.1"
+    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

.gitlab/issue_templates/Bug.md

+<!--
+
+When reporting a bug, please always include the version of Iris you are using.
+If you are using opam, you can determine your Iris version by running
+
+  opam show coq-iris -f version
+
+-->

.gitmodules

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

CONTRIBUTING.md

 # Contributing to the Iris Coq Development
 
-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 want to report a bug, please use the
-[issue tracker](https://gitlab.mpi-sws.org/FP/iris-coq/issues), which also
-requires an MPI-SWS GitLab account.  To contribute code, please send your
-MPI-SWS GitLab username to [Ralf Jung](https://gitlab.mpi-sws.org/jung) to
-enable personal projects for your account.  Then you can fork the
-[Iris git repository](https://gitlab.mpi-sws.org/FP/iris-coq/), make your
-changes in your fork, and create a merge request.
+Here you can find some how-tos for various thing sthat might come up when doing
+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 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.  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.
+
+[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.
+  (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.
+
+## How to write/update test cases
+
+The files in `tests/` are test cases.  Each of the `.v` files comes with a
+matching `.ref` file containing the expected output of `coqc`.  Adding `Show.`
+in selected places in the proofs makes `coqc` print the current goal state.
+This is used to make sure the proof mode prints goals and reduces terms the way
+we expect it to.  You can run `make MAKE_REF=1` to re-generate all the `.ref` files;
+this is useful after adding or removing `Show.` from a test.  If you do this,
+make sure to check the diff for any unexpected changes in the output!
+
+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.
+
+If you want to compile without tests run `make NO_TEST=1`.
+
+## How to build/install only one package
+
+Iris is split into multiple packages that can be installed separately via opam.
+You can invoke the Makefile of a particular package by doing `./make-package
+$PACKAGE $MAKE_ARGS`, where `$MAKE_ARGS` are passed to `make` (so you can use
+the usual `-jN`, `install`, ...).  This should only rarely be necessary. For
+example, if you are not using opam and you want to install only the `iris`
+package (without HeapLang, to avoid waiting on that part of the build), you can
+do `./make-package iris install`.  (If you are using opam, you can achieve the
+same by pinning `coq-iris` to your Iris checkout.)
+
+Note that `./make-package` will never run the test suite, so please always do a
+regular `make -jN` before submitting an MR.
+
+## How to 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:
+```
+export GITLAB_TOKEN=<your token here>
+```
+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

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 $$(test -d tests && echo tests) \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
-	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 awk.Makefile
-	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
+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.
-	@# Reinstalling is needed with opam 1 in case the pin already exists, but the builddep
-	@# package changed.
-	@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
-	  echo "# Pinning build-dep package." && \
-	  opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
-	  ((! opam --version | grep "^1\." > /dev/null) || ( \
-	    echo "# Reinstalling build-dep package." && \
-	    opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE" \
-	  ))
-
-# Some files that do *not* need to be forwarded to Makefile.coq
-Makefile: ;
-_CoqProject: ;
-awk.Makefile: ;
-opam: ;
-
-# Phony wildcard targets
-phony: ;
-.PHONY: phony
+	@# dependencies, but does not actually install anything itself.
+	@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

-# run tests with main build
-real-all: test
+# 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: 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)
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-COQ_BROKEN=
-
-# Can't use pipes because that discards error codes and dash provides no way to control that.
-# Also egrep errors if it doesn't match anything, we have to ignore that.
-# Oh Unix...
-REF_FILTER=egrep -v '(^Welcome to Coq|^Skipping rcfile loading.$$)'
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
 	$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
 -include tests/.coqdeps.d
 
-$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
-	$(SHOW)$(if $(MAKE_REF),COQTEST [ref],$(if $(COQ_BROKEN),COQTEST [ignored],COQTEST)) $<
-	$(HIDE)TEST="$$(basename -s .v $<)" && \
+# 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)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" && \
-	  ($(REF_FILTER) < "$$TMPFILE" > "$$TMPFILE.filtered" || true) && \
-	  $(if $(MAKE_REF), \
-	    mv "$$TMPFILE.filtered" "tests/$$TEST.ref", \
-	    $(if $(COQ_BROKEN), \
-	      true, \
-	      diff -u "tests/$$TEST.ref" "$$TMPFILE.filtered" \
-	    ) \
+	  sed -E -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
+	  mv "$$TMPFILE".new "$$TMPFILE" && \
+	  $(if $(COQ_REF),\
+	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
+	    true \
 	  ) && \
-	  rm -f "$$TMPFILE" "$$TMPFILE.filtered" && \
+	  rm -f "$$TMPFILE" && \
 	  touch $@

Naming.md

-# Naming conventions for variables/arguments/hypotheses in the Coq development
-
-## small letters
-
-* a : A = cmraT or cofeT
-* b : B = cmraT or cofeT
-* 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 cofeT
-* B : Type, cmraT or cofeT
-* 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 in the Coq development
-
-## Suffixes
-
-* C: OFEs
-* R: cameras
-* UR: unital cameras or resources algebras
-* F: functors (can be combined with all of the above, e.g. CF is an OFE functor)
-* G: global camera functor management
-* T: canonical structurs for algebraic classes (for example ofeT for OFEs, cmraT for cameras)

ProofMode.md

-Tactic overview
-===============
-
-Many of the tactics below apply to more goals than described in this document
-since the behavior of these tactics can be tuned via instances of the type
-classes in the file [proofmode/classes](proofmode/classes.v). Most notable, many
-of the tactics can be applied when the to be introduced or to be eliminated
-connective appears under a later, an update modality, or in the conclusion of a
-weakest precondition.
-
-Applying hypotheses and lemmas
-------------------------------
-
-- `iExact "H"`  : finish the goal if the conclusion matches the hypothesis `H`
-- `iAssumption` : finish the goal if the conclusion matches any hypothesis
-- `iApply pm_trm` : match the conclusion of the current goal against the
-  conclusion of `pm_trm` and generates goals for the premises of `pm_trm`. See
-  proof mode terms below.
-  If the applied term has more premises than given specialization patterns, the
-  pattern is extended with `[] ... []`.  As a consequence, all unused spatial
-  hypotheses move to the last premise.
-
-Context management
-------------------
-
-- `iIntros (x1 ... xn) "ipat1 ... ipatn"` : introduce universal quantifiers
-  using Coq introduction patterns `x1 ... xn` and implications/wands using proof
-  mode introduction patterns `ipat1 ... ipatn`.
-- `iClear (x1 ... xn) "selpat"` : clear the hypotheses given by the selection
-  pattern `selpat` and the Coq level hypotheses/variables `x1 ... xn`.
-- `iRevert (x1 ... xn) "selpat"` : revert the hypotheses given by the selection
-  pattern `selpat` into wands, and the Coq level hypotheses/variables
-  `x1 ... xn` into universal quantifiers. Persistent hypotheses are wrapped into
-  the persistence modality.
-- `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
-- `iSpecialize pm_trm` : instantiate universal quantifiers and eliminate
-  implications/wands of a hypothesis `pm_trm`. See proof mode terms below.
-- `iSpecialize pm_trm as #` : instantiate universal quantifiers and eliminate
-  implications/wands of a hypothesis whose conclusion is persistent. In this
-  case, all hypotheses can be used for proving the premises, as well as for
-  the resulting goal.
-- `iPoseProof pm_trm as (x1 ... xn) "ipat"` : put `pm_trm` into the context and
-  eliminates it. This tactic is essentially the same as `iDestruct` with the
-  difference that when `pm_trm` is a non-universally quantified intuitionistic
-  hypothesis, it will not throw the hypothesis away.
-- `iAssert P with "spat" as "ipat"` : generates a new subgoal `P` and adds the
-  hypothesis `P` to the current goal. The specialization pattern `spat`
-  specifies which hypotheses will be consumed by proving `P`. The introduction
-  pattern `ipat` specifies how to eliminate `P`.
-  In case all branches of `ipat` start with a `#` (which causes `P` to be moved
-  to the persistent context) or with an `%` (which causes `P` to be moved to the
-  pure Coq context), then one can use all hypotheses for proving `P` as well as
-  for proving the current goal.
-- `iAssert P as %cpat` : assert `P` and eliminate it using the Coq introduction
-  pattern `cpat`. All hypotheses can be used for proving `P` as well as for
-  proving the current goal.
-
-Introduction of logical connectives
------------------------------------
-
-- `iPureIntro` : turn a pure goal into a Coq goal. This tactic works for goals
-  of the shape `⌜φ⌝`, `a ≡ b` on discrete COFEs, and `✓ a` on discrete CMRAs.
-
-- `iLeft` : left introduction of disjunction.
-- `iRight` : right introduction of disjunction.
-
-- `iSplit` : introduction of a conjunction, or separating conjunction provided
-  one of the operands is persistent.
-- `iSplitL "H1 ... Hn"` : introduction of a separating conjunction. The
-  hypotheses `H1 ... Hn` are used for the left conjunct, and the remaining ones
-  for the right conjunct. Persistent hypotheses are ignored, since these do not
-  need to be split.
-- `iSplitR "H0 ... Hn"` : symmetric version of the above.
-- `iExist t1, .., tn` : introduction of an existential quantifier.
-
-Elimination of logical connectives
-----------------------------------
-
-- `iExFalso` : Ex falso sequitur quod libet.
-- `iDestruct pm_trm as (x1 ... xn) "ipat"` : elimination of a series of
-  existential quantifiers using Coq introduction patterns `x1 ... xn`, and
-  elimination of an object level connective using the proof mode introduction
-  pattern `ipat`.
-  In case all branches of `ipat` start with a `#` (which causes the hypothesis
-  to be moved to the persistent context) or with an `%` (which causes the
-  hypothesis to be moved to the pure Coq context), then one can use all
-  hypotheses for proving the premises of `pm_trm`, as well as for proving the
-  resulting goal. Note that in this case the hypotheses still need to be
-  subdivided among the spatial premises.
-- `iDestruct pm_trm as %cpat` : elimination of a pure hypothesis using the Coq
-  introduction pattern `cpat`. When using this tactic, all hypotheses can be
-  used for proving the premises of `pm_trm`, as well as for proving the
-  resulting goal.
-
-Separating logic specific tactics
----------------------------------
-
-- `iFrame (t1 .. tn) "selpat"` : cancel the Coq terms (or Coq hypotheses)
-  `t1 ... tn` and Iris hypotheses given by `selpat` in the goal. The constructs
-  of the selection pattern have the following meaning:
-
-  + `%` : repeatedly frame hypotheses from the Coq context.
-  + `#` : repeatedly frame hypotheses from the persistent context.
-  + `∗` : frame as much of the spatial context as possible.
-
-  Notice that framing spatial hypotheses makes them disappear, but framing Coq
-  or persistent hypotheses does not make them disappear.
-
-  This tactic finishes the goal in case everything in the conclusion has been
-  framed.
-- `iCombine "H1" "H2" as "pat"` : turns `H1 : P1` and `H2 : P2` into
-  `P1 ∗ P2`, on which `iDetruct ... as pat` is called.
-
-Modalities
-----------
-
-- `iModIntro mod` : introduction of a modality. The type class `FromModal` is
-  used to specify which modalities this tactic should introduce. Instances of
-  that type class include: later, except 0, basic update and fancy update,
-  persistently, affinely, plainly, absorbingly, objectively, and subjectively.
-  The optional argument `mod` can be used to specify what modality to introduce
-  in case of ambiguity, e.g. `⎡|==> P⎤`.
-- `iAlways` : a deprecated alias of `iModIntro`.
-- `iNext n` : an alias of `iModIntro (▷^n P)`.
-- `iNext` : an alias of `iModIntro (▷^1 P)`.
-- `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is
-  an instance of the `ElimModal` type class. Instances include: later, except 0,
-  basic update and fancy update.
-
-Induction
----------
-
-- `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction by
-  generating a hypothesis `IH : ▷ goal`. The tactic generalizes over the Coq
-  level variables `x1 ... xn`, the hypotheses given by the selection pattern
-  `selpat`, and the spatial context.
-- `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction on
-  the Coq term `x`. The Coq introduction pattern is used to name the introduced
-  variables. The induction hypotheses are inserted into the persistent context
-  and given fresh names prefixed `IH`. The tactic generalizes over the Coq level
-  variables `x1 ... xn`, the hypotheses given by the selection pattern `selpat`,
-  and the spatial context.
-
-Rewriting / simplification
---------------------------
-
-- `iRewrite pm_trm` / `iRewrite pm_trm in "H"` : rewrite using an internal
-  equality in the proof mode goal / hypothesis `H`.
-- `iEval (tac)` / `iEval (tac) in H` : performs a tactic `tac` on the proof mode
-  goal / hypothesis `H`. The tactic `tac` should be a reduction or rewriting
-  tactic like `simpl`, `cbv`, `lazy`, `rewrite` or `setoid_rewrite`. The `iEval`
-  tactic is implemented by running `tac` on `?evar ⊢ P` / `P ⊢ ?evar` where `P`
-  is the proof goal / hypothesis `H`. After running `tac`, `?evar` is unified
-  with the resulting `P`, which in turn becomes the new proof mode goal /
-  hypothesis `H`.
-  Note that parentheses around `tac` are needed.
-- `iSimpl` / `iSimpl in H` : performs `simpl` on the proof mode goal /
-  hypothesis `H`. This is a shorthand for `iEval (simpl)`.
-
-
-Iris
-----
-
-- `iInv S with "selpat" as (x1 ... xn) "ipat" "Hclose"` : where `S` is either
-   a namespace N or an identifier "H". Open the invariant indicated by S.  The
-   selection pattern `selpat` is used for any auxiliary assertions needed to
-   open the invariant (e.g. for cancelable or non-atomic invariants). The update
-   for closing the invariant is put in a hypothesis named `Hclose`.
-
-Miscellaneous
--------------
-
-- The tactic `done` is extended so that it also performs `iAssumption` and
-  introduces pure connectives.
-- The proof mode adds hints to the core `eauto` database so that `eauto`
-  automatically introduces: conjunctions and disjunctions, universal and
-  existential quantifiers, implications and wand, plainness, persistence, later
-  and update modalities, and pure connectives.
-
-Selection patterns
-==================
-
-Selection patterns are used to select hypotheses in the tactics `iRevert`,
-`iClear`, `iFrame`, `iLöb` and `iInduction`. The proof mode supports the
-following _selection patterns_:
-
-- `H` : select the hypothesis named `H`.
-- `%` : select the entire pure/Coq context.
-- `#` : select the entire persistent context.
-- `∗` : select the entire spatial context.
-
-Introduction patterns
-=====================
-
-Introduction patterns are used to perform introductions and eliminations of
-multiple connectives on the fly. The proof mode supports the following
-_introduction patterns_:
-
-- `H` : create a hypothesis named `H`.
-- `?` : create an anonymous hypothesis.
-- `_` : remove the hypothesis.
-- `$` : frame the hypothesis in the goal.
-- `[ipat1 ipat2]` : (separating) conjunction elimination. In order to eliminate
-  conjunctions `P ∧ Q` in the spatial context, one of the following conditions
-  should hold:
-  + Either the proposition `P` or `Q` should be persistent.
-  + Either `ipat1` or `ipat2` should be `_`, which results in one of the
-    conjuncts to be thrown away.
-- `[ipat1|ipat2]` : disjunction elimination.
-- `[]` : false elimination.
-- `%` : move the hypothesis to the pure Coq context (anonymously).
-- `->` and `<-` : rewrite using a pure Coq equality
-- `# ipat` : move the hypothesis to the persistent context.
-- `> ipat` : eliminate a modality (if the goal permits).
-
-Apart from this, there are the following introduction patterns that can only
-appear at the top level:
-
-- `{selpat}` : clear the hypotheses given by the selection pattern `selpat`.
-  Items of the selection pattern can be prefixed with `$`, which cause them to
-  be framed instead of cleared.
-- `!%` : introduce a pure goal (and leave the proof mode).
-- `!>` : introduce a modality by calling `iModIntro`.
-- `!#` : introduce a modality by calling `iModIntro` (deprecated).
-- `/=` : perform `simpl`.
-- `//` : perform `try done` on all goals.
-- `//=` : syntactic sugar for `/= //`
-- `*` : introduce all universal quantifiers.
-- `**` : introduce all universal quantifiers, as well as all arrows and wands.
-
-For example, given:
-
-        ∀ x, x = 0 ⊢ □ (P → False ∨ □ (Q ∧ ▷ R) -∗ P ∗ ▷ (R ∗ Q ∧ x = pred 2)).
-
-You can write
-
-        iIntros (x) "% !# $ [[] | #[HQ HR]] /= !>".
-
-which results in:
-
-        x : nat
-        H : x = 0
-        ______________________________________(1/1)
-        "HQ" : Q
-        "HR" : R
-        --------------------------------------□
-        R ∗ Q ∧ x = 1
-
-
-Specialization patterns
-=======================
-
-Since we are reasoning in a spatial logic, when eliminating a lemma or
-hypothesis of type ``P_0 -∗ ... -∗ P_n -∗ R``, one has to specify how the
-hypotheses are split between the premises. The proof mode supports the following
-_specification patterns_ to express splitting of hypotheses:
-
-- `H` : use the hypothesis `H` (it should match the premise exactly). If `H` is
-  spatial, it will be consumed.
-
-- `[H1 .. Hn]` and `[H1 .. Hn //]` : generate a goal for the premise with the
-  (spatial) hypotheses `H1 ... Hn` and all persistent hypotheses. The spatial
-  hypotheses among `H1 ... Hn` will be consumed, and will not be available for
-  subsequent goals. Hypotheses prefixed with a `$` will be framed in the
-  goal for the premise. The pattern can be terminated with a `//`, which causes
-  `done` to be called to close the goal (after framing).
-- `[-H1 ... Hn]` and `[-H1 ... Hn //]` : the negated forms of the above
-  patterns, where the goal for the premise will have all spatial premises except
-  `H1 .. Hn`.
-
-- `[> H1 ... Hn]` and `[> H1 ... Hn //]` : like the above patterns, but these
-  patterns can only be used if the goal is a modality `M`, in which case
-  the goal for the premise will be wrapped in the modality `M`.
-- `[> -H1 ... Hn]` and `[> -H1 ... Hn //]` : the negated forms of the above
-  patterns.
-
-- `[# $H1 .. $Hn]` and `[# $H1 .. $Hn //]` : generate a goal for a persistent
-  premise in which all hypotheses are available. This pattern does not consume
-  any hypotheses; all hypotheses are available in the goal for the premise, as
-  well in the subsequent goal. The hypotheses `$H1 ... $Hn` will be framed in
-  the goal for the premise. These patterns can be terminated with a `//`, which
-  causes `done` to be called to close the goal (after framing).
-- `[%]` and `[% //]` : generate a Coq goal for a pure premise. This pattern
-  does not consume any hypotheses. The pattern can be terminated with a `//`,
-  which causes `done` to be called to close the goal.
-
-- `[$]` : solve the premise by framing. It will first repeatedly frame the
-  spatial hypotheses, and then repeatedly frame the persistent hypotheses.
-  Spatial hypothesis that are not framed are carried over to the subsequent
-  goal.
-- `[> $]` : like the above pattern, but this pattern can only be used if the
-  goal is a modality `M`, in which case the goal for the premise will be wrapped
-  in the modality `M` before framing.
-- `[# $]` : solve the persistent premise by framing. It will first repeatedly
-  frame the spatial hypotheses, and then repeatedly frame the persistent
-  hypotheses. This pattern does not consume any hypotheses.
-
-For example, given:
-
-        H : □ P -∗ P 2 -∗ R -∗ x = 0 -∗ Q1 ∗ Q2
-
-One can write:
-
-        iDestruct ("H" with "[#] [H1 $H2] [$] [% //]") as "[H4 H5]".
-
-
-Proof mode terms
-================
-
-Many of the proof mode tactics (such as `iDestruct`, `iApply`, `iRewrite`) can
-take both hypotheses and lemmas, and allow one to instantiate universal
-quantifiers and implications/wands of these hypotheses/lemmas on the fly.
-
-The syntax for the arguments of these tactics, called _proof mode terms_, is:
-
-        (H $! t1 ... tn with "spat1 .. spatn")
-
-Here, `H` can be both a hypothesis, as well as a Coq lemma whose conclusion is
-of the shape `P ⊢ Q`. In the above, `t1 ... tn` are arbitrary Coq terms used
-for instantiation of universal quantifiers, and `spat1 .. spatn` are
-specialization patterns to eliminate implications and wands.
-
-Proof mode terms can be written down using the following short hands too:
-
-        (H with "spat1 .. spatn")
-        (H $! t1 ... tn)
-        H
-

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.7.1 / 8.7.2 / 8.8.0 / 8.8.1 / 8.8.2
+ - 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/FP/iris-coq/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/FP/iris-coq/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:
 
@@ -36,101 +50,147 @@ repository:
 
 To obtain a development version, also add the Iris opam repository:
 
-    opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
+    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/FP/opam-dev.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).
+
+#### 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
-  [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/FP/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.
+    [Iris Examples](https://gitlab.mpi-sws.org/iris/examples).
+* 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
 
 The following is a (probably incomplete) list of case studies that use Iris, and
 that should be compatible with this version:
 
-* [Iris Examples](https://gitlab.mpi-sws.org/FP/iris-examples) is where we
+* [Iris Examples](https://gitlab.mpi-sws.org/iris/examples) is where we
   collect miscellaneous case studies that do not have their own repository.
-* [LambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/) is a Coq
+* [LambdaRust](https://gitlab.mpi-sws.org/iris/lambda-rust) is a Coq
   formalization of the core Rust type system.
-* [iGPS](https://gitlab.mpi-sws.org/FP/sra-gps/tree/gen_proofmode_WIP) is a
-  logic for release-acquire memory.
-* [Iris Atomic](https://gitlab.mpi-sws.org/FP/iris-atomic/) is an experimental
-  formalization of logically atomic triples in Iris.
-
-## Notes for Iris Developers
+* [GPFSL](https://gitlab.mpi-sws.org/iris/gpfsl) is a logic for release-acquire
+  and relaxed memory.
+* [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:
+
+* 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).
+* The generated coqdoc is [available online](https://plv.mpi-sws.org/coqdoc/iris/).
+
+Contacting the developers:
+
+* 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 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).
-* The Iris Proof Mode (IPM) / MoSeL is documented at [ProofMode.md](ProofMode.md).
-* Naming conventions are documented at [Naming.md](Naming.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++.
-  You may have to do `make clean` as Coq will likely complain about .vo file
-  mismatches.
-
-### How to write/update test cases
-
-The files in `tests/` are test cases.  Each of the `.v` files comes with a
-matching `.ref` file containing the expected output of `coqc`.  Adding `Show.`
-in selected places in the proofs makes `coqc` print the current goal state.
-This is used to make sure the proof mode prints goals and reduces terms the way
-we expect it to.  You can run `MAKE_REF=1 make` to re-generate all the `.ref` files;
-this is useful after adding or removing `Show.` from a test.  If you do this,
-make sure to check the diff for any unexpected changes in the output!
+  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](tex/iris.sty) for typesetting the various Iris
+  connectives.

_CoqProject

--Q theories iris
--arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-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/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/counter_examples.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/double_negation.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/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/lang.v
-theories/heap_lang/metatheory.v
-theories/heap_lang/tactics.v
-theories/heap_lang/lifting.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_map.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/coin_flip.v
-theories/heap_lang/lib/counter.v
-theories/heap_lang/lib/atomic_heap.v
-theories/heap_lang/lib/increment.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
+# 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
+
+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'))