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:Require Import Coq.Lists.List. Require Import Io.All. Require Import Io.System.All. Require Import ListString.All.

Import ListNotations. Import C.Notations.

(** The main function. *) Definition main (argv : list LString.t) : C.t System.effects unit := System.log (LString.s "test").

(** The extracted program. *) Definition repos2web := Extraction.run main. Extraction "extraction/repos2web" repos2web.

• extraction/Makefile:

build: ocamlbuild repos2web.native -use-ocamlfind -package io-system

clean: ocamlbuild -clean

Install the coq:io:system package with OPAM to enable the system effects:

opam repo add coq-stable https://github.com/coq/repo-stable.git
opam install coq:io:system

Compile your Coq code to OCaml:

./configure.sh
make

Compile and run the generated OCaml:

cd extraction/
make
./repos2web.native

This should print you the message test!