Rodolphe Lepigre (Feb 13 2024 at 23:33): Rodolphe Lepigre (Feb 13 2024 at 23:33):While transitioning to Coq 8.19, we are having issues with our custom extensions of derive, some of which generate modules. There does not seem to be any way to let the driver command know that extra modules need to be declared by its syninterp phase, which I think we need to make things work as they used to. Or am I missing something? If this helps, here is an example of problematic derive extension.
Enrico Tassi (Feb 14 2024 at 09:30):Oh, I see. I should really add your project to my CI (help welcome).
Yes, I confirm the driver does not have a synterp phase. I think it should be possible to add one (matching what the interp phase does).
Enrico Tassi (Feb 14 2024 at 09:32):Please open an issue (or a PR ;-)).
May I ask feedback about the kind of errors you experienced? I tried to make the synterp related error messages clear, but well, it is hard to self evaluate the result...
Rodolphe Lepigre (Feb 14 2024 at 09:33):We basically got this error:
Error:
The command did perform no (more) actions during the parsing phase (aka
synterp), while during the execution phase (aka interp) it tried to perform a
begin-module "feature" action. Interp actions must match synterp actions. For
example if a module was imported during the synterp phase, then it must also
be imported during the interp one.
We'll work on a PR today probably, so any guidance would be appreciated. :smile:
Enrico Tassi (Feb 14 2024 at 09:34):the only real limitation is that the decision of making a module or not cannot depend on coq terms (which are not available during the parsing phase). From what I can see, you are good.
Enrico Tassi (Feb 14 2024 at 09:34):Rodolphe Lepigre said:
We basically got this error:
Error: The command did perform no (more) actions during the parsing phase (aka synterp), while during the execution phase (aka interp) it tried to perform a begin-module "feature" action. Interp actions must match synterp actions. For example if a module was imported during the synterp phase, then it must also be imported during the interp one.
my question is: does this message speak to you?
Rodolphe Lepigre (Feb 14 2024 at 09:34):Do you know what the design should be? A kind of hook for derive extensions synterp phase?
Rodolphe Lepigre (Feb 14 2024 at 09:36):Enrico Tassi said:
my question is: does this message speak to you?
Ah of course, sorry. Yeah, it was pretty obvious to us what the issue was from the message (though I find it hard to parse).
Enrico Tassi (Feb 14 2024 at 09:40):here you accumulate to the derive "interp" code
dep1 "finite_type" "finite". %finite implies eq_dec
derivation
(indt T) Prefix
(derive "finite_type"
(derive.finite_type.main (indt T) Prefix)
(finite-type-done (indt T))
).
I think you should make the derive synterp code honor a similar hook.
So that you can
#[synterp] Elpi Accumulate derive lp:{{
dep1 "finite_type" "finite".
derivation ....
}}
and that code declares the module and the include module type actions you do in your driver.
I guess the main difference is that the derivation hook cannot receive the indt T, since it does not exists, but it can receive the indt-decl ast, out of which you should be able to deduce TypeName, that you use for the module name if I see that right.
Rodolphe Lepigre (Feb 14 2024 at 09:41):OK thanks! That's pretty much what we had in mind I think, we'll have a go at it.
Enrico Tassi (Feb 14 2024 at 09:41):Great!
Janno (Feb 14 2024 at 14:08):Do we get access to the body of already defined inductives in the synterp phase? It seems to me that without this there is no way to implement the synterp phase correctly when the recursive argument is used since we won't know the definitions of the other types involved.
Janno (Feb 14 2024 at 14:08):In fact, right now we don't even seem to have access to the AST of the inductive at hand. All we get is a string that represents its fully quantified name.
Enrico Tassi (Feb 14 2024 at 15:44):Hum, no, the logical environment is not available at parsing time.
I need to look more closely to your code in order to propose something viable then.
Rodolphe Lepigre (Feb 14 2024 at 15:55):Would you be available for a quick call today or tomorrow, for example?
Janno (Feb 14 2024 at 17:35):We did manage to push things pretty far but we are now facing very confusing issues. The current state is in https://github.com/rlepigre/coq-elpi/commits/br/derive-synterp/. Only the last two commits (a0351c0b710c9f2a811759a5bb1770fc1d946d1c, eeaa3a4e0bafd188edea963a5d3163432a7f9d83) are relevant and you should be able to cherry-pick them onto a clean 8.19 branch or possibly even master. The interesting test case is in apps/derive/tests/test_finite_type.v. We are seeing extremely weird behavior: the finite_type derive code triggers two other derive routines (eq_dec and finite) and both of them work just fine and announce no synterp acitons. finite_type itself announces begin-module TyName (and more but that's not relevant yet) and for some reason this has bad effects on the interp stage. In the interp stage, we try to find the result of the eq_dec derivation using coq.locate. This succeeds but returns a path that incorrectly contains the module we announced in the synterp stage.This happens even though we call coq.locate before begin-module. The remaining code fails because the located constant simply doesn't exist at that path.
Janno (Feb 14 2024 at 17:37):We tried various things to locate exactly where the extra module comes from in the located path and it doesn't just seem to be all the announced begin-modules. We tried announcing two and only the first one showed up in the output of coq.locate.
Enrico Tassi (Feb 14 2024 at 17:56):That is surely a bug, I thought I had fixed it but maybe it was for another locate* api...
Enrico Tassi (Feb 14 2024 at 17:57):The point is that there are various locate APIs, and I guess I'm calling the "synterp one" in the interp phase, or something like that. I'll check on that tomorrow.
Rodolphe Lepigre (Feb 15 2024 at 14:13):Seems like @Janno and I did it: https://github.com/LPCIC/coq-elpi/pull/597. :smile:
Janno (Feb 15 2024 at 17:18):A somewhat related question: what is the rationale behind derive Inductive ty := .. creating a module but derive ty not also doing that? We are using the latter pretty much exclusively (mostly because our derive extensions didn't support the other syntax) but if we ever wanted to switch we would have to do quite a bit of work to our module types to reflect the change in module hierarchy.
Enrico Tassi (Feb 15 2024 at 22:06):The only reason was to have the inductive inside the module (a bit like OCaml's Foo.t) and have all derived concepts in there as well. Of course you could always store everything inside module, even if you derive "after the facts".
Said that, I don't think there is anything special to do in order to support the other syntax. What derive does is open a module, declare the inductive, and call the derivation (with a different name prefix, the empty one). I'm not so sure why your derivartions don't support that.
Rodolphe Lepigre (Feb 15 2024 at 22:26):They don't support it (or rather, fail when using it) because of a bug which @Janno and I noticed today, but that's an easy fix (a consequence is that we're not using that syntax at all today).
Rodolphe Lepigre (Feb 15 2024 at 22:26):(A bug in the implementations of our extensions.)
Rodolphe Lepigre (Feb 15 2024 at 22:42):Enrico Tassi said:
The only reason was to have the inductive inside the module (a bit like OCaml's
Foo.t) and have all derived concepts in there as well.
That design choice seems a bit odd to me: it kinds of assume that everything you'd want to define around some type will be derived automatically, but that isn't always the case. Maybe this behaviour should be controllable with an attribute? For example, this could look something like this:
#[only(eqb),wrap(Color)] derive
Inductive color := Red | Green | Blue | Yellow.
And this would produce the same as:
Module Color.
Inductive color := Red | Green | Blue | Yellow.
#[only(eqb)] derive color.
End Color.
However, to my taste, the latter is easier to understand and extend, despite being a bit more verbose.
Janno (Feb 16 2024 at 10:41):@Enrico Tassi The design we came up with in the meeting has an issue we only just noticed: the synterp actions still need to be executed in topological order but for derive extensions without a synterp phase we have no way of knowing they exist at all. We could ask for at least dep1 to be declared in both phases but that's almost as much work as just adding an empty derivation clause in synterp. So it seems to us that all extensions will need at least a trivial synterp phase either way. Do you have a different idea for solving this?
Enrico Tassi (Feb 16 2024 at 10:50):I think you are right. My preference would be to have the dep part be declared in both phases, and have a sort of default empty synterp code if the derivation registered none.
Enrico Tassi (Feb 16 2024 at 10:52):choice seems a bit odd to me: it kinds of assume that everything you'd want to define around some type will be derived
automatically, but that isn't always the case. Maybe this behaviour should be controllable with an attribut
Let's say that it should not be a module, but rather a name space. I did not dare mixing NES and derive, but that would be the ideal thing, IMHO.
Janno (Feb 16 2024 at 10:53):Should we make the module thing an optional behavior driven by an attribute? We also thought the same might make sense for the prefix. (It seems derive t custom_prefix doesn't currently work. At least I couldn't manage to make it work.) That way the prefix could also be customized when derive Inductive := .. is used.
Enrico Tassi (Feb 16 2024 at 10:56):I would agree with these changes... but I don't have the energy myself.
Janno (Feb 16 2024 at 10:57):We are already neck deep in the code. It's possible that we can do some of the work.
Janno (Feb 16 2024 at 11:07):A final thing that we are suffering from and that we don't quite know how to solve idiomatically is that we are often forced to derive on aliases due to coq module type constraints where Inductive t cannot be used to fill a Parameter t : Type. Basically the pattern is Inductive t_ := <..>. Definition t := t_. #[only(..)] derive t.
We currently have a simple adapter clause for derivation that unfolds alias constants given to derive to find the underlying inductive and we remember the original name in the automatically-generated Prefix value. Some of our extensions then do string surgery on Prefix to get back the original constant which we need both for generated names as well as for the types generated typeclass instance (which must be defined on the alias and not on the real type).
Is this something that derive should support on its own? Some kind of derive t using t_? I suspect an attribute wouldn't be the best choice because the name should be a real identifier.
Rodolphe Lepigre (Feb 16 2024 at 12:15):Enrico Tassi said:
I think you are right. My preference would be to have the
deppart be declared in both phases, and have a sort of default empty synterp code if the derivation registered none.
I thought about this plan a bit more, and I don't think that will work without also registering the nodes in the dependency graph.
If we don't do that, a standalone deriver that is not depended on and depends on nothing will never make it in the list of things to sort.
Rodolphe Lepigre (Feb 16 2024 at 12:41):An alternative is to always also register a synterp derivation, even when it does not need to do anything. That sounds a bit annoying, but might be easier.
Rodolphe Lepigre (Feb 16 2024 at 17:41):We did go with registering a synterp derivation all the time, it does not look too bad. We updated the MR with that, and also implemented new module and prefix attributes (see here for details).
Enrico Tassi (Feb 16 2024 at 19:59):Amazing thanks! But I won't be able to give you feedback before Monday, so don't hold your breath. Thanks again!
Last updated: Oct 13 2024 at 01:02 UTC