Add information about clauses to implication cards

[VojtechStep]

It's useful to see in the stacktrace what rules were added to the context. It could probably be done with better UI, but this is the least invasive version.

Example stack trace

[gares]

Nice!

Two comments:

• I don't get why we get "implication" printed twice (but I don't recall much of the trace elaborator)
• Maybe you should print the extra info inside add_clauses, since the rule you add may be compiled into multiple rules, eg (p, q) => r should give two entries, p and q and not one entry (p,q) IMO.

[VojtechStep]

By implication being printed twice you mean in the stack trace in VSCode? That's because I manually expanded the implication steps in the UI.

I'll mark this as draft and cook a bit more

[VojtechStep]

I added support for pushing multiple stack frames per step, updated the tests, and added new ones.

This is what the stack look like for the test

and here it is with the implication steps expanded

It'd be better if the "Logic - implication" wasn't there, or ideally if there was a separate window for local assumptions (and, tangentially, maybe another one for showing assigned unification variables), but I think this is as far as I can go without touching the extension code.

[VojtechStep]

The last push should fix the 4.14 errors (how is List.is_empty that recent?!), but I don't think I can do anything about the Windows situation (though I see that it also fails on master)

[gares]

With the commit I pushed and this LPCIC/elpi-lang#35 I get

when there are longer rules, they are elided as usual

[gares]

oops I forgot to promote and I have to go now. Please give it a try and if it works for you I'll merge

[VojtechStep]

Funny that you removed Shiki from the extension, I just fixed the integration this morning, and I've been looking into fixing the terrible performance (which I believe is fixable).

I think the better approach to backwards compatibility would be to have a meta packet as the first object of the trace, which specifies the data version (and if it's missing treat it as v1).

I can try implementing that if you'd like.

[gares]

About versioning the trace format, yes, that would be a more principled approach, but one would still need to pass the version around to print things differently, or version&copy the code.

I thought about that and decided it was not worth it for this little change. But if you have many changes planned, it may make perfect sense