The Coq mailing list

[Kakadu <Kakadu AT protonmail.ch>]

Hey, E.

I actually thought about mixing PPX and camlp5 stuff. It seems to be unwise to rewrite everything from camlp5 to PPX in a single release (some unobvious bugs will appear only after release, some conservative guys will be angry; why I'm talking about it, you probably know it already). But explaining camlp5 how to deal with PPX will require some work. It's not obvious how difficult it will be.....

Happy hacking,

Kakadu

-------- Original Message --------

Subject: Re: [Coq-Club] About camlp5 and coq

Local Time: November 4, 2016 9:32 PM

UTC Time: November 4, 2016 6:32 PM

From: e+coq-club AT x80.org

To: Kakadu <Kakadu AT protonmail.ch>

coq-club AT inria.fr

Hi Kakadu,

others can talk more about camlp5, I'll comment on PPX and Coq.

Kakadu <Kakadu AT protonmail.ch> writes:

> AFAIU coq is the main user of camlp5 and there are rumors that lack of

> attributes in camlp5 forbids using PPX rewriters in Coq (but this

> feature is desired).

This is not true, as long as you don't mix camlp4 files and PPX in

dangerous ways. For more details see the thread in coq-dev "OCaml

version for 8.6", dated: 26 Feb 2016.

Pierre-Marie Pédrot has indeed a proof of concept porting the plugin

mechanism to PPX, see thread "PPX proof-of-concept" dated 8 Aug 2016 in

coq-dev, also both my projects (SerAPI and jsCoq) make extensive use of

ppx and Coq without any issue.

Best,

E.