README.md 4.33 KB
Newer Older
Lennard Gäher's avatar
Lennard Gäher committed
1
# Coq development for the Semantics course at Saarland University
Lennard Gäher's avatar
Lennard Gäher committed
2

Lennard Gäher's avatar
Lennard Gäher committed
3
4
5
6
7
This repository contains the Coq code for the Semantics course.
Over the course of the semester, we gradually provide prepared templates.

## Installation Instructions

Lennard Gäher's avatar
Lennard Gäher committed
8
9


Lennard Gäher's avatar
Lennard Gäher committed
10
### Windows
Lennard Gäher's avatar
Lennard Gäher committed
11
Unfortunately, Windows does not support the libraries we use for the course very well. If you can use one of the other operating systems (macOS or Linux), we recommend you do so and follow the instructions below. Otherwise, you can use the VM that can be downloaded from [our CMS](https://cms.sic.saarland/semantics_ws2122/).
Lennard Gäher's avatar
Lennard Gäher committed
12

Lennard Gäher's avatar
Lennard Gäher committed
13
14
15
16
17
18
19
#### VM
The VM, downloadable from [our CMS](https://cms.sic.saarland/semantics_ws2122/), can be imported into VirtualBox (version 6.0 or newer is recommended). The virtual machine is based on Arch Linux and contains a pre-configured Coq setup with CoqIDE. This repository has already been cloned to its Desktop.

The default user and password are `vagrant`. 
Depending on your available system resources, you may want to increase the default amount of RAM and the number of CPU cores in VirtualBox.


Lennard Gäher's avatar
Lennard Gäher committed
20
21
### Linux/macOS

Lennard Gäher's avatar
Lennard Gäher committed
22
23
24
25
26
Clone this repository:
```
git clone https://gitlab.mpi-sws.org/FP/semantics-course.git semantics-code
```

Lennard Gäher's avatar
Lennard Gäher committed
27
28
29
30
31
32
33
34
35
36
37
For the course, we recommend installing Coq through [opam](https://opam.ocaml.org), the OCaml package manager.
To do so, please visit [the `opam` installation guide](https://opam.ocaml.org/doc/Install.html) and follow the instructions.
(Typically, this means you just have to execute the following script:)
```bash
bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
```

Now opam is installed on your machine and we can proceed to install the dependencies for the course.
To do so, please execute the following instructions:

```
Lennard Gäher's avatar
Lennard Gäher committed
38
# we enter the semantics folder we just cloned
Lennard Gäher's avatar
Lennard Gäher committed
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
cd semantics-code

# we create a new "switch", where we will install the dependencies
opam switch create semantics ocaml-base-compiler.4.11.2
eval $(opam env)
opam switch link semantics .

# 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
# you can ignore the warnings that will appear concerning missing fields and the license
make builddep
```

Congratulations, you have now installed all the dependencies and you can start to work with the course materials 🎉


## Using the Coq code

In this repository, you will find all the files from the lecture and templates for your exercise sheets. We will add new files (and solutions)
each week and you can get them by pulling from the repository.

The Coq code is organized in multiple folders and multiple files. To compile, please execute:

```
make
```

**NOTE** Since there are dependencies between the files in this development, you may need to compile some files first (by typing `make`) before you can interactively do proofs other files.



## Modifying the Coq code

To edit the Coq code and complete the exercises, you will need an editor.
There are a number of editors and editor extensions for working with Coq code.
We recommend one of the following three options:

- **VS Coq** VSCoq is an extension of the editor [VS Code](https://code.visualstudio.com). Download [the extension](https://github.com/coq-community/vscoq) and change the the following setting in VS Code:

Change `Coqtop: Bin Path` to `~/.opam/semantics/bin/`.
(That's where your semantics switch should be installed now.)

Lennard Gäher's avatar
Lennard Gäher committed
84
- **CoqIDE** is the "default" IDE for Coq. If you have installed Coq via `opam`, you can run `opam install coqide` to install it. 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.
Lennard Gäher's avatar
Lennard Gäher committed
85
- **Proof General** adds Coq support to Emacs. You can find it [here](https://github.com/ProofGeneral/PG).
Lennard Gäher's avatar
Lennard Gäher committed
86
- **Coqtail** adds Coq support to vim. You can find it [here](https://github.com/whonore/Coqtail).
Lennard Gäher's avatar
Lennard Gäher committed
87
88
89
90
91
92



**NOTE** 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 our [here how to configure them for your editor](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/editor.md).