Stream: Coq devs & plugin devs

Topic: Question on VERNAC EXTEND API & parsing/exec separation


view this post on Zulip Maxime Dénès (Aug 22 2023 at 19:18):

While investigating the following bug: https://github.com/coq-community/vscoq/issues/581, I realized that equations was using VERNAC EXTEND macros with partially applied functions in the actions. Something like derive (f c) of type pm:Declare.OblState.t -> Declare.OblState.t. This idiom has the consequence that f c is evaluated at parsing time (when calling type_vernac), instead of the expected execution phase. Question: is the plugin developer expected to write fun ~pm -> derive (f c) pm in the action (many plugins do that, in which case everything works fine), or should we revise the coqpp generation to eta-expand?

Cc @Pierre-Marie Pédrot

view this post on Zulip Pierre-Marie Pédrot (Aug 23 2023 at 10:40):

Automatically eta-expanding is a simple and efficient technique if we're 100% certain we never want side-effects in there

view this post on Zulip Enrico Tassi (Aug 23 2023 at 11:41):

Since coqpp lets you embed toplevel code { here } I think it is better to make grammar actions pure (at parse time), and force users to put side effects toplevel (if only for readability reasons)

view this post on Zulip Maxime Dénès (Aug 23 2023 at 12:32):

@Enrico Tassi Just to make sure I understand properly: which solution do you suggest?

view this post on Zulip Enrico Tassi (Aug 23 2023 at 12:43):

To always eta expand in coqpp.
If the user really wants some side effect he should put it into a toplevel code block.

view this post on Zulip Maxime Dénès (Aug 23 2023 at 12:54):

Unfortunately, I won't have time to do it myself. Should I open a coqpp issue?

view this post on Zulip Maxime Dénès (Aug 23 2023 at 12:55):

I'm also not sure technically how the eta expansion should really look like. I.e. if it depends on the classification of the action.

view this post on Zulip Maxime Dénès (Aug 23 2023 at 12:56):

(note that this change is not directly related to parsing/exec separation, it is just made more obvious by it)

view this post on Zulip Pierre-Marie Pédrot (Aug 23 2023 at 12:57):

I'm reading the coqpp code and it seems we're already eta-expanding some pieces of code, but not all

view this post on Zulip Maxime Dénès (Aug 23 2023 at 12:59):

Yes, honestly this issue rang a bell. I thought we had fixed some similar issues in the past (but not 100% sure).

view this post on Zulip Pierre-Marie Pédrot (Aug 23 2023 at 12:59):

I think that the idea of taking a ~pm argument directly in the body of the clause is a terrible design choice

view this post on Zulip Pierre-Marie Pédrot (Aug 23 2023 at 12:59):

we should not return functions precisely because they can be eta-expanded, or not

view this post on Zulip Pierre-Marie Pédrot (Aug 23 2023 at 13:00):

the return type should be abstract

view this post on Zulip Maxime Dénès (Aug 23 2023 at 13:00):

What change introduced this btw? I thought it was the vernac extend fine-grained classification PR, but not so obvious. So it may predate it.

view this post on Zulip Pierre-Marie Pédrot (Aug 23 2023 at 13:02):

I think it's 54788df72ce79998ee27db362401a56bda4daceb

view this post on Zulip Pierre-Marie Pédrot (Aug 23 2023 at 13:03):

aka https://github.com/coq/coq/pull/11836

view this post on Zulip Pierre-Marie Pédrot (Aug 23 2023 at 13:07):

I think that a backwards compatible fix for 8.18 is to force coqpp to eta-expand, but ideally for 8.19 the ~pm argument should always be passed implicitly or something, like the ist one in other extensions

view this post on Zulip Pierre-Marie Pédrot (Aug 23 2023 at 13:09):

or we force users to wrap their functions into the typed_vernac type themselves, but this is not very backwards compatible

view this post on Zulip Pierre-Marie Pédrot (Aug 23 2023 at 13:11):

there is already infrastructure to wrap the body in a unit -> 'a thunk, we could just enforce the API to always thunk it for us also

view this post on Zulip Maxime Dénès (Aug 23 2023 at 13:13):

I can help review a patch, but I won't have time to write it, I'm afraid. I still have to migrate the Coq website, the Coq CI and help with the VsCoq 2 & Coq 8.18 releases before next week... :)

view this post on Zulip Pierre-Marie Pédrot (Aug 23 2023 at 13:14):

Erf. I have to finish my share of POPL reviews, which is also a can of worms, but I can try to write a quick fix asap.

view this post on Zulip Pierre-Marie Pédrot (Aug 23 2023 at 13:57):

By the miracle of procrastination, here is the patch: https://github.com/coq/coq/pull/17978. I haven't tested it on the vscoq issue though.

view this post on Zulip Maxime Dénès (Aug 23 2023 at 13:58):

Thanks a lot! I can take care of testing.


Last updated: May 19 2024 at 16:02 UTC