The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

How hard would it be to set up the syntax plugins already in Coq so that they registered vernaculars such as [Declare NatSyntax for nat in nat_scope [O S].] and similarly for notations for negative numbers, ascii, strings, etc?

On Sun, Feb 21, 2016 at 10:12 AM, Assia Mahboubi <Assia.Mahboubi AT inria.fr> wrote:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hello,

Le 20/02/2016 01:08, Pierre-Marie Pédrot a écrit :

> Out of curiosity, what prevents you from writing / using a plugin?

My 5 cents: it is nice to see plugins as user-defined facilities that increase
the proof *assistant* code base of Coq.

But parsers are definitely part of the trusted code base. And I agree with the
other contributors to this thread that in the current state of affairs, it is
not so easy to assess the reliability of third-party plugins.

That being said, I have no concrete suggestion on how to improve the situation
concretely. Is there any hope that one day tools like Cybele/Mtac could come
at the rescue?

Anyway, for what it's worth, I wrote such a plugin during last year's Coding
Sprint, with the help of Pierre Boutillier. I just cleaned it up a bit and
made it independent from its original context so that it can serve as a
documentation stub: https://github.com/amahboubi/coq-num-notations

Best,

assia
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.22 (GNU/Linux)

iQIcBAEBAgAGBQJWydPkAAoJEFY7bbrolXGxYRoP/j1//TFFdYVPRA23mfyPuAsz
g74XI1++tqE8BPPxtuBDgm+aOGMfng1ii8/EXNSTxoJaL6N0fz9ACPCB2y//mwmU
AF0TPUJfekYb5Fu2yWaaJ3yh7IOH/4Jytxuofr9biGpWdmf+OaiZe3f9BiRoOlJc
JxMSlqVlWvTnFaiwUKtx8YcccD6XfPXS+grsX3aVK1nhyEyMYNjYkD8Ox+gnbK9d
qbDbybA9U2hzh6jbYBDjTbR99SA7XlVUndLbhXBoF6JfYJL9aIZ0wPfE4CppONNP
W+mXPz1lwQY6glvYkXmHQ5M4rHLRUCJjdtiKosTnT2iTd9dhv1v/OWcLP5ID/V0j
UPWUMEUWs0k6HMHTFROQKJzlyBG0HdZ0rqRyDYTJfEUuNgNqI8ieyfWNHeLTNIIe
z3KtqWaLj44PRp73A7f39igxeNaJJGOKPLJo4g0PmwYOEyzPWyltiOzXDlHOM70N
wiJoR2SildFUJ1T+Va2T1jWiLuKMwNtzQZS5HzB6HYkqGt9tO1UyNsuKaXLNKKfK
yV2cHPNuaPPNgC+TTA4aDP+MjBLuY8adIvXP/6vW/3GUJP7pg9y7djTZlvLM6boQ
Di2Wa3O9/jIHZ5/t5q0IiayRlYUIYuXH2nKa6pVT8oZqfKdOalw4MYVe/rRpTfPE
e7mNpbHRXVKxEARYXvbl
=t5PH
-----END PGP SIGNATURE-----