debug modules

[lyhlbyl]

debug logging:

• [ ] a multiple tags based approach to log failures or proof information during evaluation.
• [ ] possible tags
• [ ] structure view of a logging information (have a chat with Andrius for the proof logging sometimes)

tag

• [ ] tactic failures: no binding atomics; failed application
• [ ] goal type failures with deferent levels (e.g. just failures, only active branch, all)
• [ ] partition failures
• [ ] branching failures
• [ ] goal information

eval option:

• [ ] run until (break points)
• [ ] deactive goal node (choose a goal node and not to run it)
• [ ] step over
• [ ] step into

[ggrov]

Ability to log evaluation details, e.g.

• [ ] branching factor for each tactic output
• [ ] branching factor for full proof
• [ ] depth of failed branches
• [ ] success/failure for goals for each goal type / edge
• [ ] produced branches that failed on goaltype
• [ ] link actual edges to the goal they appeared on

Support for

• [ ] writing evaluation strategies (priority list)
• [ ] writing (nested) search strategies
• [ ] parallelism - should be easy to parallelise when no sharing
• [ ] in place change of graph while evaluating - this may cause problems for backtracking! i.e. working on one branch - fix graph - then backtrack to different graph. Should be possible to "map" changes over by having uniform names of vertices/edges over all branches and map any edits across all branches when "active" branch is changed
• [ ] allow to "shift" between last branches (and show how many) -- i.e. one step may give 5 different ways. The user should be able to shift between them to check all. Hierarchy needs to be preserved here.

[plebras]

see #46 and #37