coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] About camlp5 and coq

From: e+coq-club AT x80.org (Emilio Jesús Gallego Arias)
To: Kakadu <Kakadu AT protonmail.ch>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] About camlp5 and coq
Date: Fri, 04 Nov 2016 19:32:36 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e+coq-club AT x80.org; spf=Neutral smtp.mailfrom=e+coq-club AT x80.org; spf=None smtp.helo=postmaster AT cc-tupan-roaming-b.ensmp.fr
Ironport-phdr: 9a23:rtwChxFKrif4+TQ9bbwgL51GYnF86YWxBRYc798ds5kLTJ76rsqwAkXT6L1XgUPTWs2DsrQf2rCQ4/GrADVeqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2a3IyL0LWR8p7abxgA0Bm0Yrp+MT2utwLNsc8TiIpmbK0xnEjnuHxNLukVzmRxYFmXghzU9pfoupl5/GwQlvcg889HGYf3ZDYjBZNRCDArPGd9zdfqvAKCHljH3WcVTmhDykkAOAPC9hyvBpo=
Organization: X80 Heavy Industries

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.

[Coq-Club] About camlp5 and coq, Kakadu, 11/04/2016
- Re: [Coq-Club] About camlp5 and coq, Emilio Jesús Gallego Arias, 11/04/2016
  - Re: [Coq-Club] About camlp5 and coq, Kakadu, 11/08/2016
    - Re: [Coq-Club] About camlp5 and coq, Pierre-Marie Pédrot, 11/08/2016
    - Re: [Coq-Club] About camlp5 and coq, Emilio Jesús Gallego Arias, 11/08/2016