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

+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: "The canonical example language for Iris"
+description: """
+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}
+]
+
+build: ["./make-package" "iris_heap_lang" "-j%{jobs}%"]
+install: ["./make-package" "iris_heap_lang" "install"]

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"]

coq-iris.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: "A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
+description: """
+Iris is a framework for reasoning about the safety of concurrent programs using
+concurrent separation logic. It can be used to develop a program logic, for
+defining logical relations, and for reasoning about type systems, among other
+applications. This package includes the base logic, Iris Proof Mode (IPM) /
+MoSeL, and a general language-independent program logic; see coq-iris-heap-lang
+for an instantiation of the program logic to a particular programming language.
+"""
+tags: [
+  "logpath:iris.prelude"
+  "logpath:iris.algebra"
+  "logpath:iris.si_logic"
+  "logpath:iris.bi"
+  "logpath:iris.proofmode"
+  "logpath:iris.base_logic"
+  "logpath:iris.program_logic"
+]
+
+depends: [
+  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
+  "coq-stdpp" { (= "dev.2025-03-30.0.9274984b") | (= "dev") }
+]
+
+build: ["./make-package" "iris" "-j%{jobs}%"]
+install: ["./make-package" "iris" "install"]

coq-lint.sh

+#!/bin/bash
+set -e
+## A simple shell script checking for some common Coq issues.
+
+FILE="$1"
+
+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
+    exit 1
+fi

descr

-This is the Coq development of the Iris Project.

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

+Here we collect some information on how to set up your editor to properly input
+and output the unicode characters used throughout Iris.
+
+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](../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,
+Unicode syntax is required for MRs to Iris itself and other Iris-managed
+repositories.
+
+## General: Unicode Fonts
+
+Most editors will just use system fonts for rendering unicode characters and do
+not need further configuration once the fonts are installed.  Here are some
+combinations of fonts that are known to give readable results (i.e., each of
+these sets of fonts covers all the required characters):
+
+* Fira Mono, DejaVu Mono, Symbola
+
+## Emacs
+
+### Unicode Input
+
+First, install `math-symbol-lists` by doing `M-x package-install math-symbol-lists`.
+
+Next, add the following to your `~/.emacs` to configure an input method based
+on the math symbol list, and with some custom aliases for symbols used a lot in Iris:
+```
+;; Input of unicode symbols
+(require 'math-symbol-lists)
+; Automatically use math input method for Coq files
+(add-hook 'coq-mode-hook (lambda () (set-input-method "math")))
+; Input method for the minibuffer
+(defun my-inherit-input-method ()
+  "Inherit input method from `minibuffer-selected-window'."
+  (let* ((win (minibuffer-selected-window))
+         (buf (and win (window-buffer win))))
+    (when buf
+      (activate-input-method (buffer-local-value 'current-input-method buf)))))
+(add-hook 'minibuffer-setup-hook #'my-inherit-input-method)
+; Define the actual input method
+(quail-define-package "math" "UTF-8" "Ω" t)
+(quail-define-rules ; add whatever extra rules you want to define here...
+ ("\\fun"    ?λ)
+ ("\\mult"   ?⋅)
+ ("\\ent"    ?⊢)
+ ("\\valid"  ?✓)
+ ("\\diamond" ?◇)
+ ("\\box"    ?□)
+ ("\\bbox"   ?■)
+ ("\\later"  ?▷)
+ ("\\pred"   ?φ)
+ ("\\and"    ?∧)
+ ("\\or"     ?∨)
+ ("\\comp"   ?∘)
+ ("\\ccomp"  ?◎)
+ ("\\all"    ?∀)
+ ("\\ex"     ?∃)
+ ("\\to"     ?→)
+ ("\\sep"    ?∗)
+ ("\\lc"     ?⌜)
+ ("\\rc"     ?⌝)
+ ("\\Lc"     ?⎡)
+ ("\\Rc"     ?⎤)
+ ("\\lam"    ?λ)
+ ("\\empty"  ?∅)
+ ("\\Lam"    ?Λ)
+ ("\\Sig"    ?Σ)
+ ("\\-"      ?∖)
+ ("\\aa"     ?●)
+ ("\\af"     ?◯)
+ ("\\auth"   ?●)
+ ("\\frag"   ?◯)
+ ("\\iff"    ?↔)
+ ("\\gname"  ?γ)
+ ("\\incl"   ?≼)
+ ("\\latert" ?▶)
+ ("\\update" ?⇝)
+
+ ;; 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" ?ₓ)
+)
+(mapc (lambda (x)
+        (if (cddr x)
+            (quail-defrule (cadr x) (car (cddr x)))))
+      ; 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)))
+```
+
+### Font Configuration
+
+Even when usable fonts are installed, Emacs tends to pick bad fonts for some
+symbols like universal and existential quantifiers.  The following configuration
+results in a decent choice for the symbols used in Iris:
+
+```
+;; Fonts
+(set-face-attribute 'default nil :height 110) ; height is in 1/10pt
+(dolist (ft (fontset-list))
+  ; Main font
+  (set-fontset-font ft 'unicode (font-spec :name "Monospace"))
+  ; Fallback font
+  ; Appending to the 'unicode list makes emacs unbearably slow.
+  ;(set-fontset-font ft 'unicode (font-spec :name "DejaVu Sans Mono") nil 'append)
+  (set-fontset-font ft nil (font-spec :name "DejaVu Sans Mono"))
+)
+; Fallback-fallback font
+; If we 'append this to all fontsets, it picks Symbola even for some cases where DejaVu could
+; be used. Adding it only to the "t" table makes it Do The Right Thing (TM).
+(set-fontset-font t nil (font-spec :name "Symbola"))
+```
+
+### Automated Indentation
+
+The default indentation configuration of company-coq is not compatible with the Iris syntax.
+As a result, automatic indentation will indent lines incorrectly.
+
+To solve some of these indentation errors you can add the following line to your Emacs
+initialisation file:
+```
+(setq coq-smie-user-tokens
+   '(("," . ":=")
+	("∗" . "->")
+	("-∗" . "->")
+	("∗-∗" . "->")
+	("==∗" . "->")
+	("=∗" . "->") 			;; Hack to match ={E1,E2}=∗
+	("|==>" . ":=")
+	("⊢" . "->")
+	("⊣⊢" . "->")
+	("↔" . "->")
+	("←" . "<-")
+	("→" . "->")
+	("=" . "->")
+	("==" . "->")
+	("/\\" . "->")
+	("⋅" . "->")
+	(":>" . ":=")
+	("by" . "now")
+	("forall" . "now")              ;; NB: this breaks current ∀ indentation.
+   ))
+```
+This will let the indentation strategy treat the Iris symbols (e.g. `-∗`) similar to the
+closely related Coq symbols (e.g. `->`).
+Note that `->` is used in many places, as its indentation behaviour is:
+```
+  P ->
+  Q
+```
+This is the indentation behaviour is what we want, e.g. for `∗`:
+```
+  P ∗
+  Q
+```
+Note that this configuration has some caveats.
+Notably, the change to `forall` (which gives good behavior to e.g.
+`iInduction xs as [|x xs IHxs] forall (ys).`), now gives the following indentation
+behavior to universal quantification:
+```
+  ∀ x,
+  P x
+```
+This is not what we want; the second line should be indented by 2 spaces.
+
+## CoqIDE 8.9 and earlier on Linux (ibus-m17n)
+
+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 as defined [here](ibus).
+
+To use this input method, you should:
+
+1. Enable the "Coq" input using your system settings or using the IBus
+   configuration tool. The Coq input method typically appears in the category
+   "other".
+2. On some systems: In CoqIDE, you have to enable the input method by performing
+   a right click on the text area, and selecting "System (IBus)" under "input
+   method".
+
+## CoqIDE 8.10+ Unicode input
+
+Instead of configuring the input system-wide, you can use CoqIDE's support for
+inputting Unicode symbols (introduced in Coq v8.10). To input a symbol, type a
+LaTeX-like escape sequence, for example `\alpha` and then type
+`<Shift>-<Space>`, which will expand it into `α`. Expansion will work on a
+prefix of the command as well. You can also customize the expansion keyboard
+shortcut, which is under Tools/LaTeX-to-unicode.
+
+This system is configurable by adding a Unicode bindings file with additional
+expansion sequences. On Linux this file should go in
+`~/.config/coq/coqide.bindings` while on macOS it should go in
+`~/Library/Application Support/Coq/coqide.bindings` (or under `$XDG_CONFIG_HOME`
+if you have that set).
+
+Here is a `coqide.bindings` file for a variety of symbols used in Iris:
+
+```
+# LaTeX-like sequences are natively supported (eg, \forall, \mapsto)
+# Iris-specific abbreviations
+\fun            λ
+\mult           ⋅ 1
+\ent            ⊢ 1
+\valid          ✓
+\diamond        ◇
+\box            □ 1
+\bbox           ■
+\later          ▷
+\pred           φ
+\and            ∧
+\or             ∨
+\comp           ∘ 1
+\ccomp          ◎
+\all            ∀
+\ex             ∃
+\to             →
+\sep            ∗
+\lc             ⌜ 1
+\rc             ⌝ 1
+\Lc             ⎡ 1
+\Rc             ⎤ 1
+\lam            λ
+\empty          ∅
+\Lam            Λ
+\Sig            Σ
+\-              ∖ 1
+\aa             ● 1
+\af             ◯ 1
+\auth           ●
+\frag           ◯
+\iff            ↔ 1
+\gname          γ
+\incl           ≼
+\latert         ▶
+\update         ⇝
+# accents
+\"o             ö
+\Lob            Löb
+# 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             ₓ
+```
+
+## Visual Studio Code
+
+### VSCoq setup
+
+The recommended extension as of December 2019 is [Maxime Dénès's
+VSCoq](https://marketplace.visualstudio.com/items?itemName=maximedenes.vscoq).
+Press `Ctrl Shift P` or `Cmd Shift P` and then type "coq" to see the list of Coq
+commands and keyboard shortcuts.
+
+### Font setup
+
+To use unicode you need a font that supports all the symbols, such as [Fira
+Code](https://github.com/tonsky/FiraCode/wiki/Installing). Download and install
+the font, and in VS Code press `Cmd ,` or `Ctrl ,` to go to the settings, search
+for "font", and use "FiraCode-Retina" on macOS or "Fira Code Retina" on Linux as the font-family and optionally enable
+ligatures.
+
+### Unicode input setup
+
+Install the [Generic input method
+extension](https://marketplace.visualstudio.com/items?itemName=mr-konn.generic-input-method).
+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 contents of [this file](vscode).
+
+## Vim
+
+The [Coqtail](https://github.com/whonore/coqtail) plugin can be used to develop Coq code in `vim` (install it with your favorite plugin manager).
+Follow the installation instructions in Coqtail's README to setup your keybinds and find out about its usage.
+
+### Unicode support
+For Unicode support, make sure that your terminal emulator supports Unicode and configure it to use a font with Unicode support.
+
+For entering Unicode symbols, one option is the plugin [latex-unicoder](https://github.com/joom/latex-unicoder.vim).
+Install it with your favorite plugin manager.
+To enter a Unicode symbol, hit `C-l` in normal or insert mode. For more details on the usage, see its README.
+
+latex-unicoder comes with a large set of pre-configured symbols known from LaTeX, but you can also add your own by adding (and adapting) the following to your `.vimrc`:
+```
+let g:unicode_map = {
+  \ "\\fun"     :   "λ",
+  \ "\\mult"    :   "⋅",
+  \ "\\ent"     :   "⊢",
+  \ "\\valid"   :   "✓",
+  \ "\\diamond" :   "◇",
+  \ "\\box"     :   "□",
+  \ "\\bbox"   	:   "■",
+  \ "\\later"  	:   "▷",
+  \ "\\pred"   	:   "φ",
+  \ "\\and"    	:   "∧",
+  \ "\\or"     	:   "∨",
+  \ "\\comp"   	:   "∘",
+  \ "\\ccomp"  	:   "◎",
+  \ "\\all"    	:   "∀",
+  \ "\\ex"     	:   "∃",
+  \ "\\to"     	:   "→",
+  \ "\\sep"    	:   "∗",
+  \ "\\lc"     	:   "⌜",
+  \ "\\rc"     	:   "⌝",
+  \ "\\Lc"     	:   "⎡",
+  \ "\\Rc"     	:   "⎤",
+  \ "\\lam"    	:   "λ",
+  \ "\\empty"  	:   "∅",
+  \ "\\Lam"    	:   "Λ",
+  \ "\\Sig"    	:   "Σ",
+  \ "\\-"      	:   "∖",
+  \ "\\aa"     	:   "●",
+  \ "\\af"     	:   "◯",
+  \ "\\auth"   	:   "●",
+  \ "\\frag"   	:   "◯",
+  \ "\\iff"    	:   "↔",
+  \ "\\gname"  	:   "γ",
+  \ "\\incl"   	:   "≼",
+  \ "\\latert" 	:   "▶",
+  \ "\\update" 	:   "⇝",
+  \ "\\\"o"     :   "ö",
+  \ "_a"        :   "ₐ",
+  \ "_e"        :   "ₑ",
+  \ "_h"        :   "ₕ",
+  \ "_i"        :   "ᵢ",
+  \ "_k"        :   "ₖ",
+  \ "_l"        :   "ₗ",
+  \ "_m"        :   "ₘ",
+  \ "_n"        :   "ₙ",
+  \ "_o"        :   "ₒ",
+  \ "_p"        :   "ₚ",
+  \ "_r"        :   "ᵣ",
+  \ "_s"        :   "ₛ",
+  \ "_t"        :   "ₜ",
+  \ "_u"        :   "ᵤ",
+  \ "_v"        :   "ᵥ",
+  \ "_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 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
+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 (`≡`);
+- Iris `n`-equivalence on OFEs (`≡{n}≡`);
+- Iris internal equality (`≡` in `bi_scope`);
+- Iris entailment and bi-entailment (`⊢`, `⊣⊢`).
+
+We use `code font` for Coq notation and "quotes" for paper notation.
+
+## Leibniz equality and setoids
+
+First off, in the metalogic (Coq) we have both the usual propositional (or
+Leibniz) equality `=`, and setoid equality `equiv` / `≡` (defined in `stdpp`).
+Both of these are metalogic connectives from the perspective of Iris, and as
+such are declared in Coq scope `stdpp_scope`.
+
+Setoid equality for a type `A` is defined by the instance of `Equiv A`.  This
+should be accompanied by an `Equivalence` instance which proves that the given
+relation indeed is an equivalence relation.  The handling of setoidsis based on
+Coq's
+[generalized rewriting](https://coq.inria.fr/refman/addendum/generalized-rewriting.html)
+facilities.
+
+Setoid equality can coincide with Leibniz equality, which is reflected by the
+`LeibnizEquiv` typeclass. We say that types with this property are "Leibniz
+types". `equivL` provides a convenient way to define a setoid with Leibniz
+equality. The tactics `fold_leibniz` and `unfold_leibniz` can be used to
+automatically turn all equalities of Leibniz types into `≡` or `=`.
+
+Given setoids `A` and `B` and a function `f : A → B`, an instance `Proper ((≡)
+==> (≡)) f` declares that `f` respects setoid equality, as usual in Coq. Such
+instances enable rewriting with setoid equalities.
+
+Here, stdpp adds the following facilities:
+- `solve_proper` for automating proofs of `Proper` instances.
+- `f_equiv` generalizes `f_equal` to setoids (and indeed arbitrary relations
+  registered with Coq's generalized rewriting). It will for instance turn the
+  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,
+equality "=" is formalized as setoid equality, written `≡` or `equiv`, as before;
+distance "=_n" is formalized as relation `dist n`, also written `≡{n}≡`.
+Tactics `solve_proper` and `f_equiv` also support distance. There is no
+correspondence to Coq's `=` on paper.
+
+Some OFE constructors choose interesting equalities.
+- `discreteO` constructs discrete OFEs (where distance coincides with setoid equality).
+- `leibnizO` constructs discrete OFEs (like `discreteO`) but using `equivL`, so
+  that both distance and setoid equality coincide with Leibniz equality. This
+  should only be used for types that do not have a setoid equality registered.
+
+Given OFEs `A` and `B`, non-expansive functions from `A` to `B` are functions
+`f : A → B` with a proof of `NonExpansive f` (which is notation for `∀ n, Proper
+(dist n ==> dist n) f`).
+
+The type `A -n> B` packages a function with a non-expansiveness proof. This is
+useful because `A -n> B` is itself an OFE, but should be avoided whenever
+possible as it requires the caller to specifically package up function and proof
+(which works particularly badly for lambda expressions).
+
+When an OFE structure on a function type is required but the domain is discrete,
+one can use the type `A -d> B`.  This has the advantage of not bundling any
+proofs, i.e., this is notation for a plain Coq function type. See the
+`discrete_fun` documentation in [`iris.algebra.ofe`](../iris/algebra/ofe.v)
+for further details.
+
+In both OFE function spaces (`A -n> B` and `A -d> B`), setoid equality is
+defined to be pointwise equality, so that functional extensionality holds for `≡`.
+
+## Inside the Iris logic
+
+Next, we introduce notions internal to the Iris logic. Such notions often
+overload symbols used for external notions; however, those overloaded notations
+are declared in scope `bi_scope`. When writing `(P)%I`, notations in `P` are
+resolved in `bi_scope`; this is done implicitly for the arguments of all
+variants of Iris entailments.
+
+The Iris logic has an internal concept of equality: if `a` and `b` are Iris
+terms of type `A`, then their internal equality is written (on paper) "a =_A b";
+in Coq, that's written `(a ≡@{A} b)%I` (notation for `bi_internal_eq` in scope
+`bi_scope`). You can leave away the `@{A}` to let Coq infer the type.
+
+As shown in the Iris appendix, an internal equality `(a ≡ b)%I` is interpreted using
+OFE distance at the current step-index. Many types have `_equivI` lemmas
+characterizing internal equality on them. For instance, if `f, g : A -d> B`,
+lemma `discrete_fun_equivI` shows that `(f ≡ g)%I` is equivalent to
+`(∀ x, f x ≡ g x)%I`.
+
+An alternative to internal equality is to embed Coq equality into the Iris logic
+using `⌜ _ ⌝%I`.  For discrete types, `(a ≡ b)%I` is equivalent to `⌜a ≡ b⌝%I`,
+and the latter can be moved into the Coq context, making proofs more convenient.
+For types with Leibniz equality, we can even equivalently write `⌜a = b⌝%I`, so
+no `Proper` is needed for rewriting.  Note that there is no on-paper equivalent
+to using these embedded Coq equalities for types that are not discrete/Leibniz.
+
+## Relations among Iris propositions
+
+In this section, we discuss relations among internal propositions, and in particular equality/equivalence of propositions themselves.
+Even though some of these notes generalize to all internal logics (other
+`bi`s), we focus on Iris propositions (`iProp`), to discuss both their proof
+theory and their model.
+As Iris propositions form a separation logic, we assume some familiarity with
+separation logics, connectives such as `-∗`, `∗`, `emp` and `→`, and the idea
+that propositions in separation logics are interpreted with predicates over
+resources (see for instance Sec. 2.1 of the MoSEL paper).
+
+In the metalogic, Iris defines the entailment relation between uniform
+predicates: intuitively, `P` entails `Q` (written `P ⊢ Q`) means that `P`
+implies `Q` on _every_ resource and at all step-indices (for details see Iris appendix [Sec. 6]).
+Entailment `P ⊢ Q` is distinct from the magic wand, `(P -∗ Q)%I`: the former is
+a Coq-level statement of type `Prop`, the latter an Iris-level statement of type
+`iProp`.  However, the two are closely related: `P ⊢ Q` is equivalent to `emp ⊢
+P -∗ Q` (per Iris lemmas `entails_wand` and `wand_entails`).  Iris also defines
+a "unary" form of entailment, `⊢ P`, which is short for `emp ⊢ P`.
+We can also use bi-entailment `P ⊣⊢ Q` to express that both `P ⊢ Q` and `Q ⊢ P` hold.
+
+On paper, uniform predicates are defined by quotienting by an equivalence
+relation ([Iris appendix, Sec. 3.3]); in Coq, that relation is chosen as the
+setoid equivalent for the type of Iris propositions.
+This equivalence is actually equivalent to bi-entailment, per lemma `equiv_spec`:
+```coq
+Lemma equiv_spec P Q : P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P).
+```
+Relying on this equivalence, bi-entailment `P ⊣⊢ Q` is defined as notation for `≡`.
+
+## Internal equality of Iris propositions
+
+Inside the logic, we can use internal equality `(≡)%I` on any type, including
+propositions themselves.  However, there is a pitfall here: internal equality
+`≡` is in general strictly stronger than `∗-∗` (the bidirectional version of the
+magic wand), because `Q1 ≡ Q2` means that `Q1` and `Q2` are equivalent
+_independently of the available resources_. This makes `≡` even stronger than `□
+(_ ∗-∗ _)`, because `□` does permit the usage of some resources (namely, the RA
+core of the available resources can still be used).
+
+The two notions of internal equivalence and equality of propositions are related
+by the following law of propositional extensionality:
+```coq
+Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■ (P ∗-∗ Q).
+```
+This uses the plainly modality `■` to reflect that equality corresponds to
+equivalence without any resources available: `■ R` says that `R` holds
+independent of any resources that we might own (but still taking into account
+the current step-index).

docs/heap_lang.md

+# HeapLang overview
+
+HeapLang is the example language that gets shipped with Iris.  It is not the
+only language you can reason about with Iris, but meant as a reasonable demo
+language for simple examples.
+
+## Language
+
+HeapLang is a lambda-calculus with operations to allocate individual locations,
+`load`, `store`, `CmpXchg` (compare-and-exchange) and `FAA` (fetch-and-add). Moreover,
+it has a `fork` construct to spawn new threads.  In terms of values, we have
+integers, booleans, unit, heap locations, as well as (binary) sums and products.
+
+Recursive functions are the only binders, so the sum elimination (`Case`)
+expects both branches to be of function type and passes them the data component
+of the sum.
+
+For technical reasons, the only terms that are considered values are those that
+begin with the `Val` expression former.  This means that, for example, `Pair
+(Val a) (Val b)` is *not* a value -- it reduces to `Val (PairV a b)`, which is.
+This leads to some administrative redexes, and to a distinction between "value
+pairs", "value sums", "value closures" and their "expression" counterparts.
+
+However, this also makes values syntactically uniform, which we exploit in the
+definition of substitution which just skips over `Val` terms, because values
+should be closed and hence not affected by substitution.  As a consequence, we
+can entirely avoid even talking about "closed terms", that notion just does not
+have to come up anywhere.  We also exploit this when writing specifications,
+because we can just write lemmas involving terms of the form `Val ?v` and Coq
+can determine `?v` by unification (because all values start with the `Val`
+constructor).
+
+## Notation
+
+Notation for writing HeapLang terms is defined in
+[`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.
+
+We define a whole lot of short-hands, such as non-recursive functions (`λ:`),
+let-bindings, sequential composition, and a more conventional `match:` that has
+binders in both branches.
+
+The widely used `#` is a short-hand to turn a basic literal (an integer, a
+location, a boolean literal or a unit value) into a value.  Since values coerce
+to expressions, `#` is widely used whenever a Coq value needs to be placed into
+a HeapLang term.
+
+## Tactics
+
+HeapLang comes with a bunch of tactics that facilitate stepping through HeapLang
+programs as part of proving a weakest precondition.  All of these tactics assume
+that the current goal is of the shape `WP e @ E {{ Q }}`.
+
+Tactics to take one or more pure program steps:
+
+- `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
+  postcondition becomes the new goal.
+- `wp_rec`, `wp_lam`: Perform a beta reduction.  Unlike `wp_pure`, this will
+  also reduce lambdas that are hidden behind a definition.
+- `wp_let`, `wp_seq`: Reduce a let-binding or a sequential composition.
+- `wp_proj`: Reduce a projection.
+- `wp_if_true`, `wp_if_false`, `wp_if`: Reduce a conditional expression. The
+  discriminant must already be `true` or `false`.
+- `wp_unop`, `wp_binop`, `wp_op`: Reduce a unary, binary or either kind of
+  arithmetic operator.
+- `wp_case`, `wp_match`: Reduce `Case`/`match:` constructs.
+- `wp_inj`, `wp_pair`, `wp_closure`: Reduce constructors that turn expression
+  sums/pairs/closures into their value counterpart.
+
+Tactics for the heap:
+
+- `wp_alloc l as "H"`: Reduce an allocation instruction and call the new
+  location `l` (in the Coq context) and the points-to assertion `H` (in the
+  spatial context).  You can leave out the `as "H"` to introduce it as an
+  anonymous assertion, which is equivalent to `as "?"`.
+- `wp_load`: Reduce a load operation.  This automatically finds the points-to
+  assertion in the spatial context, and fails if it cannot be found.
+- `wp_store`: Reduce a store operation.  This automatically finds the points-to
+  assertion in the spatial context, and fails if it cannot be found.
+- `wp_cmpxchg_suc`, `wp_cmpxchg_fail`: Reduce a succeeding/failing CmpXchg.  This
+  automatically finds the points-to assertion.  It also automatically tries to
+  solve the (in)equality to show that the CmpXchg succeeds/fails, and opens a new
+  goal if it cannot prove this goal.
+- `wp_cmpxchg as H1 | H2`: Reduce a CmpXchg, performing a case distinction over whether
+  it succeeds or fails.  This automatically finds the points-to assertion.  The
+  proof of equality in the first new subgoal will be called `H1`, and the proof
+  of the inequality in the second new subgoal will be called `H2`.
+- `wp_faa`: Reduce a FAA.  This automatically finds the points-to assertion.
+
+Further tactics:
+
+- `wp_bind pat`: Apply the bind rule to "focus" the term matching `pat`.  For
+  example, `wp_bind (!_)%E` focuses a load operation.  This is useful in
+  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 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`.
+
+To verify a recursive function, use `iLöb`.  Make sure you do `wp_pures` before
+running `iLöb`; otherwise the induction hypothesis will likely not be applicable
+when you need it.  (This makes sure that all administrative redexes are reduced
+in your induction hypothesis, just like we state our `WP` specifications with
+all of the redexes reduced.)
+
+## Notation and lemmas for derived notions involving a thunk
+
+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`](../iris_heap_lang/lib/par.v).)  However,
+this is somewhat subtle because of the distinction between expression lambdas
+and value lambdas.
+
+The normal `e1 ||| e2` notation uses expression lambdas, because clearly we want
+`e1` and `e2` to behave normal under substitution (which they would not in a
+value lambda).  However, the *specification* for parallel composition should use
+value lambdas, because prior to applying it the term will be reduced as much as
+possible to achieve a normal form.  To facilitate this, we define a copy of the
+`e1 ||| e2` notation in the value scope that uses value lambdas.
+This is not actually a value, but we still put it in the value scope to
+differentiate from the other notation that uses expression lambdas.  (In the
+future, we might decide to add a separate scope for this.)  Then, we write the
+canonical specification using the notation in the value scope.
+
+This works very well for non-recursive notions.  For `while` loops, the
+situation is unfortunately more complex and proving the desired specification
+will likely be more involved than expected, see this [discussion].
+
+[discussion]: https://gitlab.mpi-sws.org/iris/iris/merge_requests/210#note_32842

Editor.md → docs/ibus

-Here we collect some information on how to set up your editor to properly input
-and output the unicode characters used throughout Iris.
-
-## General: Unicode Fonts
-
-Most editors will just use system fonts for rendering unicode characters and do
-not need furhter configuration once the fonts are installed.  Here are some
-combinations of fonts that are known to give readable results (i.e., each of
-these sets of fonts covers all the required characters):
-
-* Fira Mono, DejaVu Mono, Symbola
-
-## Emacs
-
-### Unicode Input
-
-First, install `math-symbol-lists` by doing `M-x package-install math-symbol-lists`.
-
-Next, add the following to your `~/.emacs` to configure an input method based
-on the math symbol list, and with some custom aliases for symbols used a lot in Iris:
-```
-;; Input of unicode symbols
-(require 'math-symbol-lists)
-; Automatically use math input method for Coq files
-(add-hook 'coq-mode-hook (lambda () (set-input-method "math")))
-; Input method for the minibuffer
-(defun my-inherit-input-method ()
-  "Inherit input method from `minibuffer-selected-window'."
-  (let* ((win (minibuffer-selected-window))
-         (buf (and win (window-buffer win))))
-    (when buf
-      (activate-input-method (buffer-local-value 'current-input-method buf)))))
-(add-hook 'minibuffer-setup-hook #'my-inherit-input-method)
-; Define the actual input method
-(quail-define-package "math" "UTF-8" "Ω" t)
-(quail-define-rules ; add whatever extra rules you want to define here...
- ("\\mult"   ?⋅)
- ("\\ent"    ?⊢)
- ("\\valid"  ?✓)
- ("\\box"    ?□)
- ("\\later"  ?▷)
- ("\\pred"   ?φ)
- ("\\and"    ?∧)
- ("\\or"     ?∨)
- ("\\comp"   ?∘)
- ("\\ccomp"  ?◎)
- ("\\all"    ?∀)
- ("\\ex"     ?∃)
- ("\\to"     ?→)
- ("\\sep"    ?∗)
- ("\\lc"     ?⌜)
- ("\\rc"     ?⌝)
- ("\\lam"    ?λ)
- ("\\empty"  ?∅)
- ("\\Lam"    ?Λ)
- ("\\Sig"    ?Σ)
- ("\\-"      ?∖)
- ("\\aa"     ?●)
- ("\\af"     ?◯)
- ("\\iff"    ?↔)
- ("\\gname"  ?γ)
- ("\\incl"   ?≼)
- ("\\latert" ?▶)
-)
-(mapc (lambda (x)
-        (if (cddr x)
-            (quail-defrule (cadr x) (car (cddr x)))))
-      (append math-symbol-list-basic math-symbol-list-extended))
-```
-
-### Font Configuration
-
-Even when usable fonts are installed, Emacs tends to pick bad fonts for some
-symbols like universal and existential quantifiers.  The following configuration
-results in a decent choice for the symbols used in Iris:
-
-```
-;; Fonts
-(set-face-attribute 'default nil :height 110) ; height is in 1/10pt
-(dolist (ft (fontset-list))
-  ; Main font
-  (set-fontset-font ft 'unicode (font-spec :name "Monospace"))
-  ; Fallback font
-  ; Appending to the 'unicode list makes emacs unbearably slow.
-  ;(set-fontset-font ft 'unicode (font-spec :name "DejaVu Sans Mono") nil 'append)
-  (set-fontset-font ft nil (font-spec :name "DejaVu Sans Mono"))
-)
-; Fallback-fallback font
-; If we 'append this to all fontsets, it picks Symbola even for some cases where DejaVu could
-; be used. Adding it only to the "t" table makes it Do The Right Thing (TM).
-(set-fontset-font t nil (font-spec :name "Symbola"))
-```
-
-## CoqIDE
-
-CoqIDE does not have support for unicode itself, but you can use the Intelligent
-Input Bus (IBus) framework for multilingual input. 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)
@@ -108,10 +6,10 @@ aliases for symbols used a lot in Iris:
 
 (map (trans
 
-;; Standard math notations
+;; Standard LaTeX math notations
   ("\\forall"         "∀")
-  ("\\fun"            "λ")
   ("\\exists"         "∃")
+  ("\\lam"            "λ")
   ("\\not"            "¬")
   ("\\/"              "∨")
   ("/\\"              "∧")
@@ -132,7 +30,6 @@ aliases for symbols used a lot in Iris:
   ("\\sqsubseteq"     "⊑")
   ("\\sqsubseteq"     "⊑")
   ("\\notsubseteq"    "⊈")
-  ("\\empty"          "∅")
   ("\\meet"           "⊓")
   ("\\join"           "⊔")
   ("\\top"            "⊤")
@@ -149,34 +46,53 @@ aliases for symbols used a lot in Iris:
   ("\\uparrow"        "↑")
 
 ;; Iris specific
-  ("\\check"          "✓")
-  ("\\later"          "▷")
-  ("\\latert"         "▶")
+  ("\\fun"            "λ")
+  ("\\mult"           "⋅")
+  ("\\ent"            "⊢")
+  ("\\valid"          "✓")
   ("\\diamond"        "◇")
-  ("\\square"         "□")
-  ("\\bsquare"        "■")
-  ("\\*"              "∗")
-  ("\\included"       "≼")
-  ("\\op"             "⋅")
-  ("\\update"         "⇝")
-  ("\\auth"           "●")
-  ("\\frag"           "◯")
+  ("\\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"           "≫=")
 
-;; Commonly used sub- and superscripts
-  ("^^+" ?⁺) ("__+" ?₊) ("^^-" ?⁻)
-  ("__0" ?₀) ("__1" ?₁) ("__2" ?₂) ("__3" ?₃) ("__4" ?₄)
-  ("__5" ?₅) ("__6" ?₆) ("__7" ?₇) ("__8" ?₈) ("__9" ?₉)
+;; accents (for iLöb)
+  ("\\\"o" "ö")
 
-  ("__a" ?ₐ) ("__e" ?ₑ) ("__h" ?ₕ) ("__i" ?ᵢ) ("__k" ?ₖ)
-  ("__l" ?ₗ) ("__m" ?ₘ) ("__n" ?ₙ) ("__o" ?ₒ) ("__p" ?ₚ)
-  ("__r" ?ᵣ) ("__s" ?ₛ) ("__t" ?ₜ) ("__u" ?ᵤ) ("__v" ?ᵥ) ("__x" ?ₓ)
+;; subscripts and superscripts
+  ("^^+" "⁺") ("__+" "₊") ("^^-" "⁻")
+  ("__0" "₀") ("__1" "₁") ("__2" "₂") ("__3" "₃") ("__4" "₄")
+  ("__5" "₅") ("__6" "₆") ("__7" "₇") ("__8" "₈") ("__9" "₉")
 
-;; Commonly used acents
-  ("\\\"o" "ö")
+  ("__a" "ₐ") ("__e" "ₑ") ("__h" "ₕ") ("__i" "ᵢ") ("__k" "ₖ")
+  ("__l" "ₗ") ("__m" "ₘ") ("__n" "ₙ") ("__o" "ₒ") ("__p" "ₚ")
+  ("__r" "ᵣ") ("__s" "ₛ") ("__t" "ₜ") ("__u" "ᵤ") ("__v" "ᵥ") ("__x" "ₓ")
 
 ;; Greek alphabet
   ("\\Alpha"  "Α")   ("\\alpha"  "α")
@@ -206,13 +122,3 @@ aliases for symbols used a lot in Iris:
   ("\\Omega"  "Ω")   ("\\omega"  "ω")
 ))
 (state (init (trans)))
-```
-
-To use this input method, you should:
-
-1. Enable the "Coq" input using your system settings or using the IBus
-   configuration tool. The Coq input method typically appears in the category
-   "other".
-2. On some systems: In CoqIDE, you have to enable the input method by performing
-   a right click on the text area, and selecting "System (IBus)" under "input
-   method".

dune

+(env
+ (_ ; Applies to all profiles (dev, release, ...).
+  (coq
+   (flags ; Configure the coqc flags.
+    (:standard ; Keeping the default flags.
+     ; Add custom flags (to be kept in sync with _CoqProject).
+     -w -notation-overridden
+     -w -redundant-canonical-projection
+     -w -unknown-warning
+     -w -argument-scope-delimiter
+     -w -notation-incompatible-prefix
+)))))