aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-02 15:06:17 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-02 15:06:17 +0200
commit02fe76c0c1c3f01c6fb4310dd4450b35f43005da (patch)
tree1d1c7c47fff5688105d0f868f9ab89d479ede899 /dev/doc
parentf6f606232ae3c32e5c90d4fd427721875529b777 (diff)
parent47bbe39d480f02dc92e4856fa8d872f52b9903a4 (diff)
Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points of Camlp5
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/changes.md44
1 files changed, 44 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index e6d741159..4177513a1 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -93,6 +93,50 @@ Primitive number parsers
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