Mismatching fields in generated trace in case of CHR

[jwintz]

Hi,

This issue concerns the trace-browser branch, the elaborator specifically.

elpi/tests/sources/trace_chr.elab.json

Line 170 in 96c4d07

"suspend_sibling": { "goal_text": "even X0", "goal_id": 10 },

I see a mismatch here, between the sibling goal_id and the goal_text fields.

It might very well be a misunderstanding of mine, but aren't they supposed to match the definition of the following step:

elpi/tests/sources/trace_chr.elab.json

Line 422 in 96c4d07

"step": [

?

[gares]

Goal 10 is resumed because the variable it contains was assigned to s X.... If I understand the question, it is normal that the goal text is not exactly the same, the purpose is indeed to see the updated goal.

[jwintz]

Fine by me ! It was more a matter of understanding ... I just find it strange to click on such a text to end up on a step which is not named the same in the context of the browser (the display ). In the screenshot below, the sibling links to goal id 10, which actually is the one display in the second screenshot.

If only ergonomic questions remain, this issue can very well be closed for me.

Thanks.

[gares]

I don't know what is best to display, but I think the trace is correct: 7 (0|5) should have as event the resumption of goal 10, since it sets X0 to (s X1).

This phenomena is true in general, a new goal (p X) may become p (f Y) before it gets the chance to be handled. Maybe one could do a wdiff and color differently f Y, signaling that the goal at creation time was less instantiated. In a few cases it would help I guess. In general, I'm not so sure, since it is very frequent. It probably depends on the display of the differences. If it was "optional/no demand" then I think it would be good.