diff options
| -rw-r--r-- | README.md | 35 | ||||
| -rw-r--r-- | tuto1/src/g_tuto1.ml4 | 5 |
2 files changed, 38 insertions, 2 deletions
@@ -1,6 +1,41 @@ 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 diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4 index 78deabed94..bd53053ec7 100644 --- a/tuto1/src/g_tuto1.ml4 +++ b/tuto1/src/g_tuto1.ml4 @@ -7,7 +7,8 @@ DECLARE PLUGIN "tuto1_plugin" *) open Ltac_plugin open Pp -(* This one is necessary, to avoid message about missing wit_string *) +(* This module defines the types of arguments to be used in the + EXTEND directives below, for example the string one. *) open Stdarg VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY @@ -68,7 +69,7 @@ END (* When adding a definition, we have to be careful that just the operation of constructing a well-typed term may already change the environment, at the level of universe constraints (which - are recorded in the evd component). The fonction + are recorded in the evd component). The function Constrintern.interp_constr ignores this side-effect, so it should not be used here. *) |