Tutorial: write a script in Coq

We will explain how to write scripts in Coq with the example of repos2web, a website generator. This generator parses an OPAM repository with Coq packages (for example, the repo-stable) and generates an HTML page (see the repo-stable page).

Get started

We first create an empty Coq project. Add the following files in a new directory:

• configure.sh:

  #!/bin/sh

  coq_makefile -f Make -o Makefile

• Make:

  -R src Repos2Web

  src/Main.v

• src/Main.v:

  ...