.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
 *.glob
 *.cache
 *.aux
@@ -8,6 +11,17 @@
 .\#*
 *~
 *.bak
+.coqdeps.d
 .coq-native/
-Makefile.coq
 *.crashcoqide
+.env
+builddep/
+_CoqProject.*
+Makefile.coq
+Makefile.coq.conf
+.Makefile.coq.d
+Makefile.package.*
+.Makefile.package.*
+_opam
+_build
+*.install

.gitlab-ci.yml

-image: ralfjung/opam-ci:latest
+image: ralfjung/opam-ci:opam2
 
-iris-coq8.6:
+stages:
+  - build
+
+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:
-  - coq
+  - fp
   script:
-  # prepare
-  - . build/opam-ci.sh coq 8.6 coq-mathcomp-ssreflect 1.6.1
-  # build
-  - 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
-  - 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
-  - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
-  - 'if (( RANDOM % 10 == 0 )); then make validate; fi'
+  - git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
+  - ci/buildjob
   cache:
-    key: "coq8.6"
+    key: "$CI_JOB_NAME"
     paths:
-    - opamroot/
+    - _opam/
+  except:
+  - triggers
+  - schedules
+  - api
+
+## Build jobs
+
+# The newest version runs with timing.
+build-coq.8.20.1:
+  <<: *template
+  variables:
+    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
+
+# The newest version also runs in MRs, without timing.
+build-coq.8.20.1-mr:
+  <<: *template
+  <<: *only_mr
+  variables:
+    OPAM_PINS: "coq version 8.20.1"
+    DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
+
+# Also ensure Dune works.
+build-coq.8.20.1-dune:
+  <<: *template
+  <<: *branches_and_mr
+  variables:
+    OPAM_PINS: "coq version 8.20.1   dune version 3.15.2"
+    MAKE_TARGET: "dune"
+
+# The oldest version runs in MRs, without name mangling.
+build-coq.8.19.2:
+  <<: *template
+  <<: *branches_and_mr
+  variables:
+    OPAM_PINS: "coq version 8.19.2"
+
+trigger-stdpp.dev:
+  <<: *template
+  variables:
+    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:
-  - master
-  - ci
-  - timing
+  - 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
+
+-->

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.  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

-# Process flags
-ifeq ($(Y), 1)
-	YFLAG=-y
-endif
+# Default target
+all: Makefile.coq
+	+@$(MAKE) -f Makefile.coq all
+.PHONY: all
 
-# Determine Coq version
-COQ_VERSION=$(shell coqc --version | egrep -o 'version 8.[0-9]' | egrep -o '8.[0-9]')
-COQ_MAKEFILE_FLAGS ?=
+# Build with dune.
+# This exists only for CI; you should just call `dune build` directly instead.
+dune:
+	@dune build --display=short
+.PHONY: dune
 
-ifeq ($(COQ_VERSION), 8.6)
-	COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-endif
+# Permit local customization
+-include Makefile.local
 
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
-	+@make -f Makefile.coq $@
-
-all: Makefile.coq
-	+@make -f Makefile.coq all
+	@#echo "Forwarding $@"
+	+@$(MAKE) -f Makefile.coq $@
+phony: ;
+.PHONY: phony
 
 clean: Makefile.coq
-	+@make -f Makefile.coq clean
-	find theories \( -name "*.v.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. POSIX awk can't do in-place editing, but coq_makefile wants the real filename, so we do some file gymnastics.
-Makefile.coq: _CoqProject Makefile awk.Makefile
-	coq_makefile $(COQ_MAKEFILE_FLAGS) -f _CoqProject -o Makefile.coq
-	mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
+# Create Coq Makefile.
+Makefile.coq: _CoqProject Makefile
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
 
 # Install build-dependencies
-build-dep:
-	build/opam-pins.sh < opam.pins
-	opam upgrade $(YFLAG) # it is not nice that we upgrade *all* packages here, but I found no nice way to upgrade only those that we pinned
-	opam pin add coq-iris "$$(pwd)#HEAD" -k git -n -y
-	opam install coq-iris --deps-only $(YFLAG)
-	opam pin remove coq-iris
-
-# Some files that do *not* need to be forwarded to Makefile.coq
-Makefile: ;
-_CoqProject: ;
-awk.Makefile: ;
-
-# Phony targets (i.e. targets that should be run no matter the timestamps of the involved files)
-phony: ;
-.PHONY: all clean phony
+OPAMFILES=$(wildcard *.opam)
+BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
+
+builddep/%-builddep.opam: %.opam Makefile
+	@echo "# Creating builddep package for $<."
+	@mkdir -p builddep
+	@sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
+
+builddep-opamfiles: $(BUILDDEPFILES)
+.PHONY: builddep-opamfiles
+
+builddep: builddep-opamfiles
+	@# We want opam to not just install the build-deps now, but to also keep satisfying these
+	@# constraints.  Otherwise, `opam upgrade` may well update some packages to versions
+	@# that are incompatible with our build requirements.
+	@# To achieve this, we create a fake opam package that has our build-dependencies as
+	@# dependencies, but does not actually install anything itself.
+	@echo "# Installing 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: 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:=$(shell find tests -name "*.v")
+NORMALIZER:=test-normalizer.sed
+
+test: $(TESTFILES:.v=.vo)
+.PHONY: test
+
+COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
+
+tests/.coqdeps.d: $(TESTFILES)
+	$(SHOW)'COQDEP TESTFILES'
+	$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
+-include tests/.coqdeps.d
+
+# 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" && \
+	  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" && \
+	  touch $@

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 always 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 "H"` : put `pm_trm` into the context as a new hypothesis
-  `H`.
-- `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 "H"` : turns `H1 : P1` and `H2 : P2` into
-  `H : P1 ★ P2`.
-
-Modalities
-----------
-
-- `iModIntro` : introduction of a modality that is an instance of the
-  `IntoModal` type class. Instances include: later, except 0, basic update and
-  fancy update.
-- `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.
-
-The later modality
-------------------
-
-- `iNext n` : introduce `n` laters by stripping that number of laters from all
-  hypotheses. If the argument `n` is not given, it strips one later if the
-  leftmost conjuct is of the shape `▷ P`, or `n` laters if the leftmost conjuct
-  is of the shape `▷^n P`.
-- `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.
-
-Induction
----------
-
-- `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
----------
-
-- `iRewrite pm_trm` : rewrite an equality in the conclusion.
-- `iRewrite pm_trm in "H"` : rewrite an equality in the hypothesis `H`.
-
-Iris
-----
-
-- `iInv N as (x1 ... xn) "ipat" "Hclose"` : open the invariant `N`, 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, always, 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.
-- `[ipat ipat]` : (separating) conjunction elimination.
-- `[ipat|ipat]` : disjunction elimination.
-- `[]` : false elimination.
-- `%` : move the hypothesis to the pure Coq context (anonymously).
-- `# 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:
-
-- `{H1 ... Hn}` : clear `H1 ... Hn`.
-- `{$H1 ... $Hn}` : frame `H1 ... Hn` (this pattern can be mixed with the
-  previous pattern, e.g., `{$H1 H2 $H3}`).
-- `!%` : introduce a pure goal (and leave the proof mode).
-- `!#` : introduce an always modality (given that the spatial context is empty).
-- `!>` : introduce a modality.
-- `/=` : perform `simpl`.
-- `*` : 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]` : generate a goal with the (spatial) hypotheses `H1 ... Hn` and
-  all persistent hypotheses. The spatial hypotheses among `H1 ... Hn` will be
-  consumed. Hypotheses may be prefixed with a `$`, which results in them being
-  framed in the generated goal.
-- `[-H1 ... Hn]`  : negated form of the above pattern.
-- `>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
-  is a modality, in which case the modality will be kept in the generated goal
-  for the premise will be wrapped into the modality.
-- `>[-H1 ... Hn]`  : negated form of the above pattern.
-- `>` : shorthand for `>[-]` (typically used for the last premise of an applied
-  lemma).
-- `[#]` : This pattern can be used when eliminating `P -★ Q` with `P`
-  persistent. Using this pattern, all hypotheses are available in the goal for
-  `P`, as well the remaining goal.
-- `[%]` : This pattern can be used when eliminating `P -★ Q` when `P` is pure.
-  It will generate a Coq goal for `P` and does not consume any hypotheses.
-
-For example, given:
-
-        H : □ P -★ P 2 -★ x = 0 -★ Q1 ∗ Q2
-
-You 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
+# Iris Coq Development [[coqdoc]](https://plv.mpi-sws.org/coqdoc/iris/)
 
-This is the Coq development of the [Iris Project](http://iris-project.org).
+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
+for carrying out separation logic proofs in Coq.
 
-## Prerequisites
+For using the Coq library, check out the
+[API documentation](https://plv.mpi-sws.org/coqdoc/iris/).
+
+For understanding the theory of Iris, a LaTeX version of the core logic
+definitions and some derived forms is available in
+[tex/iris.tex](tex/iris.tex).  A compiled PDF version of this document is
+[available online](http://plv.mpi-sws.org/iris/appendix-3.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
+
+### Prerequisites
 
 This version is known to compile with:
 
- - Coq 8.6
- - Ssreflect 1.6.1
+ - Coq 8.19.2 / 8.20.1
+ - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
+
+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.
 
-The easiest way to install the correct versions of the dependencies is
-through opam. Coq packages are available on the coq-released repository,
-set up by the command:
+### Working *with* Iris
+
+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:
 
     opam repo add coq-released https://coq.inria.fr/opam/released
 
-Once you got opam set up, just run `make build-dep` to install the right
-versions of the dependencies.  When the dependencies change, just run `make
-build-dep` again.
-
-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).
-
-## Building Instructions
-
-Run `make` to build the full development.
-
-## Structure
-
-* The folder [prelude](theories/prelude) contains an extended "Standard Library"
-  by [Robbert Krebbers](http://robbertkrebbers.nl/thesis.html).
-* 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 [proofmode](theories/proofmode) contains the Iris proof mode, which
-  extends Coq with contexts for persistent and spatial Iris assertions. It also
-  contains tactics for interactive proofs in Iris. 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
+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 install Iris:
+- `opam install coq-iris` will install the libraries making up the Iris logic,
+  but leave it up to you to instantiate the `program_logic.language` interface
+  to define a programming language for Iris to reason about.
+- `opam install coq-iris-heap-lang` will additionally install HeapLang, the
+  default language used by various Iris projects.
+
+To fetch updates later, run `opam update && opam upgrade`.
+
+#### Be notified of breaking changes
+
+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
+
+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
+
+See the [contribution guide](CONTRIBUTING.md) for information on how to work on
+the Iris development itself.
+
+## Directory Structure
+
+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.
-    Most notable here is [lib/barrier](theories/heap_lang/lib/barrier), the
-    implementation and proof of a barrier as described in
-    <http://doi.acm.org/10.1145/2818638>.
-* 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.
-
-## Documentation
-
-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.0.pdf).
+    For more examples of using Iris and heap_lang, have a look at the
+    [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/iris/examples) is where we
+  collect miscellaneous case studies that do not have their own repository.
+* [LambdaRust](https://gitlab.mpi-sws.org/iris/lambda-rust) is a Coq
+  formalization of the core Rust type system.
+* [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](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
-theories/prelude/option.v
-theories/prelude/fin_map_dom.v
-theories/prelude/bset.v
-theories/prelude/fin_maps.v
-theories/prelude/vector.v
-theories/prelude/pmap.v
-theories/prelude/stringmap.v
-theories/prelude/fin_collections.v
-theories/prelude/mapset.v
-theories/prelude/proof_irrel.v
-theories/prelude/hashset.v
-theories/prelude/pretty.v
-theories/prelude/countable.v
-theories/prelude/orders.v
-theories/prelude/natmap.v
-theories/prelude/strings.v
-theories/prelude/relations.v
-theories/prelude/collections.v
-theories/prelude/listset.v
-theories/prelude/streams.v
-theories/prelude/gmap.v
-theories/prelude/gmultiset.v
-theories/prelude/base.v
-theories/prelude/tactics.v
-theories/prelude/prelude.v
-theories/prelude/listset_nodup.v
-theories/prelude/finite.v
-theories/prelude/numbers.v
-theories/prelude/nmap.v
-theories/prelude/zmap.v
-theories/prelude/coPset.v
-theories/prelude/lexico.v
-theories/prelude/set.v
-theories/prelude/decidable.v
-theories/prelude/list.v
-theories/prelude/functions.v
-theories/prelude/hlist.v
-theories/prelude/sorting.v
-theories/algebra/cmra.v
-theories/algebra/cmra_big_op.v
-theories/algebra/cmra_tactics.v
-theories/algebra/sts.v
-theories/algebra/auth.v
-theories/algebra/gmap.v
-theories/algebra/ofe.v
-theories/algebra/base.v
-theories/algebra/dra.v
-theories/algebra/cofe_solver.v
-theories/algebra/agree.v
-theories/algebra/excl.v
-theories/algebra/iprod.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/coPset.v
-theories/algebra/deprecated.v
-theories/base_logic/upred.v
-theories/base_logic/primitive.v
-theories/base_logic/derived.v
-theories/base_logic/base_logic.v
-theories/base_logic/tactics.v
-theories/base_logic/big_op.v
-theories/base_logic/hlist.v
-theories/base_logic/soundness.v
-theories/base_logic/double_negation.v
-theories/base_logic/deprecated.v
-theories/base_logic/lib/iprop.v
-theories/base_logic/lib/own.v
-theories/base_logic/lib/saved_prop.v
-theories/base_logic/lib/namespaces.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/counter_examples.v
-theories/base_logic/lib/fractional.v
-theories/base_logic/lib/gen_heap.v
-theories/base_logic/lib/core.v
-theories/program_logic/adequacy.v
-theories/program_logic/lifting.v
-theories/program_logic/weakestpre.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/heap_lang/lang.v
-theories/heap_lang/tactics.v
-theories/heap_lang/lifting.v
-theories/heap_lang/notation.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/counter.v
-theories/heap_lang/lib/barrier/barrier.v
-theories/heap_lang/lib/barrier/specification.v
-theories/heap_lang/lib/barrier/protocol.v
-theories/heap_lang/lib/barrier/proof.v
-theories/heap_lang/proofmode.v
-theories/heap_lang/adequacy.v
-theories/tests/heap_lang.v
-theories/tests/one_shot.v
-theories/tests/joining_existentials.v
-theories/tests/proofmode.v
-theories/tests/barrier_client.v
-theories/tests/list_reverse.v
-theories/tests/tree_sum.v
-theories/tests/ipm_paper.v
-theories/proofmode/strings.v
-theories/proofmode/coq_tactics.v
-theories/proofmode/environments.v
-theories/proofmode/intro_patterns.v
-theories/proofmode/spec_patterns.v
-theories/proofmode/sel_patterns.v
-theories/proofmode/tactics.v
-theories/proofmode/notation.v
-theories/proofmode/classes.v
-theories/proofmode/class_instances.v
+# 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/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

awk.Makefile

-# awk program that patches the Makefile generated by Coq.
-
-# Detect the name this project will be installed under.
-/\$\(COQLIBINSTALL\)\/.*\/\$\$i/ {
-# Wow, POSIX awk is really broken.  I mean, isn't it supposed to be a text processing language?
-# And there is not even a way to access the matched groups of a regexp...?!? Lucky enough,
-# we can just split the string at '/' here.
-	split($0, PIECES, /\//);
-	PROJECT=PIECES[2];
-}
-
-# Patch the uninstall target to work properly, and to also uninstall stale files.
-# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
-/^uninstall:/ {
-	print "uninstall:";
-	print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
-	getline;
-	next
-}
-
-# Patch vio2vo to (a) run "make quick" with the same number of jobs, ensuring
-# that the .vio files are up-to-date, and (b) only schedule vio2vo for those
-# files where the .vo is *older* than the .vio.
-/^vio2vo:/ {
-	print "vio2vo:";
-	print "\t@make -j $(J) quick"
-	print "\t@VIOFILES=$$(for file in $(VOFILES:%.vo=%.vio); do vofile=\"$$(echo \"$$file\" | sed \"s/\\.vio/.vo/\")\"; if [ \"$$vofile\" -ot \"$$file\" -o ! -e \"$$vofile\" ]; then echo -n \"$$file \"; fi; done); \\"
-	print "\t echo \"VIO2VO: $$VIOFILES\"; \\"
-	print "\t if [ -n \"$$VIOFILES\" ]; then $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
-	getline;
-	next
-}
-
-# This forwards all unchanged lines
-1

benchmark/.gitignore

-__pycache__
-build-times.log*
-gitlab-extract

benchmark/gitlab-extract.py

-#!/usr/bin/env python3
-import argparse, pprint, sys
-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)
-    return requests.get(url, headers={'PRIVATE-TOKEN': args.private_token})
-
-# 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.")
-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 = False))
-    args.commits = "{}..origin/master".format(last_result.commit)
-
-projects = req("projects")
-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
-    print("Fetching {}...".format(commit))
-    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
-    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
-            break
-        if build['status'] != 'success':
-            # build failed or cancelled, skip to next
-            continue
-        # now fetch the build times
-        build_times = requests.get("{}/builds/{}/artifacts/file/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 one
-        break

benchmark/parse_log.py

-import re, subprocess
-
-class Result:
-    def __init__(self, commit, times):
-        self.commit = commit
-        self.times = times
-
-def parse(file, parse_times = True):
-    '''[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_/-]+) \(user: ([0-9.]+) mem: ([0-9]+) ko\)$")
-    commit = None
-    times = None
-    for line in file:
-        # 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:
-                times = {} # reset the recorded times
-            continue
-        # next file time?
-        m = time_re.match(line)
-        if m is not None:
-            if times is not None:
-                name = m.group(1)
-                time = float(m.group(2))
-                times[name] = time
-            continue
-        # nothing else we know about, ignore
-    # 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])
-    return reversed(commits.decode("utf-8").strip().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 = True)
-if args.commits:
-    commits = set(parse_log.parse_git_commits(args.commits))
-    results = filter(lambda r: r.commit in commits, results)
-results = list(results)
-
-timings = list(map(lambda t: t[:-2] if t.endswith(".v") else t, args.timings))
-for timing in timings:
-    plt.plot(list(map(lambda r: r.times.get(timing), results)), marker=next(markers), markersize=8)
-plt.legend(timings, loc = 'upper left', bbox_to_anchor=(1.05, 1.0))
-plt.xticks(range(len(results)), list(map(lambda r: r.commit[:7], results)), rotation=70)
-plt.subplots_adjust(bottom=0.2, right=0.7) # more space for the commit labels and legend
-
-plt.xlabel('Commit')
-plt.ylabel('Time (s)')
-plt.title('Time to compile files')
-plt.grid(True)
-plt.show()

build/opam-ci.sh

-#!/bin/bash
-set -e
-# This script installs the build dependencies for CI builds.
-
-# Prepare OPAM configuration
-export OPAMROOT="$(pwd)/opamroot"
-export OPAMJOBS=16
-export OPAM_EDITOR="$(which false)"
-
-# Make sure we got a good OPAM
-test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
-eval `opam conf env`
-test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 5
-test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
-test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.inria.fr/opam/released -p 10
-opam update
-
-# Install fixed versions of some dependencies
-echo
-while (( "$#" )); do # while there are arguments left
-    PACKAGE="$1" ; shift
-    VERSION="$1" ; shift
-    # Check if the pin is already set
-    if opam pin list | fgrep "$PACKAGE.$VERSION " > /dev/null; then
-        echo "[opam-ci] $PACKAGE already pinned to $VERSION"
-    else
-        echo "[opam-ci] Pinning $PACKAGE to $VERSION"
-        opam pin add "$PACKAGE" "$VERSION" -k version -y
-    fi
-done
-
-# Install build-dependencies
-echo
-make build-dep Y=1
-
-# done
-echo
-coqc -v