logsem · srghma · Jul 22, 2026 · Jul 22, 2026 · Jul 22, 2026 · Jul 22, 2026
diff --git a/.devcontainer/arm64/devcontainer.json b/.devcontainer/arm64/devcontainer.json
@@ -1,9 +1,9 @@
 {
 	"name": "iris-tutorial arm64 container",
-	"image": "ghcr.io/logsem/iris-tutorial/docker-arm64",
+	"image": "ghcr.io/logsem/iris-tutorial/debian-ocaml-5.5-arm64",
 	"customizations": {
 		"vscode": {
-		  "extensions": ["maximedenes.vscoq"]
+		  "extensions": ["rocq-prover.vsrocq"]
 		},
 		"settings": {
 			"terminal.integrated.profiles.linux": {
@@ -14,5 +14,6 @@
 			},
 			"terminal.integrated.defaultProfile.linux": "bash"
 		}
-	}
-}
+	},
+	"remoteUser": "opam"
+}
diff --git a/.devcontainer/x86-64/devcontainer.json b/.devcontainer/x86-64/devcontainer.json
@@ -1,9 +1,9 @@
 {
 	"name": "iris-tutorial x86-64 container",
-	"image": "ghcr.io/logsem/iris-tutorial/docker-x86-64",
+	"image": "ghcr.io/logsem/iris-tutorial/debian-ocaml-5.5-x86-64",
 	"customizations": {
 		"vscode": {
-		  "extensions": ["maximedenes.vscoq"]
+		  "extensions": ["rocq-prover.vsrocq"]
 		},
 		"settings": {
 			"terminal.integrated.profiles.linux": {
@@ -14,5 +14,6 @@
 			},
 			"terminal.integrated.defaultProfile.linux": "bash"
 		}
-	}
-}
+	},
+	"remoteUser": "opam"
+}
diff --git a/.dockerignore b/.dockerignore
@@ -0,0 +1,2 @@
+*
+!iris-tutorial.opam
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -11,12 +11,14 @@ on:
 jobs:
   build:
     runs-on: ubuntu-latest
-    container:
-      image: ghcr.io/logsem/iris-tutorial/docker-x86-64:latest
-      options: --user root
-
     steps:
       - uses: actions/checkout@v4
-      - name: make-ci
-        shell: bash -l {0}
-        run: export HOME=/root; eval $(opam env); make ci -j2
+      - uses: rocq-prover/docker-opam-action@v1
+        with:
+          rocq_version: '9.1'
+          ocaml_version: '5.5'
+          before_install: |
+            opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git --all --set-default
+          script: |
+            git config --global --add safe.directory "*"
+            make ci -j$(nproc)
diff --git a/.gitignore b/.gitignore
@@ -3,23 +3,23 @@
 *.vok
 *.vio
 *.v.d
-.coqdeps.d
+.rocqdeps.d
 *.glob
 *.cache
 *.aux
 \#*\#
 .\#*
 *~
 *.bak
-.coqdeps.d
-.coq-native/
-*.crashcoqide
+.rocqdeps.d
+.rocq-native/
+*.crashrocqide
 .env
 builddep/
-_CoqProject.*
-Makefile.coq
-Makefile.coq.conf
-.Makefile.coq.d
+_RocqProject.*
+Makefile.rocq
+Makefile.rocq.conf
+.Makefile.rocq.d
 Makefile.package.*
 .Makefile.package.*
 _opam

diff --git a/.gitmodules b/.gitmodules
diff --git a/Makefile b/Makefile
@@ -1,30 +1,30 @@
 SOLUTIONS := $(wildcard theories/*.v)
 EXERCISES := $(addprefix exercises/,$(notdir $(SOLUTIONS)))
 
-EXTRA_DIR:=coqdocjs/extra
-COQDOCFLAGS:= \
+EXTRA_DIR:=rocqdocjs/extra
+ROCQDOCFLAGS:= \
   --toc --toc-depth 2 --html --interpolate \
   --index indexpage --no-lib-name --parse-comments \
   --with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html
-export COQDOCFLAGS
+export ROCQDOCFLAGS
 
-all: Makefile.coq
-	+make -f Makefile.coq all
+all: Makefile.rocq
+	+make -f Makefile.rocq all
 .PHONY: all
 
-clean: Makefile.coq
-	+make -f Makefile.coq clean
-	rm -f Makefile.coq
+clean: Makefile.rocq
+	+make -f Makefile.rocq clean
+	rm -f Makefile.rocq
 .PHONY: clean
 
-html: Makefile.coq _CoqProject
+html: Makefile.rocq _RocqProject
 	rm -fr html
-	+make -f Makefile.coq $@
+	+make -f Makefile.rocq $@
 	cp -R $(EXTRA_DIR)/resources html
 .PHONY: html
 
-Makefile.coq: _CoqProject
-	coq_makefile -f _CoqProject -o Makefile.coq
+Makefile.rocq: _RocqProject
+	rocq makefile -f _RocqProject -o Makefile.rocq
 
 exercises: $(EXERCISES)
 .PHONY: exercises
@@ -34,7 +34,7 @@ $(EXERCISES): exercises/%.v: theories/%.v gen-exercises.awk
 	  echo "Exercise file $@ has been changed; skipping exercise generation"; \
 	else \
 	  echo "Generating exercise file $@ from $<"; \
-	  gawk -f gen-exercises.awk < $< > $@; \
+	  awk -f gen-exercises.awk < $< > $@; \
 	fi
 
 ci: all

diff --git a/README.md b/README.md
@@ -1,4 +1,5 @@
 # Iris Tutorial
+
 The Iris Tutorial is an introduction to the [Iris separation logic framework](https://iris-project.org/) and how to work with its [Rocq formalization](https://gitlab.mpi-sws.org/iris/iris/).
 
 The exposition is intended for a broad range of readers from advanced undergraduates to PhD students and researchers. We assume that readers are already motivated to learn Iris and thus present the material in a bottom-up fashion, rather than starting out with cool motivating examples. The tutorial material is intended to be self-contained. No specific background in logic or programming languages is assumed but some familiarity with basic programming languages theory and discrete mathematics will be beneficial, see e.g. [TAPL](https://www.cis.upenn.edu/~bcpierce/tapl/). Additionally, basic knowledge of the Rocq prover is assumed. Advanced Rocq tactics have been purposefully kept to a minimum, and some proofs are longer than necessary to facilitate learning. We demonstrate more advanced tactics in chapter [ticket_lock_advanced](/theories/ticket_lock_advanced.v).
@@ -11,34 +12,42 @@ The tutorial comes in two versions:
 The tutorial consists of several chapters, each corresponding to a Rocq file. The graph in [Chapter Dependencies](README.md#chapter-dependencies) illustrates possible ways to go through the tutorial. However, the recommended order is specified in the [Recommended Learning Path](README.md#recommended-learning-path).
 
 ## Setup
+
 This version is known to compile with
 
-- Rocq 8.20.1
-- Iris 4.3.0
+- Rocq 9.1.1
+- Iris 4.5.0
 
 The recommended way to install the dependencies is through [opam](https://opam.ocaml.org/doc/Install.html).
 
 1. Install [opam](https://opam.ocaml.org/doc/Install.html) if not already installed (a version greater than 2.0 is required).
 2. Install a new switch and link it to the project. From the root of the repository, execute
-```
+
+```sh
 opam switch create iris_tutorial 5.2.0
 opam switch link iris_tutorial .
 ```
+
 3. Add the Rocq opam repository.
-```
-opam repo add coq-released https://coq.inria.fr/opam/released
+
+```sh
+opam repo add rocq-released https://rocq-prover.org/opam/released
 opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
 opam update
 ```
+
 4. Install the right version of the dependencies as specified in the `iris-tutorial.opam` file.
-```
+
+```sh
 opam install . --deps-only
 ```
 
 ## Editor
+
 Iris makes extensive use of Unicode characters. [This guide](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/editor.md) describes how to set up your favorite editor.
 
 ## Chapter Overview
+
 - [basics](/exercises/basics.v) - Introduction to the separation
   logic and the Iris Proof Mode
 - [pure](/exercises/pure.v) - Distinction between the Rocq context and the Iris context
@@ -64,6 +73,7 @@ Iris makes extensive use of Unicode characters. [This guide](https://gitlab.mpi-
 - [ofe](/exercises/ofe.v) - Detailed introduction to OFEs
 
 ## Chapter Dependencies
+
 ```mermaid
 graph TD;
   basics --> pure;
@@ -104,6 +114,7 @@ graph TD;
 ```
 
 ## Recommended Learning Path
+
 To get a good understanding of the fundamental concepts of Iris, it is recommended to study the following chapters in the given order.
 
 1. [basics](/exercises/basics.v)
@@ -124,13 +135,15 @@ To get a good understanding of the fundamental concepts of Iris, it is recommend
 16. [adequacy](/exercises/adequacy.v)
 
 ## Exercises
+
 To work on the exercises, simply edit the files in the `exercises/` folder. Some proofs and definitions are admitted and marked as `(* exercise *)`---your task is to fill in those definitions and complete the proofs all the way to `Qed`.
 
 After you are done with a file, run `make` (with your working directory being the repository root, where the `Makefile` is located) to compile and check the exercises.
 
 If you are stuck, you can find solutions in the corresponding file in the `theories/` folder.
 
 ## Documentation
+
 This [cheatsheet](/cheatsheet.md) contains a table of the most important tactics for each logical connective. A full description of the Iris Proof Mode tactics can be found in the files [proof_mode.md](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/proof_mode.md) and [heap_lang.md](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/heap_lang.md).
 
 ## Optional Reading
@@ -160,49 +173,63 @@ To contribute, we recommend following these steps:
 For more detailed instructions, see [first-contributions](
 https://github.com/firstcontributions/first-contributions).
 
-### CoqdocJS
-This tutorial uses [CoqdocJS](https://github.com/coq-community/coqdocjs), so please make sure to format your changes accordingly. To see what your changes will look like in the documentation, run
-```
+### RocqdocJS
+
+This tutorial uses [RocqdocJS](https://github.com/rocq-community/rocqdocjs), so please make sure to format your changes accordingly. To see what your changes will look like in the documentation, run
+
+```sh
 git submodule update --init
 make html
 ```
+
 Then open `html/toc.html` in a browser, and navigate to the chapter(s) containing your changes.
 
 ### Generating the Exercises
+
 Note that the files in `exercises/` are generated from the corresponding files in `theories/`. As such, if you wish to make changes to a chapter, please make those changes to the `theories`-version of the chapter. Afterwards, the `exercises`-version can be re-generated by running `make exercises`. This requires `gawk` to be installed (which should be available on Linux, and on macOS can be installed via `brew install gawk`).
 
 The syntax for the solution files is as follows:
 
+```rocq
     (* SOLUTION *) Proof.
       solution here.
     Qed.
+```
 
 is replaced by
 
+```rocq
     Proof.
       (* exercise *)
     Admitted.
+```
 
 and the more powerful
 
+```rocq
     (* BEGIN SOLUTION *)
       solution here.
     (* END SOLUTION BEGIN TEMPLATE
       exercise template here.
     END TEMPLATE *)
+```
 
 is replaced by
 
+```rocq
       exercise template here.
+```
 
 ### Contact
+
 If you have specific requests or questions about the tutorial, please contact:
 
 **Amin Timany**\
 Aarhus University\
 <timany@cs.au.dk>
 
 ### Contributors
+
 Below is a list of people who have contributed to the tutorial, sorted by last name. If you have contributed to the project, please add yourself to the list.
 
 **Lars Birkedal**\

diff --git a/TODO.md b/TODO.md
@@ -1,10 +1,12 @@
 # Fixes
+
 - The chapter [gr_predicates.v] does actually not talk about guarded fixpoints, only least fixpoints
 - Clean up proofs in some chapters
   - Reduce use of SSreflect
   - Simplify proofs
 
 # Possible future topics
+
 - Chapter on prophecies
 - Chapter on HOCAP-style specifications
 - Chapters "Linked List", "Arrays", and "Merge Sort" all use list functionality from std++ (e.g. fmap and lookup). These should be introduced beforehand, for example in an appendix, with the chapters referring to the appendix.
@@ -24,5 +26,6 @@
 - How to define logical relations models of type systems in Iris.
 
 # Features
-- Make tutorial accessible as an interactive webpage (jscoq)
-  - See e.g. https://jscoq.github.io/ext/sf/
+
+- Make tutorial accessible as an interactive webpage (jsrocq)
+  - See e.g. <https://jsrocq.github.io/ext/sf/>
diff --git a/_CoqProject → _RocqProject b/_CoqProject → _RocqProject
diff --git a/coqdocjs/README.md b/coqdocjs/README.md
diff --git a/coqdocjs/example/.gitignore b/coqdocjs/example/.gitignore
diff --git a/coqdocjs/example/Makefile b/coqdocjs/example/Makefile