Render why/2 proof terms as an audit tree instead of a flattened term - #5
Merged
Merged
Conversation
Manifold.Prolog.AuditTree recognizes the shape a why/2-style proof comes back as (fact/1, rule/2, either/2, builtin/1, or a flat list of them for a conjunction's body) and draws it as a tree instead of leaving it to flatten into one opaque Prolog term like every other query answer. Manifold.Turn catches this for both routes a goal can reach a query result from: question mode's own `?- why(...)` and a goal the model generated itself. Neither path knows or cares which produced the proof; both now log it as an audit tree via the same helper. Pure unit coverage in test/manifold/prolog/audit_tree_test.exs (no swipl needed). test/integration/why_audit_test.exs exercises the question-mode path end to end against the shipped prelude.
Kernel.node/1 (the BIF reporting the local Erlang node) is auto-imported
into every module, so the private node/1 building a proof's
{label, tag, children} tuple failed to compile: 'imported Kernel.node/1
conflicts with local function'. Renamed to proof_node/1.
The integration test asserted on captured Logger.info output, but config/test.exs deliberately sets `level: :warning` to keep the suite quiet — so the audit tree was computed and immediately discarded by the logger, and the test saw an empty log. Rather than fight that (documented, deliberate) policy, attach the audit tree to the `query` message itself as an additive `:audit` field — visible to any consumer (UI, log, test), not just a log line, and absent whenever a query's answer isn't why/2-shaped. Documented in docs/PROTOCOL.md alongside the existing `answer` field. test/integration/why_audit_test.exs now asserts on the emitted message's payload instead of captured logs.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Manifold.Prolog.AuditTree recognizes the shape a why/2-style proof comes
back as (fact/1, rule/2, either/2, builtin/1, or a flat list of them for
a conjunction's body) and draws it as a tree instead of leaving it to
flatten into one opaque Prolog term like every other query answer.
Manifold.Turn catches this for both routes a goal can reach a query
result from: question mode's own
?- why(...)and a goal the modelgenerated itself. Neither path knows or cares which produced the
proof; both now log it as an audit tree via the same helper.
Pure unit coverage in test/manifold/prolog/audit_tree_test.exs (no
swipl needed). test/integration/why_audit_test.exs exercises the
question-mode path end to end against the shipped prelude.