Stream: Coq devs & plugin devs

Topic: Help with module code refactoring


view this post on Zulip Maxime Dénès (Mar 11 2022 at 12:17):

Hi! I would welcome some help to refactor the following hack: https://github.com/coq/coq/blob/master/vernac/declaremods.ml#L970

view this post on Zulip Maxime Dénès (Mar 11 2022 at 12:18):

For a clean parsing/execution separation, I need module declaration primitives to return data (not just unit). Having these different codepaths makes it inconvenient.

view this post on Zulip Enrico Tassi (Mar 11 2022 at 13:29):

Not so sure this spec is sufficient to give you a hand. It would be better if you wrote the signatures and let others fill in, no?

view this post on Zulip Maxime Dénès (Mar 11 2022 at 13:39):

Well, I guess that's more or less doing the work :)

view this post on Zulip Maxime Dénès (Mar 11 2022 at 13:40):

Help was on removing this hack and code duplication, not on the parsing separation.

view this post on Zulip Maxime Dénès (Mar 11 2022 at 13:42):

It seems pretty clear there's an impedance mismatch somewhere with these list to options conversion, and calling different functions when the list contains several elements, doesn't it?

view this post on Zulip Maxime Dénès (Mar 11 2022 at 13:44):

There's nothing I'm really missing to return the values I need, it is just that this hack makes the code even worse than it is already.

view this post on Zulip Maxime Dénès (Mar 11 2022 at 13:46):

The spec of the refactoring is: make the special case for empty list and single element list disappear :)

view this post on Zulip Gaëtan Gilbert (Mar 11 2022 at 14:16):

the empty list case is VernacDeclareModule ie https://coq.github.io/doc/master/refman/language/core/modules.html#coq:cmd.Declare-Module
one element is VernacDefineModule with a 1 element list as the last argument, ie https://coq.github.io/doc/master/refman/language/core/modules.html#coq:cmd.Module used as Module M (? args) := stuff.
multiple element is also VernacDefineModule as Module M (?args) := stuff <+ otherstuff <+ etc., it seems to be interpreted as Module M (?args). Include stuff. Include otherstuff. Include etc. End M.
(VernacDefineModule just does Declaremods.start_module)

view this post on Zulip Maxime Dénès (Mar 11 2022 at 14:16):

Yes, exactly.

view this post on Zulip Maxime Dénès (Mar 11 2022 at 14:17):

So, very suspicious to dispatch on different code paths.

view this post on Zulip Maxime Dénès (Mar 11 2022 at 14:19):

I guess the cleanest would probably to have the module definition code handle multiple bodies, rather than elaborating to an interactive session. Or the other way, always do the elaboration.

view this post on Zulip Maxime Dénès (Mar 11 2022 at 14:19):

But of course, I wouldn't be surprised if they do subtly different things...

view this post on Zulip Hugo Herbelin (Mar 11 2022 at 18:51):

It is not independent on the following question: do we want to avoid rechecking the contents of a module when computing the result of Include M <+ N? Currently, we trust the kernel that each declaration of an included module (or of an included "functor applied to self" in the case of <+) are already correct. Afaicj, If we want to avoid the start_module/end_module for M1 <+ ... <+ Mn while still avoiding to retype-check the whole included content, we would have to move the operation M1 <+ ... <+ Mn in the kernel, that is, moving Declareops.declare_one_include to the kernel, and trusting it.

view this post on Zulip Hugo Herbelin (Mar 11 2022 at 18:52):

An orthogonal but side question is: do we want to have Include and <+ nodes directly in the kernel, that is in structure_field_body? The pros are to have more sharing and thus suspectingly more efficient modules (??). The cons are that this increases a bit the TCB.

view this post on Zulip Hugo Herbelin (Mar 11 2022 at 18:52):

Slightly related is also https://github.com/coq/coq/pull/11897.

view this post on Zulip Hugo Herbelin (Mar 11 2022 at 18:53):

Related is also the (not so easy) question of functionalizing further declaremods.ml so that, typically, the side effects on the global state are only in vernacentries.ml.


Last updated: Mar 28 2024 at 23:01 UTC