Janno (Mar 12 2024 at 16:48): Janno (Mar 12 2024 at 16:48):We are running into a problem with named clauses. We don't know if the behavior is intended. Here's a minimal reproducer.
Require Import elpi.elpi.
Elpi Db foo lp:{{/*(*/
/*)*/}}.
Module A.
Elpi Accumulate foo lp:{{/*(*/
pred bla.
:name "bla.fail"
bla :- coq.error "bla".
/*)*/}}.
Elpi Typecheck.
End A.
Module B.
Import A.
Elpi Command bla.
Elpi Accumulate Db foo.
Elpi Accumulate lp:{{/*(*/
main _ :- coq.elpi.accumulate library "foo" (clause _ (before "bla.fail") true).
/*)*/}}.
Elpi Typecheck.
Elpi Export bla.
End B.
Module C.
Import A B.
bla.
End C.
Elpi Typecheck bla.
(* Error: File "(elpi.add_clause)", line 1, column 0, character 0:unable to graft this clause: no clause named bla.fail *)
The example doesn't represent exactly what happens in our code base. We actually have the Elpi Db command and the following Elpi Accumulate in an individual file and the rest happens in other files that import that file. It's not possible to reproduce exactly in a single file because Elpi Db does not work inside modules.
Janno (Mar 12 2024 at 16:53):This is not technically a regression w.r.t. to 8.18 but we stumbled over it because we separated a lot of Elpi Db foo commands into #[phase="both"] Elpi Db foo lp:{{ <common stuff > }}. and then Elpi Accumulate foo lp:{{ <interp stuff> }}. In one particular example the named clause moved into the Elpi Accumulate command and is now no longer available unless the command's module is imported directly (and before any modules that use the command).
Janno (Mar 12 2024 at 16:54):Basically the difference is between Elpi Db which is super global and Elpi Accumulate which is not.
Janno (Mar 12 2024 at 16:54):And it is very surprising that moving code like this will make clients fail in such a weird way, especially since it depends on import order and transitive imports and all that
Enrico Tassi (Mar 12 2024 at 20:38):I think it is expected.I also believe I have an attribute to coq.elpi.accumulate to make the clause "superglobal", if you want. I don't have the equivalent for Elpi Accumulate but that could be added I guess, although not be the default.
Truth is, Coq-Elpi inherits this business from Coq, and in general it is not easy to express what should be exposed to clients and what should be hidden. In HB we have a command HB.reexport that can be used to put all "public" declarations into a module which is supposed to be exported. I'm not so sure I recall the pattern completely, maybe @Cyril Cohen or @Kazuhiko Sakaguchi can help here. Here an instance: https://github.com/math-comp/math-comp/blob/3de709760cb37e79cea851dc2942d11e79f53dd2/mathcomp/ssreflect/order.v#L8284-L8289
Janno (Mar 13 2024 at 11:26):I am not sure I entirely agree with "expected" here. The failure happens in mostly unrelated elpi commands called after the problematic action was executed. In this case the problematic action is not even running bla. It is closing the module afterwards (or importing the module that runs bla in another file). It's a very non-local failure mode and it took us hours to find the actual cause.
Enrico Tassi (Mar 13 2024 at 14:16):Don't get me wrong, I sympathize. But it seems to me that the problem is akin to a TC resolution failure due to the fact one did not import the module containing the missing instance. Or a Hint Resolve..
Sure, you can declare all instances and hints as Global, but that is not really recommended, AFAIK, because then there is no way to take these back.
In a way, I don't see how this is elpi specific, other than you can't write Global Elpi Accumulate. I'm happy to add that so that you can more easily follow your patterns. But it also seems your patterns are not the recommended ones (for TC instances, Hints, .. etc). I don't have a strong opinion on this, but on the contrary if you have, it would be better to tall the Coq devs, especially @Pierre-Marie Pédrot that did much work to let users move toward non-global hints.
Enrico Tassi (Mar 13 2024 at 14:18):I mean, you guys have a large code base, hence experience. If the containers for extra logical stuff Coq provides are not good, we devs better know why. Putting things global is a way to escape these containers, defeating their purpose.
Enrico Tassi (Mar 13 2024 at 14:34):After a live discussion with @Cyril Cohen the thing which is annoying (in his experience) is that is the author of a .v file that has to make his file "easy to import" by exporting all its dependencies. Otherwise one has not only to import that files, but also its dependencies, and there is not way to know that some imports are missing (eg no warning for example).
In MC we make some stuff like all_ssreflect easy to import "by hand".
(I'm typing because I do happen to have a keyboard)
Janno (Mar 13 2024 at 16:04):Hm, I don't think I am managing to communicate what irks me about this. I don't mind TC search failing due to a non-Global instance missing. But I do mind typeclass search in Y.v failing with an anomaly because I called typeclass search with a local instance in scope in file X.v and Y.v imports X.v.
Gaëtan Gilbert (Mar 13 2024 at 16:12):Putting things global is a way to escape these containers, defeating their purpose.
Isn't the problem that it does escape even though it's not global? IIUC the command fails due to the presence of some modules which are not imported.
Janno (Mar 13 2024 at 16:16):My understanding is that the command fails because it tries to replay a libobject entry which relies on another module being in imported.
Enrico Tassi (Mar 13 2024 at 18:48):Well, yes, but the libobject in question needs the other liboject to be executed, since it wants to graft a rule A before another rule B (that does not exist if you don't Import the module containing the libobject for rule B).
I'm not so sure what else could I do, other than giving an error. Then I can for sure improve the message, it comes from elpi itself, I could put some "coq context" to it, like "did you Import the module containing rule ...?".
I could also add the rule at the end, but I'm not so sure it makes things easier to debug, since the rule might end up terribly misplaced and make your program fail or loop...
I'm really open to suggestions.
Last updated: Oct 13 2024 at 01:02 UTC