Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] About camlp5 and coq


Chronological Thread 
  • From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] About camlp5 and coq
  • Date: Tue, 8 Nov 2016 14:26:07 +0100

On 08/11/2016 10:59, Kakadu wrote:
> 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).

I know I'm biased, but I'd rather think the exact opposite. I think
you're merging two things here.

We should get rid of CAMLPX for **OCaml file processing** as quickly as
possible, for CAMLP4 is already in good way of zombification, and even
CAMPL5 is lagging behind OCaml syntax by several versions (no local
opens, no GADTs, ...). Switching to PPX won't affect any Coq user,
except if they write ML plugins. In the latter case they already have
enough reasons to hate Coq devs at each new release not to care about a
minor preprocessing detail which is fixed by a handful of sed
invocations in **ML files**. Furthermore, there is no possible bugs out
of that, if the preprocessed code compiles, then it works. If we do
something silly we would realized it immediately.

The use of CAMLPX as a parsing engine is a totally unrelated matter, and
there is no plan to get rid of it in a near future. This is indeed a
serious implementation detail that can break **Coq** source code in a
gazillion of ways. I'm indeed thinking about embedding our own
stripped-down version of CAMLP5 parsing engine to have more control on
it, but that's about it.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page