-
Notifications
You must be signed in to change notification settings - Fork 1
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).
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
!