Stream: Elpi users & devs

Topic: First experience report

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:

• a few unlocalized syntax errors (typically, forgotting a parenthesis in a Coq quotation), maybe this is fixed by getting rid of camlp5, haven't tried on master
• I keep forgetting the commas in predicate declarations, I wonder whether they could be made optional since the i: or o: should be enough to separate the arguments
• I often move rules from one predicate to another and forget to rename them (or do a typo), since most of the code seems to be of the form

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>.

• some error messages are painful to read because they are on very long uncut lines (that's admittedly a cosmetic detail)

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

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.

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.

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.

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: Oct 13 2024 at 01:02 UTC