Coq development for the Semantics course 2023 at Saarland University

This repository contains the Coq code for the Semantics course taught by Derek Dreyer at Saarland University in winter semester 23/24. It will be updated throughout the semester as the course progresses.

Installation instructions

Windows

Unfortunately, Windows does not support Coq and the libraries we are using well. If you can use either Linux or MacOS instead, please follow the instructions below. Otherwise we recommend you set up WSL as explained here, proceed with the installation instructions below, and set up VSCode for use with WSL.

Linux/MacOS

We recommend installing Coq through opam, the OCaml package manager. To do so, visit the opam installation guide and follow the instructions.

Next, clone this repository:

git clone https://gitlab.mpi-sws.org/FP/semantics-2023.git

Now proceed to install the dependencies:

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.1
# We tell opam to automatically enable the switch `semantics` in this directory
opam switch link semantics .
eval $(opam env)


# We tell opam where to find the dependencies
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

# We install the dependencies
make builddep

Compiling the Coq code

In this repository you can find the templates for the exercises, files from the lectures, and some auxiliary files. We will make more and more files available as the course progresses.

The Coq code is spread out among multiple files and directories. To compile, run the following command

make -j
# or, alternatively, if you want to restrict the number of threads used:
make -j4

IMPORTANT: You will have to compile to interactively do proofs. You will have to recompile if the dependencies of the file your editing change.

By default, the exercise proofs won't be compiled by the above command. You can still work on them interactively, but if you want make to check them, you can uncomment the respective lines in the _CoqProject file. (We do not add them by default, so `make' will not complain if your proofs of an old exercise do not work.)

Editing the Coq code

To edit the Coq code and complete the exercises, you will need an editor. We recommend you use CoqIDE or VsCoq (VSCode).

CoqIDE

To install CoqIDE, run the following command:

opam install coqide

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.

VsCoq

VsCoq is an extension of the editor VS Code. Download and install instructions can be found here.

We recommend that you install the version 0.3.9 by running:

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.

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.