blob: f82edb2352b9b0dc9a5269a18fc6c0c92ebc5ac5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
How to write plugins in Coq
===========================
# Working environment : merlin, tuareg (open question)
## OCaml & related tools
These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html)
```shell
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
```shell
git clone git@github.com:coq/coq.git
cd coq
./configure -profile devel
make -j2
cd ..
export PATH=$PWD/coq/bin:$PATH
```
## This tutorial
```shell
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:
```bash
cd tuto0; make
coqtop -I src -R theories Tuto0
```
In the Coq session type:
```coq
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`.
|
