Stream: Elpi users & devs

Topic: ease of debugging

Enzo Crance (Jun 03 2021 at 14:45):

Hello. Is there another way to find where and why a predicate failed than

• enabling trace and getting lost in several hundreds of lines of trace
• using good old coq.say debug which is not very pleasant either ?
  I'm spending a lot of time on debugging and the prolog-like semantics are what makes these debugging sessions feel eternal. I must be doing it wrong

Cyril Cohen (Jun 03 2021 at 15:00):

You can use std.spy and/or std.spy-do!

Cyril Cohen (Jun 03 2021 at 15:01):

(it will log the input and output of a clause)

Enrico Tassi (Jun 03 2021 at 16:35):

A trace browser is planned, and engineering manpower allocated... then there was the pandemic and it stalled.

The best you can get is by Elpi Trace "predicate" so that only goals about "predicate" are displayed. It's actually a regex following OCaml's conventions.

Enrico Tassi (Jun 03 2021 at 16:38):

If you have ideas on what exactly a trace browser should let you do/filter/jump-to, I'm all ears. I've some ideas, but my POV is probably biased.

Last updated: Oct 13 2024 at 01:02 UTC