From 50d55ecc6c2fd91a71bbe5f6a1beeab97fa2a0d1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Jun 2018 17:14:18 +0200 Subject: Documenting the transition strategy of GEXTEND. --- dev/doc/changes.md | 44 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) (limited to 'dev') diff --git a/dev/doc/changes.md b/dev/doc/changes.md index cbb95625f..c140c67b0 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -87,6 +87,50 @@ Vernacular commands The test suite now allows writing unit tests against OCaml code in the Coq code base. Those unit tests create a dependency on the OUnit test framework. +### Transitioning away from Camlp5 + +In an effort to reduce dependency on Camlp5, the use of Camlp5 GEXTEND macro +is discouraged. Most plugin writers do not need this low-level interface, but +for those who do, the transition path is somewhat straightforward. To convert +a ml4 file containing only standard OCaml with GEXTEND statements, the following +should be enough: +- replace its "ml4" extension with "mlg" +- replace GEXTEND with GRAMMAR EXTEND +- wrap every occurrence of OCaml code into braces { } + +For instance, code of the form +``` +let myval = 0 + +GEXTEND Gram + GLOBAL: my_entry; + +my_entry: +[ [ x = bar; y = qux -> do_something x y + | "("; z = LIST0 my_entry; ")" -> do_other_thing z +] ]; +END +``` +should be turned into +``` +{ +let myval = 0 +} + +GRAMMAR EXTEND Gram + GLOBAL: my_entry; + +my_entry: +[ [ x = bar; y = qux -> { do_something x y } + | "("; z = LIST0 my_entry; ")" -> { do_other_thing z } +] ]; +END +``` + +Currently mlg files can only contain GRAMMAR EXTEND statements. They do not +support TACTIC, VERNAC nor ARGUMENT EXTEND. In case you have a file containing +both kinds at the same time, it is recommended splitting it in two. + ## Changes between Coq 8.7 and Coq 8.8 ### Bug tracker -- cgit v1.2.3