Process attributes after Qed/Defined#22118
Conversation
coqbot-app
Bot
added
the
needs: full CI
|
@SkySkimmer What should the next steps here be?
I'm happy to put more cycles into the development. |
That seems fine, there doesn't seem to be a way to get the error earlier anyway.
I don't see the point of having it be a plugin, it seems like it should be in the statically linked part. But do it as a separate PR since it has much more bikeshed potential. |
gmalecha-at-skylabs
force-pushed
the
gmalecha/attributes-on-hooks
branch
from
110bc01 to
3034b35
Compare
|
I have removed the plugin code from the PR. |
|
@coqbot run full ci |
coqbot-app
Bot
removed
the
needs: full CI
|
|
||
| (* Programmable-attribute hooks must also fire when a Lemma/Theorem is | ||
| completed (at Qed/Defined), not only for Definition. *) | ||
| #[print] |
There was a problem hiding this comment.
I feel like this doesn't test much since the test script doesn't check the output
There was a problem hiding this comment.
I'm used to dune output/expect tests, but I think those don't work here. I've added the tests though.
| val make_g : (S.t -> 'a -> 'a) -> 'a g | ||
| val make : (S.t -> unit) -> t | ||
| val call : ?hook:t -> S.t -> unit | ||
| val seq : t -> t -> t |
There was a problem hiding this comment.
how about adding a list version and using that in vernacentries?
I believe it would also mean call can be unexported
There was a problem hiding this comment.
I've added seqs, but call was pre-existing (probably unused though).
SkySkimmer
added
kind: enhancement
gmalecha-at-skylabs
force-pushed
the
gmalecha/attributes-on-hooks
branch
from
3034b35 to
154d476
Compare
coqbot-app
Bot
added
the
needs: full CI
gmalecha-at-skylabs
force-pushed
the
gmalecha/attributes-on-hooks
branch
from
154d476 to
40e8800
Compare
2 participants
This PR extends the handling of attributes so that handlers are executed when the term is completed, e.g. at the
QedorDefined.It uses this feature to implement a plugin that provides an attribute
#[hint(db=...,cost=...,visibility=...)]. This should be either incorporated into core Rocq or introduced as a separate plugin.For now, I'm just looking for feedback, the commits should be independently reviewable. The last commit contains the hint attribute implementation and could probably use more testing.