.gitignore

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

.gitlab-ci.yml

@@ -6,6 +6,8 @@ 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:
@@ -42,10 +44,11 @@ variables:
 
 ## Build jobs
 
-build-coq.8.15.1:
+# The newest version runs with timing.
+build-coq.8.20.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.15.1"
+    OPAM_PINS: "coq version 8.20.1"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
     OPAM_PKG: "1"
@@ -55,42 +58,35 @@ build-coq.8.15.1:
   - fp-timing
   interruptible: false
 
-build-coq.8.14.1:
+# The newest version also runs in MRs, without timing.
+build-coq.8.20.1-mr:
   <<: *template
-  <<: *branches_and_mr
+  <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.14.1"
-    MANGLE_NAMES: "1"
+    OPAM_PINS: "coq version 8.20.1"
     DENY_WARNINGS: "1"
-    OCAML: "ocaml-base-compiler.4.07.1"
+    MANGLE_NAMES: "1"
 
-build-coq.8.13.2:
+# Also ensure Dune works.
+build-coq.8.20.1-dune:
   <<: *template
   <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.13.2"
-    DENY_WARNINGS: "1"
-    OCAML: "ocaml-base-compiler.4.07.1"
+    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++)
-trigger-stdpp.dev-coq.8.15.1:
+# The oldest version runs in MRs, without name mangling.
+build-coq.8.19.2:
   <<: *template
+  <<: *branches_and_mr
   variables:
-    STDPP_REPO: "iris/stdpp"
-    OPAM_PINS: "coq version 8.15.1   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV"
-  except:
-  only:
-  - triggers
-  - schedules
-  - api
+    OPAM_PINS: "coq version 8.19.2"
 
-# Nightly job with latest Coq branch
-trigger-stdpp.dev-coq.dev:
+trigger-stdpp.dev:
   <<: *template
   variables:
     STDPP_REPO: "iris/stdpp"
-    OPAM_PINS: "coq version dev   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV"
+    OPAM_PINS: "coq version $NIGHTLY_COQ   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV"
     CI_COQCHK: "1"
   except:
   only:

CONTRIBUTING.md

@@ -42,6 +42,9 @@ 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.

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,18 +4,23 @@ 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 all Instance/Argument/Hint are qualified.
+# Make sure everything imports the options, and some general linting.
 	$(SHOW)"COQLINT"
 	$(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 ; \
+	  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 egrep '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
+	$(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
@@ -26,8 +31,6 @@ test: $(TESTFILES:.v=.vo)
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
-COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
@@ -43,17 +46,16 @@ tests/.coqdeps.d: $(TESTFILES)
 # - 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 --strip-trailing-cr -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
@@ -30,9 +30,12 @@ Importing Iris has some side effects as the library sets some global options.
 
 This version is known to compile with:
 
- - Coq 8.13.2 / 8.14.1 / 8.15.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.
@@ -64,7 +67,7 @@ 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 "staging" and "deprecated"
+notification group.  Note that this excludes the "unstable" and "deprecated"
 packages (see below).
 
 #### Use of Iris in submitted artifacts
@@ -123,7 +126,7 @@ modules in separate folders.
     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_staging](iris_staging) package contains libraries that are not yet
+* 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
@@ -137,6 +140,9 @@ modules in separate folders.
   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
@@ -159,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
@@ -171,10 +178,9 @@ 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://iris-project.org/chat.html).  This is also the
-  right place to ask questions.
+* 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)

_CoqProject

@@ -10,16 +10,23 @@
 -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
-# Fixing this one requires Coq 8.15.
--arg -w -arg -deprecated-typeclasses-transparency-without-locality
+# 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
@@ -49,12 +56,14 @@ 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
@@ -75,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
@@ -107,6 +118,7 @@ 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
@@ -134,13 +146,15 @@ 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
@@ -163,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
@@ -180,7 +196,6 @@ 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_unstable/algebra/monotone.v
 
 iris_deprecated/base_logic/auth.v
 iris_deprecated/base_logic/sts.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()

coq-iris.opam

@@ -27,8 +27,8 @@ tags: [
 ]
 
 depends: [
-  "coq" { (>= "8.13" & < "8.16~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2022-08-03.0.b99e79cf") | (= "dev") }
+  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
+  "coq-stdpp" { (= "dev.2025-02-26.0.d2e8771d") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]

coq-lint.sh

@@ -4,7 +4,7 @@ set -e
 
 FILE="$1"
 
-if egrep -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope|Opaque|Transparent)\b' "$FILE"; then
+if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold|Rewrite)|(Open|Close)\s+Scope|Opaque|Transparent|Typeclasses (Opaque|Transparent))\b' "$FILE"; then
     echo "ERROR: $FILE contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
     echo "Please add 'Global' or 'Local' as appropriate."
     echo

docs/dune.md

+Support for the dune build system
+=================================
+
+**NOTE:** in case of problem with the dune build, you can ask @lepigre or
+@Blaisorblade for help.
+
+The library can be built using dune by running `dune build`. Note that `dune`
+needs to be installed separately with `opam install dune`, as it is currently
+not part of the dependencies of the project.
+
+Useful links:
+- [dune documentation](https://dune.readthedocs.io)
+- [coq zulip channel](https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users)
+
+
+Editor support
+--------------
+
+Good dune support in editors is lacking at the moment, but there are tricks you
+can play to make it work.
+
+One option is to configure your editor to invoke the `dune coq top` command
+instead of `coqtop`, but that is not easy to configure.
+
+Another option is to change the `_CoqProject` file to something like:
+```
+-Q iris iris
+-Q _build/default/iris iris
+-Q iris_heap_lang iris.heap_lang
+-Q _build/default/iris_heap_lang iris.heap_lang
+-Q iris_unstable iris.unstable
+-Q _build/default/iris_unstable iris.unstable
+-Q iris_deprecated iris.deprecated
+-Q _build/default/iris_deprecated iris.deprecated
+```
+Note that this includes two bindings for each logical path: a binding to a
+folder in the source tree (where editors will find the `.v` files), and a
+binding to the same folder under `_build/default` (where editors will find
+the corresponding `.vo` files). The binding for a source folder must come
+before the binding for the corresponding build folder, so that editors know
+to jump to source files in the source tree (and not their read-only copy in
+the build folder).
+
+If you do this, you still need to invoke `dune` manually to make sure that the
+dependencies of the file you are stepping through are up-to-date. To build a
+single file, you can do, e.g., `dune build iris/prelude/options.vo`. To build
+only the `iris` folder, you can do `dune build iris`.

docs/editor.md

@@ -5,7 +5,7 @@ If you really want to, you can also avoid having to type unicode characters by
 importing `iris.bi.ascii`.  That enables parsing-only ASCII alternatives to many
 unicode notations. (Feel free to report an issue when you notice that a notation
 is missing.)  The easiest way to learn the ASCII syntax is to
-[read this file](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/bi/ascii.v).
+[read this file](../iris/bi/ascii.v).
 Note however that this will make your code harder to read and work on for Iris
 developers that are used to our default unicode notation---generally, our
 recommendation is to use the unicode syntax whenever possible. In particular,
@@ -96,12 +96,12 @@ on the math symbol list, and with some custom aliases for symbols used a lot in
 (mapc (lambda (x)
         (if (cddr x)
             (quail-defrule (cadr x) (car (cddr x)))))
-      (append math-symbol-list-basic math-symbol-list-extended))
+      ; need to reverse since different emacs packages disagree on whether
+      ; the first or last entry should take priority...
+      ; see <https://mattermost.mpi-sws.org/iris/pl/46onxnb3tb8ndg8b6h1z1f7tny> for discussion
+      (reverse (append math-symbol-list-basic math-symbol-list-extended)))
 ```
 
-Finally, set your default input method with `M-x customize-set-value`, setting
-`default-input-method` to `math`.
-
 ### Font Configuration
 
 Even when usable fonts are installed, Emacs tends to pick bad fonts for some
@@ -183,134 +183,7 @@ On Linux with old versions of CoqIDE you can use the Intelligent
 Input Bus (IBus) framework to input Unicode symbols. First, install `ibus-m17n`
 via your system's package manager. Next, create a file `~/.m17n.d/coq.mim` to
 configure an input method based on the math symbol list, and with some custom
-aliases for symbols used a lot in Iris:
-
-```
-;; Usage: copy to ~/.m17n.d/coq.mim
-
-(input-method t coq)
-(description "Input method for Coq")
-(title "Coq")
-
-(map (trans
-
-;; Standard LaTeX math notations
-  ("\\forall"         "∀")
-  ("\\exists"         "∃")
-  ("\\lam"            "λ")
-  ("\\not"            "¬")
-  ("\\/"              "∨")
-  ("/\\"              "∧")
-  ("->"               "→")
-  ("<->"              "↔")
-  ("\\<-"             "←") ;; we add a backslash because the plain <- is used for the rewrite tactic
-  ("\\=="             "≡")
-  ("\\/=="            "≢")
-  ("/="               "≠")
-  ("<="               "≤")
-  ("\\in"             "∈")
-  ("\\notin"          "∉")
-  ("\\cup"            "∪")
-  ("\\cap"            "∩")
-  ("\\setminus"       "∖")
-  ("\\subset"         "⊂")
-  ("\\subseteq"       "⊆")
-  ("\\sqsubseteq"     "⊑")
-  ("\\sqsubseteq"     "⊑")
-  ("\\notsubseteq"    "⊈")
-  ("\\meet"           "⊓")
-  ("\\join"           "⊔")
-  ("\\top"            "⊤")
-  ("\\bottom"         "⊥")
-  ("\\vdash"          "⊢")
-  ("\\dashv"          "⊣")
-  ("\\Vdash"          "⊨")
-  ("\\infty"          "∞")
-  ("\\comp"           "∘")
-  ("\\prf"            "↾")
-  ("\\bind"           "≫=")
-  ("\\mapsto"         "↦")
-  ("\\hookrightarrow" "↪")
-  ("\\uparrow"        "↑")
-
-;; Iris specific
-  ("\\fun"            "λ")
-  ("\\mult"           "⋅")
-  ("\\ent"            "⊢")
-  ("\\valid"          "✓")
-  ("\\diamond"        "◇")
-  ("\\box"            "□")
-  ("\\bbox"           "■")
-  ("\\later"          "▷")
-  ("\\pred"           "φ")
-  ("\\and"            "∧")
-  ("\\or"             "∨")
-  ("\\comp"           "∘")
-  ("\\ccomp"          "◎")
-  ("\\all"            "∀")
-  ("\\ex"             "∃")
-  ("\\to"             "→")
-  ("\\sep"            "∗")
-  ("\\lc"             "⌜")
-  ("\\rc"             "⌝")
-  ("\\Lc"             "⎡")
-  ("\\Rc"             "⎤")
-  ("\\empty"          "∅")
-  ("\\Lam"            "Λ")
-  ("\\Sig"            "Σ")
-  ("\\-"              "∖")
-  ("\\aa"             "●")
-  ("\\af"             "◯")
-  ("\\auth"           "●")
-  ("\\frag"           "◯")
-  ("\\iff"            "↔")
-  ("\\gname"          "γ")
-  ("\\incl"           "≼")
-  ("\\latert"         "▶")
-  ("\\update"         "⇝")
-  ("\\bind"           "≫=")
-
-;; accents (for iLöb)
-  ("\\\"o" "ö")
-
-;; subscripts and superscripts
-  ("^^+" "⁺") ("__+" "₊") ("^^-" "⁻")
-  ("__0" "₀") ("__1" "₁") ("__2" "₂") ("__3" "₃") ("__4" "₄")
-  ("__5" "₅") ("__6" "₆") ("__7" "₇") ("__8" "₈") ("__9" "₉")
-
-  ("__a" "ₐ") ("__e" "ₑ") ("__h" "ₕ") ("__i" "ᵢ") ("__k" "ₖ")
-  ("__l" "ₗ") ("__m" "ₘ") ("__n" "ₙ") ("__o" "ₒ") ("__p" "ₚ")
-  ("__r" "ᵣ") ("__s" "ₛ") ("__t" "ₜ") ("__u" "ᵤ") ("__v" "ᵥ") ("__x" "ₓ")
-
-;; Greek alphabet
-  ("\\Alpha"  "Α")   ("\\alpha"  "α")
-  ("\\Beta"   "Β")   ("\\beta"   "β")
-  ("\\Gamma"  "Γ")   ("\\gamma"  "γ")
-  ("\\Delta"  "Δ")   ("\\delta"  "δ")
-  ("\\Epsilon"  "Ε") ("\\epsilon"  "ε")
-  ("\\Zeta"   "Ζ")   ("\\zeta"   "ζ")
-  ("\\Eta"  "Η")     ("\\eta"  "η")
-  ("\\Theta"  "Θ")   ("\\theta"  "θ")
-  ("\\Iota"   "Ι")   ("\\iota"   "ι")
-  ("\\Kappa"  "Κ")   ("\\kappa"  "κ")
-  ("\\Lamda"  "Λ")   ("\\lamda"  "λ")
-  ("\\Lambda"   "Λ") ("\\lambda"   "λ")
-  ("\\Mu"   "Μ")     ("\\mu"   "μ")
-  ("\\Nu"   "Ν")     ("\\nu"   "ν")
-  ("\\Xi"   "Ξ")     ("\\xi"   "ξ")
-  ("\\Omicron"  "Ο") ("\\omicron"  "ο")
-  ("\\Pi"   "Π")     ("\\pi"   "π")
-  ("\\Rho"  "Ρ")     ("\\rho"  "ρ")
-  ("\\Sigma"  "Σ")   ("\\sigma"  "σ")
-  ("\\Tau"  "Τ")     ("\\tau"  "τ")
-  ("\\Upsilon"  "Υ") ("\\upsilon"  "υ")
-  ("\\Phi"  "Φ")     ("\\phi"  "φ")
-  ("\\Chi"  "Χ")     ("\\chi"  "χ")
-  ("\\Psi"  "Ψ")     ("\\psi"  "ψ")
-  ("\\Omega"  "Ω")   ("\\omega"  "ω")
-))
-(state (init (trans)))
-```
+aliases for symbols used a lot in Iris as defined [here](ibus).
 
 To use this input method, you should:
 
@@ -435,189 +308,7 @@ extension](https://marketplace.visualstudio.com/items?itemName=mr-konn.generic-i
 To insert a symbol, type the code for a symbol such as `\to` and then press
 `Space` or `Tab`. To enable Iris unicode input support, open your user settings,
 press `Cmd ,` or `Ctrl ,`, type "generic-input-methods.input-methods", and then
-click on "Edit in settings.json" and add the following:
-
-```
-  "generic-input-methods.input-methods": [
-        {
-            "name": "Iris Math",
-            "commandName": "text.math",
-            "languages": [
-                "coq"
-            ],
-            "triggers": [
-                "\\"
-            ],
-            "dictionary": [
-                // Standard LaTeX math notations
-                { "label": "forall", "body": "∀", "description": "∀" },
-                { "label": "exists", "body": "∃", "description": "∃" },
-                { "label": "lam", "body": "λ", "description": "λ" },
-                { "label": "not", "body": "¬", "description": "¬" },
-                { "label": "->", "body": "→", "description": "→" },
-                { "label": "<->", "body": "↔", "description": "↔" },
-                { "label": "<-", "body": "←", "description": "←" },
-                { "label": "==", "body": "≡", "description": "≡" },
-                { "label": "/==", "body": "≢", "description": "≢" },
-                { "label": "/=", "body": "≠", "description": "≠" },
-                { "label": "neq", "body": "≠", "description": "≠" },
-                { "label": "nequiv", "body": "≢", "description": "≢" },
-                { "label": "<=", "body": "≤", "description": "≤" },
-                { "label": "leq", "body": "≤", "description": "≤" },
-                { "label": "in", "body": "∈", "description": "∈" },
-                { "label": "notin", "body": "∉", "description": "∉" },
-                { "label": "cup", "body": "∪", "description": "∪" },
-                { "label": "cap", "body": "∩", "description": "∩" },
-                { "label": "setminus", "body": "∖", "description": "∖" },
-                { "label": "subset", "body": "⊂", "description": "⊂" },
-                { "label": "subseteq", "body": "⊆", "description": "⊆" },
-                { "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
-                { "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
-                { "label": "notsubseteq", "body": "⊈", "description": "⊈" },
-                { "label": "meet", "body": "⊓", "description": "⊓" },
-                { "label": "join", "body": "⊔", "description": "⊔" },
-                { "label": "top", "body": "⊤", "description": "⊤" },
-                { "label": "bottom", "body": "⊥", "description": "⊥" },
-                { "label": "vdash", "body": "⊢", "description": "⊢" },
-                { "label": "|-", "body": "⊢", "description": "⊢" },
-                { "label": "dashv", "body": "⊣", "description": "⊣" },
-                { "label": "Vdash", "body": "⊨", "description": "⊨" },
-                { "label": "infty", "body": "∞", "description": "∞" },
-                { "label": "comp", "body": "∘", "description": "∘" },
-                { "label": "prf", "body": "↾", "description": "↾" },
-                { "label": "bind", "body": "≫=", "description": "≫=" },
-                { "label": "mapsto", "body": "↦", "description": "↦" },
-                { "label": "hookrightarrow", "body": "↪", "description": "↪" },
-                { "label": "uparrow", "body": "↑", "description": "↑" },
-
-                // Iris specific
-                { "label": "fun", "body": "λ", "description": "λ" },
-                { "label": "mult", "body": "⋅", "description": "⋅" },
-                { "label": "ent", "body": "⊢", "description": "⊢" },
-                { "label": "valid", "body": "✓", "description": "✓" },
-                { "label": "diamond", "body": "◇", "description": "◇" },
-                { "label": "box", "body": "□", "description": "□" },
-                { "label": "bbox", "body": "■", "description": "■" },
-                { "label": "later", "body": "▷", "description": "▷" },
-                { "label": "pred", "body": "φ", "description": "φ" },
-                { "label": "and", "body": "∧", "description": "∧" },
-                { "label": "or", "body": "∨", "description": "∨" },
-                { "label": "comp", "body": "∘", "description": "∘" },
-                { "label": "ccomp", "body": "◎", "description": "◎" },
-                { "label": "all", "body": "∀", "description": "∀" },
-                { "label": "ex", "body": "∃", "description": "∃" },
-                { "label": "to", "body": "→", "description": "→" },
-                { "label": "sep", "body": "∗", "description": "∗" },
-                { "label": "star", "body": "∗", "description": "∗" },
-                { "label": "lc", "body": "⌜", "description": "⌜" },
-                { "label": "rc", "body": "⌝", "description": "⌝" },
-                { "label": "Lc", "body": "⎡", "description": "⎡" },
-                { "label": "Rc", "body": "⎤", "description": "⎤" },
-                { "label": "empty", "body": "∅", "description": "∅" },
-                { "label": "Lam", "body": "Λ", "description": "Λ" },
-                { "label": "Sig", "body": "Σ", "description": "Σ" },
-                { "label": "-", "body": "∖", "description": "∖" },
-                { "label": "aa", "body": "●", "description": "●" },
-                { "label": "af", "body": "◯", "description": "◯" },
-                { "label": "auth", "body": "●", "description": "●" },
-                { "label": "frag", "body": "◯", "description": "◯" },
-                { "label": "iff", "body": "↔", "description": "↔" },
-                { "label": "gname", "body": "γ", "description": "γ" },
-                { "label": "incl", "body": "≼", "description": "≼" },
-                { "label": "latert", "body": "▶", "description": "▶" },
-                { "label": "update", "body": "⇝", "description": "⇝" },
-                { "label": "bind", "body": "≫=", "description": "≫=" },
-
-                // accents (for iLöb)
-                { "label": "\"o", "body": "ö", "description": "ö" },
-
-                // subscripts and superscripts
-                { "label": "^^+", "body": "⁺", "description": "⁺" },
-                { "label": "__+", "body": "₊", "description": "₊" },
-                { "label": "^^-", "body": "⁻", "description": "⁻" },
-                { "label": "__0", "body": "₀", "description": "₀" },
-                { "label": "__1", "body": "₁", "description": "₁" },
-                { "label": "__2", "body": "₂", "description": "₂" },
-                { "label": "__3", "body": "₃", "description": "₃" },
-                { "label": "__4", "body": "₄", "description": "₄" },
-                { "label": "__5", "body": "₅", "description": "₅" },
-                { "label": "__6", "body": "₆", "description": "₆" },
-                { "label": "__7", "body": "₇", "description": "₇" },
-                { "label": "__8", "body": "₈", "description": "₈" },
-                { "label": "__9", "body": "₉", "description": "₉" },
-                { "label": "__a", "body": "ₐ", "description": "ₐ" },
-                { "label": "__e", "body": "ₑ", "description": "ₑ" },
-                { "label": "__h", "body": "ₕ", "description": "ₕ" },
-                { "label": "__i", "body": "ᵢ", "description": "ᵢ" },
-                { "label": "__k", "body": "ₖ", "description": "ₖ" },
-                { "label": "__l", "body": "ₗ", "description": "ₗ" },
-                { "label": "__m", "body": "ₘ", "description": "ₘ" },
-                { "label": "__n", "body": "ₙ", "description": "ₙ" },
-                { "label": "__o", "body": "ₒ", "description": "ₒ" },
-                { "label": "__p", "body": "ₚ", "description": "ₚ" },
-                { "label": "__r", "body": "ᵣ", "description": "ᵣ" },
-                { "label": "__s", "body": "ₛ", "description": "ₛ" },
-                { "label": "__t", "body": "ₜ", "description": "ₜ" },
-                { "label": "__u", "body": "ᵤ", "description": "ᵤ" },
-                { "label": "__v", "body": "ᵥ", "description": "ᵥ" },
-                { "label": "__x", "body": "ₓ", "description": "ₓ" },
-
-                // Greek alphabet
-                { "label": "Alpha", "body": "Α", "description": "Α" },
-                { "label": "alpha", "body": "α", "description": "α" },
-                { "label": "Beta", "body": "Β", "description": "Β" },
-                { "label": "beta", "body": "β", "description": "β" },
-                { "label": "Gamma", "body": "Γ", "description": "Γ" },
-                { "label": "gamma", "body": "γ", "description": "γ" },
-                { "label": "Delta", "body": "Δ", "description": "Δ" },
-                { "label": "delta", "body": "δ", "description": "δ" },
-                { "label": "Epsilon", "body": "Ε", "description": "Ε" },
-                { "label": "epsilon", "body": "ε", "description": "ε" },
-                { "label": "Zeta", "body": "Ζ", "description": "Ζ" },
-                { "label": "zeta", "body": "ζ", "description": "ζ" },
-                { "label": "Eta", "body": "Η", "description": "Η" },
-                { "label": "eta", "body": "η", "description": "η" },
-                { "label": "Theta", "body": "Θ", "description": "Θ" },
-                { "label": "theta", "body": "θ", "description": "θ" },
-                { "label": "Iota", "body": "Ι", "description": "Ι" },
-                { "label": "iota", "body": "ι", "description": "ι" },
-                { "label": "Kappa", "body": "Κ", "description": "Κ" },
-                { "label": "kappa", "body": "κ", "description": "κ" },
-                { "label": "Lamda", "body": "Λ", "description": "Λ" },
-                { "label": "lamda", "body": "λ", "description": "λ" },
-                { "label": "Lambda", "body": "Λ", "description": "Λ" },
-                { "label": "lambda", "body": "λ", "description": "λ" },
-                { "label": "Mu", "body": "Μ", "description": "Μ" },
-                { "label": "mu", "body": "μ", "description": "μ" },
-                { "label": "Nu", "body": "Ν", "description": "Ν" },
-                { "label": "nu", "body": "ν", "description": "ν" },
-                { "label": "Xi", "body": "Ξ", "description": "Ξ" },
-                { "label": "xi", "body": "ξ", "description": "ξ" },
-                { "label": "Omicron", "body": "Ο", "description": "Ο" },
-                { "label": "omicron", "body": "ο", "description": "ο" },
-                { "label": "Pi", "body": "Π", "description": "Π" },
-                { "label": "pi", "body": "π", "description": "π" },
-                { "label": "Rho", "body": "Ρ", "description": "Ρ" },
-                { "label": "rho", "body": "ρ", "description": "ρ" },
-                { "label": "Sigma", "body": "Σ", "description": "Σ" },
-                { "label": "sigma", "body": "σ", "description": "σ" },
-                { "label": "Tau", "body": "Τ", "description": "Τ" },
-                { "label": "tau", "body": "τ", "description": "τ" },
-                { "label": "Upsilon", "body": "Υ", "description": "Υ" },
-                { "label": "upsilon", "body": "υ", "description": "υ" },
-                { "label": "Phi", "body": "Φ", "description": "Φ" },
-                { "label": "phi", "body": "φ", "description": "φ" },
-                { "label": "Chi", "body": "Χ", "description": "Χ" },
-                { "label": "chi", "body": "χ", "description": "χ" },
-                { "label": "Psi", "body": "Ψ", "description": "Ψ" },
-                { "label": "psi", "body": "ψ", "description": "ψ" },
-                { "label": "Omega", "body": "Ω", "description": "Ω" },
-                { "label": "omega", "body": "ω", "description": "ω" }
-            ]
-        }
-    ]
-```
-
+click on "Edit in settings.json" and add the contents of [this file](vscode).
 
 ## Vim
 
@@ -688,3 +379,14 @@ let g:unicode_map = {
   \ "_x"        :   "ₓ",
 \ }
 ```
+
+
+Alternatively, you can use snippets using [UltiSnips](https://github.com/SirVer/ultisnips).
+
+Install it with your favorite plugin manager, and register a completion key in your configuration:
+```
+let g:UltiSnipsExpandTrigger="<c-l>"
+```
+To insert a unicode character, type its trigger word, such as `\forall` or `->`, and then press `<c-l>` while still in insert mode.
+
+To register most common unicode characters, put [this file](vim_ultisnips) either at `~/.vim/UltiSnips/coq_unicode.snippets` or `~/.config/nvim/UltiSnips/coq_unicode.snippets`, depending on your preferred variant of Vim.

docs/equalities_and_entailments.md

 # Equalities in Iris
 
-Using Iris involves dealing with a few subtly different equivalence and equality
+Using std++ and Iris involves dealing with a few subtly different equivalence and equality
 relations, especially among propositions.
 This document summarizes these relations and the subtle distinctions among them.
 This is not a general introduction to Iris: instead, we discuss the different
@@ -8,7 +8,7 @@ Iris equalities and the interface to their Coq implementation. In particular, we
 discuss:
 - Equality ("=") in the *on-paper* Iris metatheory
 - Coq's Leibniz equality (`=`) and std++'s setoid equivalence (`≡`);
-- N-equivalence on OFEs (`≡{n}≡`);
+- Iris `n`-equivalence on OFEs (`≡{n}≡`);
 - Iris internal equality (`≡` in `bi_scope`);
 - Iris entailment and bi-entailment (`⊢`, `⊣⊢`).
 
@@ -45,6 +45,52 @@ Here, stdpp adds the following facilities:
   goal `f a ≡ f b` into `a ≡ b` given an appropriate `Proper` instance (here,
   `Proper ((≡) ==> (≡)) f`).
 
+## Defining Proper instances
+
+- For each function `f` that could be used in generalized rewriting (e.g., has
+  setoid, ofe, ordered arguments), there should be a `Params f n` instance. This
+  instance forces Coq's setoid rewriting mechanism not to rewrite in the first
+  `n` arguments of the function `f`. This significantly reduces backtracking
+  during `Proper` search and thus improves performance/avoids failing instance
+  searches that diverge. These first arguments typically include type variables
+  (`A : Type` or `B : A → Type`), type class parameters (`C A`), and Leibniz
+  arguments (`i : nat` or `i : Z`), so they cannot be rewritten or do not need
+  setoid rewriting.
+  Examples:
+  + For `cons : ∀ A, A → list A → list A` we have `Params (@cons) 1`,
+    indicating that the type argument named `A` is not up to rewriting.
+  + For `replicate : ∀ A, nat → A → list A` we have `Params (@replicate) 2`
+    indicating that the type argument `A` is not up to rewriting and that the
+    `nat`-typed argument also does not show up as rewriteable in the `Proper`
+    instance (because rewriting with `=` doesn't need such an instance).
+  + For `lookup : ∀ {Lookup K A M}, K → M → option A` we have
+    `Params (@lookup) 5`: there are 3 Type parameters, 1 type class, and a key
+    (which is Leibniz for all instances).
+- Consequenently, `Proper .. f` instances are always written in such a way
+  that `f` is partially applied with the first `n` arguments from `Params f n`.
+  Note that implicit arguments count here.
+  Further note that `Proper` instances never start with `(=) ==>`.
+  Examples:
+  + `Proper ((≡@{A}) ==> (≡@{list A}) ==> (≡@{list A})) cons`,
+    where `cons` is `@cons A`, matching the 1 in `Params`.
+  + `Proper ((≡@{A}) ==> (≡@{list A})) (replicate n)`,
+    where `replicate n` is `@replicate A n`.
+  + `Proper ((≡@{M}) ==> (≡@{option A})) (lookup k)`,
+    where `lookup k` is `@lookup K A M _ k`, so 5 parameters are fixed, matching
+    the `Params` instance.
+- Lemmas about higher-order functions often need `Params` premises.
+  These are also written using the convention above. Example:
+  ```coq
+  Lemma set_fold_ind `{FinSet A C} {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
+    (∀ x, Proper ((≡) ==> impl) (P x)) → ...
+  ```
+- For premises involving predicates (such as `P` in `set_fold_ind` above), we
+  always write the weakest `Proper`: that is, use `impl` instead of `iff` (and
+  in Iris, write `(⊢)` instead of `(⊣⊢)`). For "simple" `P`s, there should be
+  instances to solve both `impl` and `iff` using `solve_proper`, and for more
+  complicated cases where `solve_proper` fails, an `impl` is much easier to
+  prove by hand than an `iff`.
+
 ## Equivalences on OFEs
 
 On paper, OFEs involve two relations, equality "=" and distance "=_n". In Coq,

docs/heap_lang.md

@@ -33,7 +33,7 @@ constructor).
 ## Notation
 
 Notation for writing HeapLang terms is defined in
-[`notation.v`](../theories/heap_lang/notation.v).  There are two scopes, `%E` for
+[`notation.v`](../iris_heap_lang/notation.v).  There are two scopes, `%E` for
 expressions and `%V` for values.  For example, `(a, b)%E` is an expression pair
 and `(a, b)%V` a value pair.  The `e` of a `WP e {{ Q }}` is implicitly in `%E`
 scope.
@@ -55,9 +55,12 @@ that the current goal is of the shape `WP e @ E {{ Q }}`.
 
 Tactics to take one or more pure program steps:
 
-- `wp_pure`: Perform one pure reduction step.  Pure steps are defined by the
-  `PureExec` typeclass and include beta reduction, projections, constructors, as
-  well as unary and binary arithmetic operators.
+- `wp_pure pat credit:"H"`: Perform one pure reduction step. `pat` optionally
+  defines the pattern that the redex has to match; it defaults to `_` (any
+  redex). The `credit:` argument is optional, too; when present, a later credit
+  will be generated in a fresh hypothesis named `"H"`.
+  Pure steps are defined by the `PureExec` typeclass and include beta reduction,
+  projections, constructors, as well as unary and binary arithmetic operators.
 - `wp_pures`: Perform as many pure reduction steps as possible. This
   tactic will **not** reduce lambdas/recs that are hidden behind a definition.
   If the computation reaches a value, the `WP` will be entirely removed and the
@@ -101,14 +104,16 @@ Further tactics:
   particular when accessing invariants, which is only possible when the `WP` in
   the goal is for a single, atomic operation -- `wp_bind` can be used to bring
   the goal into the right shape.
-- `wp_apply pm_trm`: Apply a lemma whose conclusion is a `WP`, automatically
-  applying `wp_bind` as needed.  See the [ProofMode docs](./proof_mode.md) for an
-  explanation of `pm_trm`.
-- `wp_smart_apply pm_trm`: like `wp_apply`, but also performs pure reduction
-  steps to reveal a redex that matches `pm_trm`. Precisely, if applying the
-  lemma fails, `wp_smart_apply` will perform a step of pure reduction (via
-  `wp_pure`), and repeat. (This means that `wp_smart_apply` is not the same
-  as `wp_pures; wp_apply`.)
+- `wp_apply pm_trm as (x1 ... xn) "ipat1 ... ipatn"`:
+  Apply a lemma whose conclusion is a `WP`, automatically applying `wp_bind` as
+  needed. The `as` clause is optional and can be used to introduce the
+  postcondition; this works particularly well for Texan triples. See the
+  [ProofMode docs](./proof_mode.md) for an explanation of `pm_trm` and `ipat`.
+- `wp_smart_apply pm_trm as (x1 ... xn) "ipat1 ... ipatn"`:
+  like `wp_apply`, but also performs pure reduction steps to reveal a redex that
+  matches `pm_trm`. To be precise, if applying the lemma fails, `wp_smart_apply`
+  will perform a step of pure reduction (via `wp_pure`), and repeat. (This means
+  that `wp_smart_apply` is not the same as `wp_pures; wp_apply`.)
 
 There is no tactic for `Fork`, just do `wp_apply wp_fork`.
 
@@ -123,7 +128,7 @@ all of the redexes reduced.)
 Sometimes, it is useful to define a derived notion in HeapLang that involves
 thunks.  For example, the parallel composition `e1 ||| e2` is definable in
 HeapLang, but that requires thunking `e1` and `e2` before passing them to
-`par`. (This is defined in [`par.v`](theories/heap_lang/lib/par.v).)  However,
+`par`. (This is defined in [`par.v`](../iris_heap_lang/lib/par.v).)  However,
 this is somewhat subtle because of the distinction between expression lambdas
 and value lambdas.