coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Anybody uses the Quote plugin?

From: Tej Chajed <tchajed AT mit.edu>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Anybody uses the Quote plugin?
Date: Fri, 20 Jul 2018 08:41:28 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tchajed AT mit.edu; spf=Pass smtp.mailfrom=tchajed AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-4.mit.edu
Ironport-phdr: 9a23:Li4gMB2Rinm71TUjsmDT+DRfVm0co7zxezQtwd8Zse0TLfad9pjvdHbS+e9qxAeQG9mDtbQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYghEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLnhykHODw5/m/ZicJ+kbxVrw66qhNl34LZepuYOOZicq7fe94RWGpPXtxWVyxEGo6ycZUAD+gcNutGr4nyvVkOogWjCgKxA+7v1iNHhn/s0q04zesuDBrL3AkhH9ISqnjbssj6NLoLXO2z0aLGwzLDb/ZM1jf87ojFah8hofCQXbJwbMre0lMjGB/CjlWVsYDlOjKV1vgXv2eF8uVgSOSigHMkpQFpujWj28QhhpPNi44P1FzJ9T91zJs1KNGgVkJ3fdqpHIFTuiyaLYd6XN4uTmNytConyLAKpJi2dzUQxps93R7QcfmHfpCI4h39UOaRJi91i29geLO+nhqy9FKvyuz4VsmvzllFsjNJksLQuX8X0RzT7NaISuFk8kquwzqP0gHT6v1eLU8qiKXbNoYtwr82lpUNrUTOBjL6lUbsgKKSbEko5Oil5/76brjmvpOcMpV7igD6MqQggMy/BuE4PxASX2eH+eSzzr/j8lPkT7hRi/02k7XZvIrEKssGu661GxVV3Zo76xajEzem18wVkmUALFJcYR6Ik4zpO0zVL/3jFve+g1GskC9xyPzcP73hBI/NLnnZn7v7c7Z98R0U9A1mxtdGoplQF7tJdPn0Qwr6sMHSJh4/KQ29hej9XoZTzIQbDF6CAOeyMKrQvFPAsv4kI+COaYM9vTfhbfUp+qi93jcChVYBcPzxjtMsY3eiE6E+ehTLUT/Xmt4EVFwykE87Re3uhkeFVG8BYneuGa8w+2NiUd70PcL4XomoxYe58mKjBJQHNGVHFhaBHWq6L9zZCcdJUzqbJ4paqhJBVbWlTNR4hx2rpkr/wrtjNeffvzYTvJTl2cIwu6vWlA10+DBpXZyQ

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.

[Coq-Club] Anybody uses the Quote plugin?, Maxime Dénès, 07/20/2018
- Re: [Coq-Club] Anybody uses the Quote plugin?, Tej Chajed, 07/20/2018
  - Re: [Coq-Club] Anybody uses the Quote plugin?, John Wiegley, 07/20/2018
  - Re: [Coq-Club] Anybody uses the Quote plugin?, Hugo Herbelin, 07/22/2018
    - Re: [Coq-Club] Anybody uses the Quote plugin?, Matthieu Sozeau, 07/23/2018
      - Re: [Coq-Club] Anybody uses the Quote plugin?, Jason Gross, 07/27/2018
    - Re: [Coq-Club] Anybody uses the Quote plugin?, Christian Doczkal, 07/31/2018