Maxime Dénès (Aug 22 2023 at 19:18): 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
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
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)
Maxime Dénès (Aug 23 2023 at 12:32):@Enrico Tassi Just to make sure I understand properly: which solution do you suggest?
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.
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?
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.
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)
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
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).
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
Pierre-Marie Pédrot (Aug 23 2023 at 12:59):we should not return functions precisely because they can be eta-expanded, or not
Pierre-Marie Pédrot (Aug 23 2023 at 13:00):the return type should be abstract
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.
Pierre-Marie Pédrot (Aug 23 2023 at 13:02):I think it's 54788df72ce79998ee27db362401a56bda4daceb
Pierre-Marie Pédrot (Aug 23 2023 at 13:03):aka https://github.com/coq/coq/pull/11836
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
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
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
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... :)
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.
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.
Maxime Dénès (Aug 23 2023 at 13:58):Thanks a lot! I can take care of testing.
Last updated: Sep 15 2024 at 13:02 UTC