The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

Somehow, a question is also whether it would be worth that someone
eventually provides a generic-enough quote function in Coq, for use at
both the vernac level or the plugin level.

My understanding of the Gross-Erbsen-Chlipala ITP 2018
reification-by-parametricity paper is that this quote function almost
already exists, it is "pattern". Then, what about going in the
direction of providing a variant of "pattern" which encapsulates the
boilerplate of the technique and which, maybe, also abstracts over the
foreign subterms?

Idem at the plugin level. Already e.g. ring, micromega, btauto have
their own reification mechanisms (sometimes even in Ltac) and this
seems suboptimal.

Best,

Hugo

On Fri, Jul 20, 2018 at 11:45:32AM -0700, John Wiegley wrote:
> I would also support dropping Quote; each time I've been able to use it, I
> ended up just copying Ltac macros from existing templates so I would have 
> the
> configurability needed for future changes.

On Fri, Jul 20, 2018 at 08:41:28AM -0400, Tej Chajed wrote:
> I definitely support getting rid of Quote. I used it once and then ran into 
> an
> issue: my unquote function took a type parameter, which is unsupported, 
> even if
> you try specializing it. I talked to Jason Gross, copied some code from 
> their 
> reification-by-parametricity paper, and got it working fairly easily in pure
> Ltac.
> 
> It would be great to have some examples from that paper coped into the Coq 
> test
> suite and try to give it visibility, instead of maintaining Quote. It's a 
> more
> powerful technique and I believe with just a little boilerplate can replace
> uses of Quote (if anybody actually weighs in and is using it).
> 
> On Fri, Jul 20, 2018 at 3:20 AM Maxime Dénès 
> <mail AT maximedenes.fr>
>  wrote:
> 
>     Dear Coq-clubbers,
> 
>     I'm trying to clean up the set of plugins shipped with Coq, so that we
>     can make the maintenance done by the development team more focused and
>     effective.
> 
>     I was wondering if anybody was using the Quote plugin in real-world
>     developments. See https://github.com/coq/coq/pull/7894 for more context.
> 
>     Thank you in advance for your feedback!
> 
>     Maxime.
>