amethyst
/
semantics-2023
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '3989cb7caa'
${ noResults }
semantics-2023/README.md

2.8 KiB
Raw Blame History

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.0
# 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.

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

VSCode

TODO links to installation instructions for VSCode/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.