From: Arnaud Spiwack <aspiwack@lix.polytechnique.fr>
To: Alain Frisch <alain@frisch.fr>
Cc: "Gabriel Scherer" <gabriel.scherer@gmail.com>,
"Wojciech Meyer" <wojciech.meyer@googlemail.com>,
"Jérémie Dimino" <jeremie@dimino.org>,
caml-list@inria.fr
Subject: Re: [Caml-list] Camlp4/p5 type reflection [was: OCaml maintenance status / community fork (again)]
Date: Sun, 11 Dec 2011 14:36:35 +0100 [thread overview]
Message-ID: <CAMoPVjfRFKijY0tGvgDCx7jaqH++DaJg0JtV0VV8aHWgZUtpzQ@mail.gmail.com> (raw)
In-Reply-To: <4EE4AFB8.5040509@frisch.fr>
[-- Attachment #1: Type: text/plain, Size: 865 bytes --]
> 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:
>
This is not entirely correct. Coq uses camlp4's extensible ocaml syntax in
quite a bit of its code. (though less than it use to, I hear). The
following features are used:
- the alternative representation of OCaml AST
> - the Camlp4 grammar definitions for OCaml syntax(es)
> - quotations/antiquotations to produce fragments of the OCaml AST
> - OCaml syntax extensions to define grammar entries
> - custom OCaml syntax extension for the Coq source code itself
>
Though quotations are used *very* sparsely (mostly in legacy code, they are
not maintained).
Arnaud Spiwack
[-- Attachment #2: Type: text/html, Size: 1251 bytes --]
next prev parent reply other threads:[~2011-12-11 13:37 UTC|newest]
Thread overview: 78+ messages / expand[flat|nested] mbox.gz Atom feed top
2011-12-08 9:10 [Caml-list] OCaml maintenance status / community fork (again) Benedikt Meurer
2011-12-08 9:54 ` Alain Frisch
2011-12-08 10:28 ` Benedikt Meurer
2011-12-08 10:46 ` Alain Frisch
2011-12-08 11:08 ` Benedikt Meurer
2011-12-08 16:42 ` Fabrice Le Fessant
2011-12-08 10:47 ` ivan chollet
2011-12-08 14:07 ` oliver
2011-12-08 11:11 ` Pierre-Alexandre Voye
2011-12-08 18:18 ` Török Edwin
2011-12-09 21:42 ` oliver
2011-12-08 10:16 ` Gabriel Scherer
2011-12-08 11:07 ` Stéphane Glondu
2011-12-09 2:11 ` Jacques Garrigue
2011-12-09 10:37 ` Jérémie Dimino
2011-12-09 11:03 ` Gabriel Scherer
2011-12-09 11:17 ` Stefano Zacchiroli
2011-12-09 11:50 ` Jonathan Protzenko
2011-12-09 12:36 ` Alain Frisch
2011-12-09 23:22 ` Goswin von Brederlow
2011-12-09 22:33 ` oliver
2011-12-09 14:24 ` Benedikt Meurer
2011-12-09 17:00 ` Mehdi Dogguy
2011-12-09 17:36 ` Benedikt Meurer
2011-12-09 17:45 ` Mehdi Dogguy
2011-12-09 23:24 ` Goswin von Brederlow
2011-12-10 9:31 ` Benedikt Meurer
2011-12-10 14:45 ` Xavier Leroy
2011-12-10 15:58 ` Benedikt Meurer
2011-12-12 10:21 ` Xavier Leroy
2011-12-12 10:59 ` Benedikt Meurer
2011-12-12 12:20 ` Mehdi Dogguy
2011-12-12 15:17 ` Goswin von Brederlow
2011-12-19 4:09 ` Romain Beauxis
2011-12-19 17:35 ` Alain Frisch
2011-12-12 12:57 ` Gerd Stolpmann
2011-12-10 17:06 ` Török Edwin
2011-12-10 18:28 ` Jérémie Dimino
2011-12-10 18:34 ` Wojciech Meyer
2011-12-10 19:10 ` Wojciech Meyer
2011-12-10 20:55 ` Jérémie Dimino
2011-12-10 21:40 ` [Caml-list] Camlp4/p5 type reflection [was: OCaml maintenance status / community fork (again)] Wojciech Meyer
2011-12-10 23:34 ` Gabriel Scherer
2011-12-11 0:47 ` [Caml-list] Camlp4/p5 type reflection [ Wojciech Meyer
2011-12-11 11:19 ` Gabriel Scherer
2011-12-11 18:14 ` Jérémie Dimino
2011-12-11 9:04 ` [Caml-list] Camlp4/p5 type reflection [was: OCaml maintenance status / community fork (again)] Stéphane Glondu
2011-12-11 9:36 ` Török Edwin
2011-12-11 10:29 ` Gabriel Scherer
2011-12-11 11:23 ` Gerd Stolpmann
2011-12-11 11:38 ` Gabriel Scherer
2011-12-11 10:20 ` Fabrice Le Fessant
2011-12-11 10:47 ` Gabriel Scherer
2011-12-11 13:27 ` Alain Frisch
2011-12-11 13:35 ` Gabriel Scherer
2011-12-11 13:42 ` Alain Frisch
2011-12-11 13:36 ` Arnaud Spiwack [this message]
2011-12-11 13:46 ` Stéphane Glondu
2011-12-10 23:28 ` [Caml-list] OCaml maintenance status / community fork (again) Jesper Louis Andersen
2011-12-11 11:02 ` Gerd Stolpmann
2011-12-13 19:36 ` oliver
2011-12-14 12:13 ` Gerd Stolpmann
2011-12-16 10:03 ` Stéphane Glondu
2011-12-11 13:33 ` Goswin von Brederlow
2011-12-11 13:59 ` [Caml-list] Community distribution [was: OCaml maintenance status / community fork (again)] Benedikt Meurer
2011-12-12 17:48 ` [Caml-list] OCaml maintenance status / community fork (again) Stéphane Glondu
2011-12-13 20:39 ` [Caml-list] New experimental ARM backend [was: OCaml maintenance status / community fork (again)] Benedikt Meurer
2011-12-14 9:18 ` Mark Shinwell
2011-12-14 21:51 ` Benedikt Meurer
2011-12-18 11:57 ` [Caml-list] " Benedikt Meurer
2011-12-18 13:08 ` Benedikt Meurer
2011-12-18 14:50 ` Alexandre Pilkiewicz
2011-12-18 16:42 ` Benedikt Meurer
2011-12-18 17:23 ` Stéphane Glondu
2011-12-21 10:11 ` [Caml-list] " Benedikt Meurer
2011-12-18 13:16 ` [Caml-list] " Benedikt Meurer
2011-12-17 18:36 ` [Caml-list] OCaml maintenance status / community fork (again) Stéphane Glondu
2011-12-18 4:25 ` Till Varoquaux
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=CAMoPVjfRFKijY0tGvgDCx7jaqH++DaJg0JtV0VV8aHWgZUtpzQ@mail.gmail.com \
--to=aspiwack@lix.polytechnique.fr \
--cc=alain@frisch.fr \
--cc=caml-list@inria.fr \
--cc=gabriel.scherer@gmail.com \
--cc=jeremie@dimino.org \
--cc=wojciech.meyer@googlemail.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox