Add VsCoq instructions

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