Skip to content
This repository has been archived by the owner. It is now read-only.
A collection of small projects to illustrate how to write plugins for Coq
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
tuto0
tuto1
tuto2
tuto3
.gitignore
.travis.yml
LICENSE
README.md

README.md

This site is now frozen

This development has moved to the Coq repository in directory doc/plugin_tutorials. For the master branch you can access at https://github.com/coq/coq/tree/master/doc/plugin_tutorial.

How to write plugins in Coq

Working environment : merlin, tuareg (open question)

OCaml & related tools

These instructions use OPAM

opam init --root=$PWD/CIW2018 --compiler=4.06.0 -j2
eval `opam config env --root=$PWD/CIW2018`
opam install camlp5 ocamlfind num # Coq's dependencies
opam install lablgtk              # Coqide's dependencies (optional)
opam install merlin               # prints instructions for vim and emacs

Coq

git clone git@github.com:coq/coq.git
cd coq
./configure -profile devel
make -j2
cd ..
export PATH=$PWD/coq/bin:$PATH

This tutorial

git clone git@github.com:ybertot/plugin_tutorials.git
cd plugin_tutorials/tuto0
make .merlin                # run before opening .ml files in your editor
make                        # build

tuto0 : basics of project organization

package a ml4 file in a plugin, organize a Makefile, _CoqProject

  • Example of syntax to add a new toplevel command
  • Example of function call to print a simple message
  • Example of syntax to add a simple tactic (that does nothing and prints a message)
  • To use it:
    cd tuto0; make
    coqtop -I src -R theories Tuto0

In the Coq session type:

    Require Import Tuto0.Loader. HelloWorld.

tuto1 : Ocaml to Coq communication

Explore the memory of Coq, modify it

  • Commands that take arguments: strings, symbols, expressions of the calculus of constructions
  • Commands that interact with type-checking in Coq
  • A command that adds a new definition or theorem
  • A command that uses a name and exploits the existing definitions or theorems
  • A command that exploits an existing ongoing proof
  • A command that defines a new tactic

Compilation and loading must be performed as for tuto0.

tuto2 : Ocaml to Coq communication

A more step by step introduction to writing commands

  • Explanation of the syntax of entries
  • Adding a new type to and parsing to the available choices
  • Handling commands that store information in user-chosen registers and tables

Compilation and loading must be performed as for tuto1.

tuto3 : manipulating terms of the calculus of constructions

Manipulating terms, inside commands and tactics.

  • Obtaining existing values from memory
  • Composing values
  • Verifying types
  • Using these terms in commands
  • Using these terms in tactics
  • Automatic proofs without tactics using type classes and canonical structures

compilation and loading must be performed as for tuto0.

You can’t perform that action at this time.