Stream: Elpi users & devs

Topic: First experience report


view this post on Zulip Pierre Roux (Apr 13 2022 at 08:25):

I recently had my first experience with coq-elpi (in the context of https://github.com/math-comp/algebra-tactics/pull/54 ). All in all, this was a very pleasant ride. Thanks a lot for putting so much effort into the tutorials and the doc, they were of great help! Here are the few issues I encountered nonetheless:

pread a <args>.
a <rule>.
a <rule>.
a <rule>.

pread b <args>.
b <rule>.
b <rule>.
b <rule>.

I'd greatly appreciate warnings if I happen to write

pread a <args>.
a <rule>.

pread b <args>.
b <rule>.
b <rule>.
a <rule>.
b <rule>.
b' <rule>.

@Enrico Tassi Do you want me to open issues? (I can't promise PRs)

view this post on Zulip Enrico Tassi (Apr 13 2022 at 08:48):

Thanks for the feedback, please open issues.

The , in pred... I don't thing I can make it optional. I'd need to check the new grammar better, but i and o are not keywords (and l-prolog users are used to use i and o are Church's types for individuals and propositions, I did add prop myself to the language of types to avoid confusion).
If you try with a recent coq-elpi, then the error message should look like this one: https://github.com/LPCIC/elpi/blob/master/src/parser/error_messages.txt#L429 (hope it helps)

I did not try the new menhir parser enough to know if the parentheses thing is better. I think people manage to give good errors about missing parentheses these days, I don't know how. Pointers would be welcome if you know.

About the warnings, I agree with you. Unfortuntely the static checker is a bit of a hack, implemented in elpi itself.. also the compiler loses the order of clauses/type-declarations pretty early. There is still a Loc.t, but that would be harder to use.

About the error messages, I think that can be solved. I did put in coq-elpi the Coq Pp module (with boxes and co) and it worked decently. So maybe I can do the same for OCaml boxes in plan elpi and format error messages decently.

view this post on Zulip Enrico Tassi (Apr 13 2022 at 08:50):

I think I misread one issue, are you saying that {{ coq syntax error }} is unlocalized? That should be fixable indeed.

view this post on Zulip Pierre Roux (Apr 15 2022 at 10:37):

Enrico Tassi said:

About the warnings, I agree with you. Unfortuntely the static checker is a bit of a hack, implemented in elpi itself.. also the compiler loses the order of clauses/type-declarations pretty early. There is still a Loc.t, but that would be harder to use.

Too bad, couldn't we put the warning in the parser then? That'd likely be incomplete in the middle of .v files but would at least work when reading an entire .elpi file.

view this post on Zulip Enrico Tassi (Apr 15 2022 at 17:38):

There is the first compiler step, from ast to structured ast, now that I think about it... there the warning could find its place. https://github.com/LPCIC/elpi/blob/f5186ece691e76653017ead1522f03989a2e319e/src/compiler.ml#L546

pred are already compiled into type+mode, but the order is still there.

I'll look into it after easter, please open an issue.


Last updated: Feb 05 2023 at 14:02 UTC