feat(dashboard): redesign graph tab as tactic proof tree#5
Merged
Conversation
Replace the mixed ProofNode/Branch/Goal graph with a proper tactic proof tree rooted at the top-level goal. Goals are nodes, tactics are edges, and attribution shows whether goals were closed by agents or BFS. Protocol: - Add `solved_by` field to ProofGoal for agent attribution (None = BFS) Search engine: - Add `on_goal_update` callback to both search functions that emits ProofGoal updates as the search progresses (root, children, solved) - Extract LSP search into lsp_search.rs to keep search.rs under 500 lines - Add openproof-protocol dependency to openproof-search Event wiring: - autonomous.rs passes callback that sends ProofGoalUpdated events - apply.rs marks matching proof goals as Closed when BFS solves a sorry Frontend: - Rewrite graph.js as goal-centric tactic tree with tree layout algorithm - Clickable nodes expand to show full goal text and failed tactics - Attribution badges: "bfs", "agent:prover", "agent:repairer", etc. - Frontier nodes (open leaves) pulse with amber glow - In-progress nodes pulse with blue glow - Stats bar shows total/closed/open/failed/frontier counts
markm39
force-pushed
the
feat/proof-tree-graph
branch
from
c1cedcd to
fce2cba
Compare
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
1 participant
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.
Summary
solved_byattribution field toProofGoal(agent role or None for BFS)ProofGoalUpdatedevents via callbackChanges across crates
solved_by: Option<String>toProofGoalon_goal_updatecallback to both search functions; extract LSP search tolsp_search.rsautonomous.rsto sendProofGoalUpdatedeventsClosedwhen BFS solves inapply.rsgraph.jsas goal-centric treeTest plan
cargo test --workspacepassescargo clippy --workspace -- -D warningsclean