March 4, 2015
We will explain how to write scripts in Coq using the library Coq.io with the example of repos2web, a website generator. This generator parses an OPAM repository with Coq packages and generates an HTML page.
opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-io-system
Create an empty Coq project by adding the following files in a fresh directory:
configure.sh, the configure script:
#!/bin/sh coq_makefile -f Make -o Makefile
coq_makefile project file:
-R src Repos2Web src/Main.v
src/Main.v, the main source file:
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, the Makefile for the extracted program:
build: ocamlbuild repos2web.native -use-ocamlfind -package io-system clean: ocamlbuild -clean
Compile your Coq code to OCaml:
Compile and run the generated OCaml:
cd extraction/ make ./repos2web.native
This should print you the message
test on the terminal!
To write our script we need to understand the basis of how OPAM for Coq repositories are organized (for example in opam-coq-archive). All the packages are in the
packages folders. There is one folder per package name, all prefixed by
coq- because we are in the Coq namespace. In each package folder, there is one folder per version of the package with three files
url to describe the package.
packages/ coq-list-string/ coq-list-string.1.0.0/ descr opam url coq-list-string.2.0.0/ ... ...
We define the data type of an OPAM repository in src/Model.v. In a first pass, we will generate an element of type
Packages.t. This is a list of packages described by a name and a list of versions. In a second pass, we will generate an element of type
FullPackages.t, by adding the description of each version and by computing each latest version using the (complex) Debian ordering.
The first pass is described in src/Main.v in the
Basic module. The function
list_coq_files lists the files/folders which are starting with the
coq- prefix in a given
Definition list_coq_files (folder : LString.t) : C (option (list Name.t)) := let! folders := System.list_files folder in match folders with | None => do! log (LString.s "The folder " ++ folder ++ LString.s " cannot be listed.") in ret None | Some folders => ret (Some (Name.of_strings folders)) end.
Let us precise the return type
C (option (list Name.t)). We defined
Definition C := C.t System.effects.
for convenience. This means than
C is the type of computations doing interactions with the system. We need to use this special type because Coq is a purely functional language: without using the type
C, functions cannot do inputs–outputs.
C is parametrized by
option (list Name.t), the result type of the function. Thus, the result of
list_coq_files can be either:
Nonein case of error,
As described in Tutorial: a Hello World in Coq, we use the
let! operator to combine computations and the
ret operator to return a pure value. We interact with the system by calling the following functions:
list_files : LString.t -> C (option (list LString.t)): list the content of a folder
log : LString.t -> C unit: print a message on the terminal
The complete list of system functions is available on system API.
We continue by defining more functions and conclude with:
Definition get_packages (repository : LString.t) : C (option Packages.t) := let! names := list_coq_files repository in match names with | None => ret None | Some names => get_packages_of_names repository names end.
to get the list of packages in a repository folder (or
None in case of error).
The second pass follows the same structure as the first one. The main trick is the function:
(** Return the latest version, using Debian `dpkg` for comparison. *) Definition max_version (version1 version2 : Version.t) : C (option Version.t) := ...
which uses the
dpkg command line tool to compare two versions numbers according to the Debian ordering. If you want to test it, the
dpkg tool should be available on most Linux distribution, even on those which are not based on Debian.
We define the HTML rendering in src/View.v. The last function is:
Definition index (packages : FullPackages.t) : LString.t := header ++ title packages ++ table packages ++ footer.
which pretty-prints a list of packages to HTML. This function is pure (no inputs–outputs), because the return type is not
C of something but
LString.t. There is nothing special about the pretty-printing, and we generate the page using the Bootstrap CSS framework to get a nice rendering.
main function in src/Main.v combines the parsing and the rendering to write the output file in
Definition main (argv : list LString.t) : C unit := match argv with | [_; repository] => let repository := repository ++ LString.s "/packages" in let! packages := Basic.get_packages repository in match packages with | None => log (LString.s "The packages cannot be listed.") | Some packages => let! full_packages := Full.get_packages repository packages in let index_content := View.index full_packages in let index_name := LString.s "html/index.html" in let! is_success := System.write_file index_name index_content in if is_success then log (index_name ++ LString.s " generated.") else log (LString.s "Cannot generate " ++ index_name ++ LString.s ".") end | _ => log (LString.s "Exactly one argument expected (the repository folder).") end.
We use the list of command line arguments
argv to get the folder in which the OPAM repository is stored. You can add a Coq-ish theme downloading this Bootstrap CSS:
curl -L https://github.com/clarus/coq-red-css/releases/download/coq-blog.1.0.2/style.min.css >html/style.min.css