Skip to content

Commit 912405d

Browse files
update README
1 parent f793420 commit 912405d

2 files changed

Lines changed: 7 additions & 17 deletions

File tree

Makefile

Lines changed: 0 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -41,12 +41,3 @@ ci: all
4141
+@make -B exercises # force make (in case exercise files have been edited directly)
4242
if [ -n "$$(git status --porcelain)" ]; then echo 'ERROR: Exercise files are not up-to-date with solutions. `git diff` and `git status` after re-making them:'; git diff; git status; exit 1; fi
4343
.PHONY: ci
44-
45-
pdf: html
46-
@if ! command -v wkhtmltopdf >/dev/null 2>&1; then \
47-
echo "wkhtmltopdf not found. Running inside nix-shell..."; \
48-
nix-shell -p wkhtmltopdf --run "bash ./generate_pdf.sh"; \
49-
else \
50-
bash ./generate_pdf.sh; \
51-
fi
52-
.PHONY: pdf

README.md

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ The tutorial consists of several chapters, each corresponding to a Rocq file. Th
1515

1616
This version is known to compile with
1717

18-
- Rocq 9.1.1
18+
- Rocq 9.2
1919
- Iris 4.5.0
2020

2121
The recommended way to install the dependencies is through [opam](https://opam.ocaml.org/doc/Install.html).
@@ -24,7 +24,7 @@ The recommended way to install the dependencies is through [opam](https://opam.o
2424
2. Install a new switch and link it to the project. From the root of the repository, execute
2525

2626
```sh
27-
opam switch create iris_tutorial 5.2.0
27+
opam switch create iris_tutorial 5.4.0
2828
opam switch link iris_tutorial .
2929
```
3030

@@ -58,7 +58,7 @@ Iris makes extensive use of Unicode characters. [This guide](https://gitlab.mpi-
5858
- [linked_lists](/exercises/linked_lists.v) - Linked lists
5959
- [later](/exercises/later.v) - The later modality and recursive functions
6060
- [arrays](/exercises/arrays.v) - Arrays in HeapLang
61-
- [gr_predicates](/exercises/gr_predicates.v) - Guarded Recursive Predicates
61+
- [gr_predicates](/exercises/gr_predicates.v) - Guarded Recursive Predicates (TODO: not actually guarded fixpoints, only least)
6262
- [resource_algebra](/exercises/resource_algebra.v) - Introduction to resource algebras
6363
- [invariants](/exercises/invariants.v) - Invariants
6464
- [timeless](/exercises/timeless.v) - Timeless propositions
@@ -178,15 +178,14 @@ https://github.com/firstcontributions/first-contributions).
178178
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
179179

180180
```sh
181-
git submodule update --init
182181
make html
183182
```
184183

185184
Then open `html/toc.html` in a browser, and navigate to the chapter(s) containing your changes.
186185

187186
### Generating the Exercises
188187

189-
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`).
188+
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 `awk` to be installed.
190189

191190
The syntax for the solution files is as follows:
192191

@@ -236,9 +235,9 @@ Below is a list of people who have contributed to the tutorial, sorted by last n
236235
Aarhus University\
237236
<birkedal@cs.au.dk>
238237

239-
**Simon Gregersen**\
240-
Aarhus University\
241-
<gregersen@cs.au.dk>
238+
**Simon Oddrshede Gregersen**\
239+
CISPA Helmholtz Center for Information Security
240+
<gregersen@cispa.de>
242241

243242
**Mathias Adam Møller**\
244243
Aarhus University\

0 commit comments

Comments
 (0)