From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id pBBDl4Ow016548 for ; Sun, 11 Dec 2011 14:47:04 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AokDAD+z5E6K54gDgWdsb2JhbABDhQejKoI/IgEBFiYlgXIBAQQBI1YFCwsaAgUhAgIPAkYGDQEHAhCHdAKjVpBbgTSJI4EWBJRxhUuMXQ X-IronPort-AV: E=Sophos;i="4.71,335,1320620400"; d="scan'208";a="134907661" Received: from rouge.crans.org ([138.231.136.3]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 11 Dec 2011 14:46:59 +0100 Received: from localhost (localhost.crans.org [127.0.0.1]) by rouge.crans.org (Postfix) with ESMTP id 8D2F585E3; Sun, 11 Dec 2011 14:46:57 +0100 (CET) X-Virus-Scanned: Debian amavisd-new at crans.org Received: from rouge.crans.org ([10.231.136.3]) by localhost (rouge.crans.org [10.231.136.3]) (amavisd-new, port 10024) with LMTP id U73DAbwk4pFz; Sun, 11 Dec 2011 14:46:57 +0100 (CET) Received: from [192.168.39.1] (fbx.up7.fr [81.56.96.177]) (using TLSv1 with cipher AES256-SHA (256/256 bits)) (No client certificate requested) by rouge.crans.org (Postfix) with ESMTPSA id 3793885E0; Sun, 11 Dec 2011 14:46:57 +0100 (CET) Message-ID: <4EE4B450.60409@glondu.net> Date: Sun, 11 Dec 2011 14:46:56 +0100 From: =?UTF-8?B?U3TDqXBoYW5lIEdsb25kdQ==?= User-Agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.24) Gecko/20111114 Icedove/3.1.16 MIME-Version: 1.0 To: Alain Frisch CC: Gabriel Scherer , Wojciech Meyer , =?UTF-8?B?SsOpcsOpbWllIERpbWlubw==?= , caml-list@inria.fr References: <55531934-37A5-4CC5-AB67-20CE4CCE8269@googlemail.com> <4EE37070.4010702@inria.fr> <1323541702.32136.8.camel@aurora> <1323550544.32136.19.camel@aurora> <4EE4AFB8.5040509@frisch.fr> In-Reply-To: <4EE4AFB8.5040509@frisch.fr> X-Enigmail-Version: 1.1.2 OpenPGP: id=49881AD3 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id pBBDl4Ow016548 Subject: Re: [Caml-list] Camlp4/p5 type reflection [was: OCaml maintenance status / community fork (again)] Le 11/12/2011 14:27, Alain Frisch a écrit : > My understanding (please correct me if I'm wrong) is that Coq uses > camlp{4,5} only as an extensible parser library in order to parse its > own language (which can be extended with user-defined notations). In > particular, Coq does not use the following camlp{4,5} features: > > [1] the revised OCaml syntax > [2] the alternative representation of OCaml AST > [3] the Camlp4 grammar definitions for OCaml syntax(es) > [4] quotations/antiquotations to produce fragments of the OCaml AST > [5] OCaml syntax extensions to define grammar entries > [6] custom OCaml syntax extension for the Coq source code itself > (or maybe only very simple one, like macro/conditional compilation?) As far as I know, Coq uses: [1,2,3] not at all [4] a bit (e.g. tactics/tauto.ml4) [5] a lot (e.g. most of *.ml4 files) [6] for macros and conditional compilation indeed > I wonder how much energy it would take to create a stand-alone > extensible parser library, implemented in pure OCaml (normal syntax), > and following a similar API and semantics as camlp{4,5}, on which Coq > parsing could be built. The same library could be used as a foundation > for future versions of camlp{4,5}. It would be a simple library, with > no external dependency (in particular, no dependency to the OCaml > internals), and very little maintenance burden. I've heard of some attempts to port Coq to dypgen, but since no public announcement was made, I guess this is quite difficult... Are there other such libraries? It's not really Coq's business to create a new one... Cheers, -- Stéphane