.gitattributes

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

.gitignore

@@ -22,3 +22,6 @@ Makefile.coq.conf
 .Makefile.coq.d
 Makefile.package.*
 .Makefile.package.*
+_opam
+_build
+*.install

.gitlab-ci.yml

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

.gitmodules

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

CONTRIBUTING.md

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

Makefile

@@ -3,6 +3,12 @@ all: Makefile.coq
 	+@$(MAKE) -f Makefile.coq all
 .PHONY: all
 
+# Build with dune.
+# This exists only for CI; you should just call `dune build` directly instead.
+dune:
+	@dune build --display=short
+.PHONY: dune
+
 # Permit local customization
 -include Makefile.local
 

Makefile.coq.local

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

ProofMode.md

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

README.md

-# IRIS COQ DEVELOPMENT [[coqdoc]](https://plv.mpi-sws.org/coqdoc/iris/)
+# Iris Coq Development [[coqdoc]](https://plv.mpi-sws.org/coqdoc/iris/)
 
 This is the Coq development of the [Iris Project](http://iris-project.org),
 which includes [MoSeL](http://iris-project.org/mosel/), a general proof mode
@@ -10,7 +10,7 @@ For using the Coq library, check out the
 For understanding the theory of Iris, a LaTeX version of the core logic
 definitions and some derived forms is available in
 [tex/iris.tex](tex/iris.tex).  A compiled PDF version of this document is
-[available online](http://plv.mpi-sws.org/iris/appendix-3.2.pdf).
+[available online](http://plv.mpi-sws.org/iris/appendix-3.4.pdf).
 
 ## Side-effects
 
@@ -30,13 +30,15 @@ Importing Iris has some side effects as the library sets some global options.
 
 This version is known to compile with:
 
- - Coq 8.10.2 / 8.11.2 / 8.12.1
+ - Coq 8.19.2 / 8.20.1
  - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
 
-If you need to work with Coq 8.7 or Coq 8.8, please check out the
-[iris-3.2 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.2).
-For Coq 8.9, you can use the
-[iris-3.3 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.3).
+Generally we always aim to support the last two stable Coq releases. Support for
+older versions will be dropped when it is convenient.
+
+If you need to work with older versions of Coq, you can check out the
+[tags](https://gitlab.mpi-sws.org/iris/iris/-/tags) for old Iris releases that
+still support them.
 
 ### Working *with* Iris
 
@@ -65,7 +67,8 @@ 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.
+notification group.  Note that this excludes the "unstable" and "deprecated"
+packages (see below).
 
 #### Use of Iris in submitted artifacts
 
@@ -85,39 +88,60 @@ the Iris development itself.
 
 ## Directory Structure
 
-* 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 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 [bi](iris/bi) contains the BI++ laws, as well as derived
-  connectives, laws and constructions that are applicable for general BIS.
-* 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 [heap_lang](iris_heap_lang) defines the ML-like concurrent heap
-  language
-  * The subfolder [lib](iris_heap_lang/lib) contains a few derived
+Iris is structured into multiple *packages*, some of which contain multiple
+modules in separate folders.
+
+* The [iris](iris) package contains the language-independent parts of Iris.
+  + The folder [prelude](iris/prelude) contains modules imported everywhere in
+    Iris.
+  + The folder [algebra](iris/algebra) contains the COFE and CMRA
+    constructions as well as the solver for recursive domain equations.
+    - The subfolder [lib](iris/algebra/lib) contains some general derived RA
+      constructions.
+  + The folder [bi](iris/bi) contains the BI++ laws, as well as derived
+    connectives, laws and constructions that are applicable for general BIs.
+    - The subfolder [lib](iris/bi/lib) contains some general derived logical
+      constructions.
+  + The folder [proofmode](iris/proofmode) contains
+    [MoSeL](http://iris-project.org/mosel/), which extends Coq with contexts for
+    intuitionistic and spatial BI++ assertions. It also contains tactics for
+    interactive proofs. Documentation can be found in
+    [proof_mode.md](docs/proof_mode.md).
+  + The folder [base_logic](iris/base_logic) defines the Iris base logic and
+    the primitive connectives.  It also contains derived constructions that are
+    entirely independent of the choice of resources.
+    - The subfolder [lib](iris/base_logic/lib) contains some generally useful
+      derived constructions.  Most importantly, it defines composable
+      dynamic resources and ownership of them; the other constructions depend
+      on this setup.
+  + The folder [program_logic](iris/program_logic) specializes the base logic
+    to build Iris, the program logic.   This includes weakest preconditions that
+    are defined for any language satisfying some generic axioms, and some derived
+    constructions that work for any such language.
+  + The folder [si_logic](iris/si_logic) defines a "plain" step-indexed logic
+    and shows that it is an instance of the BI interface.
+* The [iris_heap_lang](iris_heap_lang) package defines the ML-like concurrent
+  language HeapLang and provides tactic support and proof mode integration.
+  + The subfolder [lib](iris_heap_lang/lib) contains a few derived
     constructions within this language, e.g., parallel composition.
     For more examples of using Iris and heap_lang, have a look at the
     [Iris Examples](https://gitlab.mpi-sws.org/iris/examples).
+* The [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. Users of the Iris Coq library should *not* depend on these
-  modules; they may change or disappear without any notice.
-* The folder [si_logic](iris/si_logic) defines a "plain" step-indexed logic
-  and shows that it is an instance of the BI interface.
+  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
 
@@ -141,6 +165,7 @@ that should be compatible with this version:
 
 Getting along with Iris in Coq:
 
+* The coding style is documented in the [style guide](docs/style_guide.md).
 * Iris proof patterns and conventions are documented in the
   [proof guide](docs/proof_guide.md).
 * Various notions of equality and logical entailment in Iris and their Coq
@@ -153,16 +178,13 @@ Getting along with Iris in Coq:
 
 Contacting the developers:
 
-* Discussion about the Iris Coq development happens on the mailing list
-  [iris-club@lists.mpi-sws.org](https://lists.mpi-sws.org/listinfo/iris-club)
-  and in the [Iris Chat](https://mattermost.mpi-sws.org/iris).  This is also the
-  right place to ask questions.  The chat requires an account at the
-  [MPI-SWS GitLab](https://gitlab.mpi-sws.org/users/sign_in) (use the "Register"
-  tab). If you have trouble joining the chat, please contact
-  [Ralf](https://gitlab.mpi-sws.org/jung).
+* Discussion about the Iris Coq development happens in the [Iris
+  Chat](https://iris-project.org/chat.html). This is also the right place to ask
+  questions.
 * If you want to report a bug, please use the
-  [issue tracker](https://gitlab.mpi-sws.org/iris/iris/issues), which also
-  requires an MPI-SWS GitLab account.
+  [issue tracker](https://gitlab.mpi-sws.org/iris/iris/issues), which requires
+  an MPI-SWS GitLab account. The [chat page](https://iris-project.org/chat.html)
+  describes how to create such an account.
 * To contribute to Iris itself, see the [contribution guide](CONTRIBUTING.md).
 
 Miscellaneous:

_CoqProject

@@ -8,14 +8,25 @@
 -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
@@ -26,7 +37,6 @@ iris/algebra/view.v
 iris/algebra/auth.v
 iris/algebra/gmap.v
 iris/algebra/ofe.v
-iris/algebra/dra.v
 iris/algebra/cofe_solver.v
 iris/algebra/agree.v
 iris/algebra/excl.v
@@ -43,19 +53,25 @@ iris/algebra/gmultiset.v
 iris/algebra/coPset.v
 iris/algebra/proofmode_classes.v
 iris/algebra/ufrac.v
-iris/algebra/namespace_map.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/frac_agree.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
@@ -68,8 +84,10 @@ 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.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
@@ -88,9 +106,6 @@ 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/viewshifts.v
-iris/base_logic/lib/auth.v
-iris/base_logic/lib/sts.v
 iris/base_logic/lib/boxes.v
 iris/base_logic/lib/na_invariants.v
 iris/base_logic/lib/cancelable_invariants.v
@@ -101,12 +116,14 @@ 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/hoare.v
 iris/program_logic/language.v
 iris/program_logic/ectx_language.v
 iris/program_logic/ectxi_language.v
@@ -117,6 +134,7 @@ 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
@@ -128,19 +146,24 @@ 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/frame_instances.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
@@ -154,8 +177,10 @@ 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
@@ -165,3 +190,14 @@ 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'))

benchmark/visualize.py

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

build-all

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

coq-iris-deprecated.opam

+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+version: "dev"
+
+synopsis: "Deprecated Iris libraries"
+description: """
+This package contains libraries that have been deprecated from Iris, and are planned to be
+entirely removed at some point.
+"""
+
+depends: [
+  "coq-iris" {= version}
+]
+
+build: ["./make-package" "iris_deprecated" "-j%{jobs}%"]
+install: ["./make-package" "iris_deprecated" "install"]

coq-iris-heap-lang.opam

@@ -5,11 +5,16 @@ license: "BSD-3-Clause"
 homepage: "https://iris-project.org/"
 bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+version: "dev"
 
-synopsis: "HeapLang is the canonical example language for Iris"
+synopsis: "The canonical example language for Iris"
 description: """
-This package provides the iris.heap_lang Coq module.
+This package defines HeapLang, a concurrent lambda calculus with references, and
+uses Iris to build a program logic for HeapLang programs.
 """
+tags: [
+  "logpath:iris.heap_lang"
+]
 
 depends: [
   "coq-iris" {= version}

coq-iris-unstable.opam

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