From 38a2cffd4c3a656462b71404c4706049f074f56d Mon Sep 17 00:00:00 2001
From: mueck <mueck@mpi-sws.org>
Date: Mon, 16 Oct 2023 16:34:13 +0200
Subject: [PATCH] Add VsCoq instructions

---
 README.md | 27 ++++++++++++++++++++++-----
 1 file changed, 22 insertions(+), 5 deletions(-)

diff --git a/README.md b/README.md
index 5693fb4..0233f9e 100644
--- a/README.md
+++ b/README.md
@@ -23,7 +23,7 @@ cd semantics-2023
 
 # We create a new "switch" to install the dependencies in. Switches are independent 
 # installation prefixes with their own set of installed packages.
-opam switch create semantics ocaml-base-compiler.4.14.0
+opam switch create semantics ocaml-base-compiler.4.14.1
 # We tell opam to automatically enable the switch `semantics` in this directory
 opam switch link semantics .
 eval $(opam env)
@@ -51,7 +51,7 @@ make -j4
 
 
 ## Editing the Coq code
-To edit the Coq code and complete the exercises, you will need an editor. We recommend you use [CoqIDE](https://coq.inria.fr/refman/practical-tools/coqide.html) or [VSCoq](https://github.com/coq-community/vscoq) ([VSCode](https://code.visualstudio.com/)).
+To edit the Coq code and complete the exercises, you will need an editor. We recommend you use [CoqIDE](https://coq.inria.fr/refman/practical-tools/coqide.html) or [VsCoq](https://github.com/coq-community/vscoq) ([VSCode](https://code.visualstudio.com/)).
 
 ### CoqIDE
 
@@ -60,8 +60,25 @@ To install CoqIDE, run the following command:
 opam install coqide
 ```
 
-### VSCode
+You need the GTK+-development libraries installed for that on your system (`gtksourceview3`). Starting with version 2.1, `opam` should automatically ensure that on most operating systems. If that does not work, you may need to install them yourself, depending on your system.
 
-TODO links to installation instructions for VSCode/VSCoq
+### VsCoq
 
-If you're using WSL for Coq then you will want to use VSCoq (VSCode) because it integrates well with WSL. For instructions on how to set this up, see [here](https://code.visualstudio.com/docs/remote/wsl).
+[VsCoq](https://github.com/coq-community/vscoq) is an extension of the editor [VS Code](https://code.visualstudio.com). Download and install instructions can be found [here](https://marketplace.visualstudio.com/items?itemName=maximedenes.vscoq).
+
+We recommend that you install the version 0.3.9 by running:
+```bash
+code --install-extension maximedenes.vscoq@0.3.9
+```
+Then change `Coqtop: Bin Path` to `~/.opam/semantics/bin/` in the extension settings.
+(That's where your semantics switch should be installed now.)
+
+There is also a newer version VsCoq 2 with new features that you can use instead. Our experience is that the older version is a bit more performant than the new version, but that might change during the course.
+
+If you're using WSL for Coq then you will want to use VsCoq (VSCode) because it integrates well with WSL. For instructions on how to set this up, see [here](https://code.visualstudio.com/docs/remote/wsl).
+
+### Important for all editors
+
+Many of the Coq files use unicode notation for symbols. For example,
+instead of writing `nat -> nat -> nat`, we typically write `nat → nat → nat`.
+You can find out [here how to configure them for your editor](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/editor.md).