On February I am teaching a short course on Rocq. The course will focus on some basic notions of formalization techniques using dependent types. This page contains some basic resources for the course.

First, let us check some basic installation steps, so you can run/compile code on your local machine.

Installation

For a more robust interfacing, it is recommended to get Rocq installed locally. The official Rocq page is https://rocq-prover.org, and it contains a lot of resources for beginners and specific installation instruction for your platform, including Windows.

For instance https://rocq-prover.org/docs list a lot of learning tools, books, and tutorials for users at different levels.

Installing Opam

Rocq itself is implemented in the Ocaml programming language, and as such, most of its libraries are managed by OCaml’s own package manager: opam. Opam is natively supported by most operating systems natively while Windows is fully supported since opam 2.2.

Fresh Install

For detailed instructions, please check https://opam.ocaml.org/doc/Install.html. Here, I will provide the very basic commands to install it, and if you need more detailed instructions or use a specific version of linux, please refer back to the aforementioned link.

• Windows
• macOS

• On the powershell on windows, use winget to install opam.

  winget install Git.Git OCaml.opam
  

  WinGet, the Windows Package Manager, is available on Windows 11 and later versions of Windows 10. See the official documentation for additional info.

• On macOS brew is your easiest option.

  brew install opam
  

Initializing opam

The first thing to do after installing opam is to initialize the local environment.

opam init

Upgrading from an older (forgotten) opam setup

Delete old opam switches and configurations

rm -rf ~/.opam

reinitialize opam

opam init

Installing Rocq

With opam initialized, we can install (the latest) version of rocq by simply:

opam install rocq-prover

The editor

To use an editor you will need the rocq-language-server package from opam.

opam install vsrocq-language-server

The setup for the course is as follows:

• Visual Studio Code
  • Mandatory Extension
    • VsRocq
  • Optional Extensions
    • vs-code-icons
    • Unicode Shortcuts

Project Setup

There are two ways of compiling Rocq’s files:

• the _CoqProject file, which generates a make file for your project based on a specific syntax. See Building Rocq Projects page for details. This is the older way of building coq projects.
• for modern projects, I recommend building projects using Dune. See The Rocq Prover Builder Language page on Dune’s documentation for a detailed instruction on how to setup a project from scratch. In the short course we are going to use dune to build the projects. To install dune on your machine you simply use opam.

  opam install dune
  

Lectures

Lecture 0 – Inductively Defined Types

Materials for the lectures will be added soon.

Extra Exercises

Lecture 1 – Natural Numbers

Rocq files