Proof Assistants
Course material
Introduction slides
Isabelle material
Coq material
Lecture recordings
Recordings are available via Panopto on the
Moodle page
for the course (click the arrow in the upper right corner to open a sidebar
that contains the videos).
Installation instructions
Installing Isabelle
Installation
The course will use Isabelle 2024. You can download it from its
website, and there are detailed
installation instructions available
here for Linux,
Windows, and macOS (including workarounds for potential issues with
signatures/certificates or anti-virus programs).
IDE
We recommend using the jEdit prover IDE, which comes bundled with Isabelle.
Testing
If everything works well, you should be able to load
this test file
or
that demo file
into Isabelle without any errors.
Installing Coq
Installation
The course will use Coq version 8.18.
The easiest way to install is to use the
Coq platform,
which provides binary installers and installation scripts for all major OS.
In particular, there is a
snap package.
We will only need the
base level (
IDE level if you want to use CoqIDE, see below).
Alternatively, you can use opam (OCaml's package manager) directly if you already are used to it.
In that case, you should follow the instructions from
Coq's website.
IDE
We recommend using
VSCode or
VSCodium with the VSCoq extension.
For the time being,
VSCoq Legacy is the stable
version. A reimplementation,
VSCoq 2, is currently
developed to replace it, however it is still somewhat experimental, so we recommend keeping to VSCoq Legacy for the time being.
Alternatively, you can also use
CoqIDE
which is provided alongside Coq in the Coq Platform, and is also available on opam.
It might work better if you experience issues with VSCode.
If you want to keep using your favourite editor, there might be a Coq extension for it, you can check
this page for more information.
Testing
If everything works well, you should be able to step through this
test file.
