Stream: Coq devs & plugin devs

Topic: Making a new attribute


view this post on Zulip Gregory Malecha (Dec 13 2022 at 12:54):

I'm wondering if it is possible to (and if so if there is any documentation on how to) define a custom attribute that runs additional vernacular after the command generates the new definition. Two examples,

#[hint(db=my_db,level=100)]
Lemma foo : ...
Proof. ... Qed. (* note that here, it is important that the attribute runs after the [Qed] *)

Or

#[deriving(eq_dec)]
Variant t := A | B.

I know that Elpi has a great Deriving command, I'm just wondering if it is possible to put this functionality into an attribute.

view this post on Zulip Enrico Tassi (Dec 13 2022 at 12:56):

As of today, it is not possible. But you are not alone liking the idea

view this post on Zulip Enrico Tassi (Dec 13 2022 at 12:57):

In short, it is not my top priority, otherwise I would try to do it.
What is not trivial is which API/power one wants to expose.

view this post on Zulip Enrico Tassi (Dec 13 2022 at 13:00):

For example #[derive] as Elpi is a plugin, one would need the plugin take over the command very early, to start a module, then declare the inductive and the derives stuff, and finally close the module. That is not trivial to do in a generic way.
While for the hint db one, I believe it is simpler since it is all in Coq proper and all actions would need to be performed after the declaration.

view this post on Zulip Gaëtan Gilbert (Dec 13 2022 at 13:01):

with derive you want the inductive itself to go in the module?

view this post on Zulip Enrico Tassi (Dec 13 2022 at 13:02):

This is what I do in Elpi, and you would write it like this:

derive Variant bla bla.

where derive is a command (written in Elpi) and Variant ... is it's argument. So I can start a module and then declare the inductive inside.

Today it is a module, but I'd rather use a name space if we had it.

view this post on Zulip Enrico Tassi (Dec 13 2022 at 13:04):

A namespace would simplify things, in particular it remove the "time constraint", since you can add stuff in a name space after the facts.

view this post on Zulip Gregory Malecha (Dec 13 2022 at 14:28):

My (likely overly simplified) mental model is the following:

  1. elaboration and type checking produces a "term" (e.g. a constr, a mutual inductive, etc)
  2. introducing a name (possibly including setting visibility, e.g. local, global, export)

It seems like you could replace these steps or introduce new logic between the steps.
Examples:

In the namespace setup, you probably want any new definitions introduced after 3 to be included inside the module, so there might be some need for a special closing setup.

view this post on Zulip Gregory Malecha (Dec 13 2022 at 14:31):

The downside of replacing the whole command (which we do a lot) is that you need to make sure that you don't affect the command in a fundamental manner. For example, you can't (maybe you can now) lock a definition where the body uses nested match because ELPI doesn't support that construct, even though, the idea of locking something is completely parametric in the body.

view this post on Zulip Enrico Tassi (Dec 13 2022 at 15:29):

That one now works (since the 8.16 release) since Elpi lets Coq typecheck the argument, but I see your point, I still have to "simulate" what Coq does (e.g. declare implicit arguments, etc) and it is easy to behave slightly differently...

view this post on Zulip Gregory Malecha (Dec 13 2022 at 16:17):

On friday I ran into something where I had Definition foo : forall {a}, ... := @X and i wasn't ending up with the implicit annotation on a

view this post on Zulip Gregory Malecha (Dec 13 2022 at 16:22):

I should mention that I appreciate all the work that you've put into ELPI, it really is a great system

view this post on Zulip Enrico Tassi (Dec 13 2022 at 16:54):

That implicit is not seen by Elpi, only the ones you write before the :.
In Coq you can write implicit directives everywhere (sometimes they are ignored), in Elpi I had to make a choice so to keep terms simple, and I compromise for: only "parameters" have them.

view this post on Zulip Enrico Tassi (Dec 13 2022 at 16:54):

Thanks, much appreciated.

view this post on Zulip Enrico Tassi (Dec 13 2022 at 16:57):

Definition foo {a : ...} ... := ... should work

view this post on Zulip Gregory Malecha (Dec 13 2022 at 17:03):

yeah, that required me to do @X a. It isn't too bad to work around, its just a bit jarring because I expected something else.

view this post on Zulip Gregory Malecha (Dec 13 2022 at 17:29):

I have very little understanding of the vernac stuff. Is there any interest in the attribute "model" that I mentioned above? I assume it is over-simplified in many ways.

view this post on Zulip Enrico Tassi (Dec 13 2022 at 20:43):

I think I want something like that. But I don't havy many use cases other than derive. Maybe collecting more of these is a good start.

view this post on Zulip Gregory Malecha (Dec 13 2022 at 20:53):

I think most instances look like derive. We have lots of different things that we derive at many different levels, but i would say that most of them are essentially a variant of derive

view this post on Zulip Gregory Malecha (Dec 13 2022 at 20:54):

if you think of "generate a definition after another definition" as "derive" then that's mostly what the pattern proposed above supports.


Last updated: Mar 28 2024 at 20:01 UTC