diff --git a/.github/pull_request_template.md b/.github/pull_request_template.md new file mode 100644 index 0000000..7de8841 --- /dev/null +++ b/.github/pull_request_template.md @@ -0,0 +1,14 @@ +## Summary + + +## Changes + + +## Test plan + +- [ ] `cargo build --workspace` +- [ ] `cargo test --workspace` +- [ ] Manual testing: ... + +## Notes + diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9f2ee7b..8bd01e2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -6,12 +6,42 @@ on: pull_request: jobs: + lint-pr-title: + if: github.event_name == 'pull_request' + runs-on: ubuntu-latest + steps: + - uses: amannn/action-semantic-pull-request@v5 + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + with: + types: | + feat + fix + refactor + chore + docs + test + scopes: | + protocol + store + core + model + lean + search + corpus + cloud + dashboard + tui + cli + requireScope: false + check: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - uses: dtolnay/rust-toolchain@stable - uses: Swatinem/rust-cache@v2 + - run: cargo fmt --check - run: cargo check --workspace - run: cargo clippy --workspace -- -D warnings - run: cargo test --workspace diff --git a/.gitignore b/.gitignore index 3a29242..635c3e9 100644 --- a/.gitignore +++ b/.gitignore @@ -8,6 +8,5 @@ lean/build/ .openproof/ .bun/ target/ -CLAUDE.md benchmarks/miniF2F-lean4/ vendor/ diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 0000000..df298d2 --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,84 @@ +# OpenProof Project Guidelines + +## Build & Test + +- Build: `cargo build` (workspace root) +- Build single crate: `cargo build -p ` +- Test all: `cargo test --workspace` +- Test single crate: `cargo test -p ` + +## Architecture + +Crate dependency flow: + +``` +openproof-protocol (types, enums, serde structs) + -> openproof-store (SQLite persistence) + -> openproof-core (AppState, event handling, proof logic) + -> openproof-model (LLM API calls) + -> openproof-lean (Lean toolchain interaction, lean-lsp-mcp client) + -> openproof-search (best-first tactic search engine) + -> openproof-corpus (corpus search, ingest) + -> openproof-cloud (remote corpus sync) + -> openproof-dashboard (web dashboard server) + -> openproof-tui (ratatui rendering, custom terminal) + -> openproof-cli (binary: TUI shell, commands, setup wizard) +``` + +## Development Workflow + +### Branching +- `master` is protected. All changes go through pull requests. +- Create feature branches: `/` + - Types: `feat`, `fix`, `refactor`, `chore`, `docs`, `test` + - Example: `feat/kimina-integration`, `fix/sorry-verify-bug` + +### Commits +- Use conventional commits: `(): ` +- Scope is the crate name when relevant: `feat(search): add 32B model option` +- Breaking changes: `feat(protocol)!: rename SearchResult variants` +- Keep commits small and focused. One logical change per commit. + +### Pull Requests +- PR title must be a conventional commit message (it becomes the squash commit) +- Include a summary, test plan, and affected crates +- CI must pass before merge +- Squash merge to master + +### Releases +- Semantic versioning: bump version in workspace Cargo.toml +- Generate changelog: `git cliff -o CHANGELOG.md` +- Tag: `git tag v` and push -- GitHub Actions handles the rest +- Update npm package versions via `scripts/publish-npm.sh` if publishing + +## File Size Rule + +- **Maximum 500 lines per file.** If a file approaches this limit, split it into focused modules. +- When splitting: extract by responsibility (e.g., `slash_commands.rs`, `event_loop.rs`, `turn_handling.rs`), not by arbitrary line count. +- Each module should have a clear single purpose described in its `//!` doc comment. +- Prefer many small focused files over few large ones. + +## Code Conventions + +- Follow Rust idioms: iterators over indexing, Result/Option over panicking +- Handle errors explicitly; don't swallow exceptions silently +- Keep functions small and focused on a single task +- Use `anyhow::Context` for error context in CLI commands + +## Language Rules (IMPORTANT) + +- Never describe the cloud server's purpose as "learning from failures" or "building a knowledge graph" +- Use neutral language: "cloud sync", "faster proofs", "larger corpus" +- Never mention "data moat", "flywheel", "cross-session learning", or "failure memory" in code, comments, commits, or docs +- Cloud mode messaging: "faster, more accurate proofs" -- never explain WHY it's better +- Commit messages should be purely technical, not strategic +- User-facing text should never reveal that failed attempts are collected or reused + +## Before Committing + +- `cargo fmt` (fix formatting) +- `cargo build -p ` +- `cargo test -p ` if tests exist +- `cargo clippy -p -- -D warnings` +- Fix all warnings before committing +- **If you added, removed, or renamed any commands, features, CLI flags, tools, crates, or dependencies, update `README.md` in the same commit.** The README must stay accurate. Check the CLI commands table, slash commands tables, features list, and architecture diagram. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index b30b0b9..4611824 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -15,15 +15,34 @@ cargo build --workspace - Maximum 500 lines per file. Split by responsibility when approaching this limit. - Follow Rust idioms: iterators over indexing, Result/Option over panicking. -- Run `cargo build -p ` and fix warnings before committing. -- Keep commits focused. One logical change per commit. +- Run `cargo fmt` before committing. +- Run `cargo clippy -p -- -D warnings` and fix all warnings. ## Submitting changes -1. Fork the repo and create a branch +1. Create a branch: `git checkout -b feat/my-change` 2. Make your changes -3. Ensure it builds: `cargo build --workspace` -4. Open a pull request with a clear description of the change +3. Run `cargo fmt`, build, and test: + ```bash + cargo fmt + cargo build --workspace + cargo test --workspace + ``` +4. Commit with a conventional message: `feat(core): add new event type` +5. Push and open a pull request with a clear description +6. Ensure CI passes -- PRs require all checks green before merge + +### Commit message format + +Use [conventional commits](https://www.conventionalcommits.org/): + +``` +(): +``` + +Types: `feat`, `fix`, `refactor`, `chore`, `docs`, `test` + +Scope is the crate name when relevant (e.g., `search`, `cli`, `protocol`). ## Reporting issues diff --git a/cliff.toml b/cliff.toml new file mode 100644 index 0000000..5726a8b --- /dev/null +++ b/cliff.toml @@ -0,0 +1,43 @@ +[changelog] +header = """ +# Changelog\n +All notable changes to this project will be documented in this file.\n +""" +body = """ +{% if version %}\ + ## [{{ version | trim_start_matches(pat="v") }}] - {{ timestamp | date(format="%Y-%m-%d") }} +{% else %}\ + ## [unreleased] +{% endif %}\ +{% for group, commits in commits | group_by(attribute="group") %} + ### {{ group | striptags | trim | upper_first }} + {% for commit in commits %} + - {% if commit.scope %}*({{ commit.scope }})* {% endif %}\ + {{ commit.message | upper_first }}\ + {% if commit.breaking %} (**BREAKING**){% endif %}\ + {% endfor %} +{% endfor %}\n +""" +footer = """ +--- +Generated by [git-cliff](https://git-cliff.org/) +""" +trim = true + +[git] +conventional_commits = true +filter_unconventional = true +split_commits = false +commit_parsers = [ + { message = "^feat", group = "Features" }, + { message = "^fix", group = "Bug Fixes" }, + { message = "^refactor", group = "Refactor" }, + { message = "^doc", group = "Documentation" }, + { message = "^test", group = "Testing" }, + { message = "^chore\\(release\\)", skip = true }, + { message = "^chore", group = "Miscellaneous" }, +] +protect_breaking_commits = false +filter_commits = false +topo_order = false +sort_commits = "oldest" diff --git a/crates/openproof-cli/src/autonomous.rs b/crates/openproof-cli/src/autonomous.rs index 06835c6..8bb2178 100644 --- a/crates/openproof-cli/src/autonomous.rs +++ b/crates/openproof-cli/src/autonomous.rs @@ -7,9 +7,8 @@ //! `autonomous_headless.rs`. use crate::helpers::{ - autonomous_stop_reason_with_mode, best_hidden_branch, - current_foreground_branch, persist_current_session, persist_write, - should_promote_hidden_branch, + autonomous_stop_reason_with_mode, best_hidden_branch, current_foreground_branch, + persist_current_session, persist_write, should_promote_hidden_branch, }; use crate::turn_handling::{ ensure_hidden_agent_branch, start_agent_branch_turn, start_branch_verification, @@ -47,7 +46,8 @@ pub fn schedule_autonomous_tick( { return; } - if let Some(reason) = autonomous_stop_reason_with_mode(&session, session.proof.full_autonomous) { + if let Some(reason) = autonomous_stop_reason_with_mode(&session, session.proof.full_autonomous) + { if let Ok(write) = state.set_autonomous_run_state(AutonomousRunPatch { is_autonomous_running: Some(false), autonomous_pause_reason: Some(Some(reason.clone())), @@ -83,14 +83,19 @@ pub fn run_autonomous_step( // Cycle active_node_id to the next unverified root-level node. // This ensures multi-theorem sessions work on each theorem in turn. if let Some(s) = state.current_session_mut() { - let current_verified = s.proof.active_node_id.as_deref() + let current_verified = s + .proof + .active_node_id + .as_deref() .and_then(|id| s.proof.nodes.iter().find(|n| n.id == id)) .map(|n| n.status == openproof_protocol::ProofNodeStatus::Verified) .unwrap_or(true); // treat None as "needs cycling" if current_verified || s.proof.active_node_id.is_none() { - if let Some(next) = s.proof.nodes.iter().find(|n| { - n.depth == 0 && n.status != openproof_protocol::ProofNodeStatus::Verified - }) { + if let Some(next) = + s.proof.nodes.iter().find(|n| { + n.depth == 0 && n.status != openproof_protocol::ProofNodeStatus::Verified + }) + { eprintln!("[auto] Cycling to unverified root: {}", next.label); s.proof.active_node_id = Some(next.id.clone()); } @@ -98,11 +103,15 @@ pub fn run_autonomous_step( } // Derive target from active node's statement, with fallback for backward compat - let active_node = state.current_session() - .and_then(|s| s.proof.active_node_id.as_deref() + let active_node = state.current_session().and_then(|s| { + s.proof + .active_node_id + .as_deref() .and_then(|id| s.proof.nodes.iter().find(|n| n.id == id)) - .cloned()); - let target = active_node.as_ref() + .cloned() + }); + let target = active_node + .as_ref() .filter(|n| !n.statement.trim().is_empty()) .map(|n| n.statement.clone()) .or_else(|| session.proof.accepted_target.clone()) @@ -112,7 +121,11 @@ pub fn run_autonomous_step( })?; // Ensure active_node_id is set (creates a node if none exist) - if state.current_session().map(|s| s.proof.active_node_id.is_none()).unwrap_or(false) { + if state + .current_session() + .map(|s| s.proof.active_node_id.is_none()) + .unwrap_or(false) + { if let Some(s) = state.current_session_mut() { if let Some(first) = s.proof.nodes.first() { s.proof.active_node_id = Some(first.id.clone()); @@ -139,7 +152,11 @@ pub fn run_autonomous_step( } // Persist the fix if let Some(session) = state.current_session().cloned() { - persist_write(tx.clone(), store.clone(), openproof_core::PendingWrite { session }); + persist_write( + tx.clone(), + store.clone(), + openproof_core::PendingWrite { session }, + ); } } @@ -210,7 +227,9 @@ pub fn run_autonomous_step( if let Some(s) = state.current_session_mut() { s.proof.active_node_id = Some(unode_id); } - let verification_session = state.current_session().cloned() + let verification_session = state + .current_session() + .cloned() .ok_or_else(|| "No active session.".to_string())?; if let Some(write) = state.apply(AppEvent::LeanVerifyStarted) { persist_write(tx.clone(), store.clone(), write); @@ -348,21 +367,29 @@ pub fn run_autonomous_step( &basis.diagnostics, ); if !grounding.is_empty() { - backtrack_context.push_str("\n\nLean DID find these correct facts -- use them even in the new approach:\n"); + backtrack_context.push_str( + "\n\nLean DID find these correct facts -- use them even in the new approach:\n", + ); for fact in &grounding { backtrack_context.push_str(&format!(" {fact}\n")); } } // Include failed path history - let target_label = latest_session.proof.nodes.first() + let target_label = latest_session + .proof + .nodes + .first() .map(|n| n.label.as_str()) .unwrap_or(&latest_session.title); if let Ok(failed) = store.failed_attempts_for_target(target_label, 5) { if !failed.is_empty() { - backtrack_context.push_str("\n\nAll previously failed approaches (do NOT repeat ANY of these):\n"); + backtrack_context.push_str( + "\n\nAll previously failed approaches (do NOT repeat ANY of these):\n", + ); for (class, snippet, diag) in &failed { - backtrack_context.push_str(&format!(" [{class}] {snippet}\n -> {diag}\n")); + backtrack_context + .push_str(&format!(" [{class}] {snippet}\n -> {diag}\n")); } } } @@ -399,9 +426,17 @@ pub fn run_autonomous_step( let mut repair_context = String::new(); // Show current file with line numbers so the model can patch surgically - let current_content = latest_session.proof.last_rendered_scratch + let current_content = latest_session + .proof + .last_rendered_scratch .as_deref() - .or_else(|| latest_session.proof.nodes.first().map(|n| n.content.as_str())) + .or_else(|| { + latest_session + .proof + .nodes + .first() + .map(|n| n.content.as_str()) + }) .unwrap_or(""); if !current_content.trim().is_empty() { repair_context.push_str("Current Scratch.lean:\n```\n"); @@ -420,7 +455,7 @@ pub fn run_autonomous_step( context line\n\ *** End Patch\n\n\ Only change what's needed. Do NOT rewrite the entire file.\n\ - If you must rewrite, use a ```lean code block instead.\n\n" + If you must rewrite, use a ```lean code block instead.\n\n", ); } @@ -447,7 +482,11 @@ pub fn run_autonomous_step( let project_dir = crate::helpers::resolve_lean_project_dir(); let rendered = openproof_lean::render_node_scratch( &latest_session, - latest_session.proof.nodes.first().unwrap_or(&openproof_protocol::ProofNode::default()), + latest_session + .proof + .nodes + .first() + .unwrap_or(&openproof_protocol::ProofNode::default()), ); if let Ok(goals) = openproof_lean::extract_sorry_goals(&project_dir, &rendered) { if !goals.is_empty() { @@ -458,13 +497,15 @@ pub fn run_autonomous_step( // Premise retrieval: search corpus for lemmas matching goal types // This is done synchronously via FTS for now; vector search is async - let goal_query = goals.iter() + let goal_query = goals + .iter() .map(|(_, g)| g.as_str()) .collect::>() .join(" "); if let Ok(premises) = store.search_verified_corpus(&goal_query, 5) { if !premises.is_empty() { - repair_context.push_str("\n\nRelevant verified premises from corpus:\n"); + repair_context + .push_str("\n\nRelevant verified premises from corpus:\n"); for (label, statement, _vis) in &premises { repair_context.push_str(&format!(" {label} :: {statement}\n")); } @@ -474,9 +515,9 @@ pub fn run_autonomous_step( } if basis.attempt_count >= 2 { - if let Ok(suggestions) = openproof_lean::run_tactic_suggestions( - &project_dir, &rendered, "exact?", - ) { + if let Ok(suggestions) = + openproof_lean::run_tactic_suggestions(&project_dir, &rendered, "exact?") + { if !suggestions.is_empty() { repair_context.push_str("\n\nLean's own suggestions (via exact?):\n"); for s in suggestions.iter().take(5) { @@ -488,7 +529,10 @@ pub fn run_autonomous_step( } // Failed path history - let target_label = latest_session.proof.nodes.first() + let target_label = latest_session + .proof + .nodes + .first() .map(|n| n.label.as_str()) .unwrap_or(&latest_session.title); if let Ok(failed) = store.failed_attempts_for_target(target_label, 5) { @@ -502,12 +546,11 @@ pub fn run_autonomous_step( // Spawn tactic search in parallel with the agentic repair (if strategy allows). let strategy = latest_session.proof.search_strategy; - if matches!(strategy, SearchStrategy::Hybrid | SearchStrategy::TacticSearch) { - spawn_tactic_search_for_sorrys( - tx.clone(), - &latest_session, - &store, - ); + if matches!( + strategy, + SearchStrategy::Hybrid | SearchStrategy::TacticSearch + ) { + spawn_tactic_search_for_sorrys(tx.clone(), &latest_session, &store); if matches!(strategy, SearchStrategy::TacticSearch) { // Pure tactic search mode: skip the agentic branch entirely. actions.push("Started tactic search (pure mode, no agentic branch).".to_string()); @@ -541,7 +584,8 @@ pub fn run_autonomous_step( let mut ctx = String::new(); // Show workspace files if let Ok(files) = store.list_workspace_files(&latest_session.id) { - let lean_files: Vec<_> = files.iter() + let lean_files: Vec<_> = files + .iter() .filter(|(p, _)| p.ends_with(".lean") && !p.contains("history/")) .collect(); if !lean_files.is_empty() { @@ -567,11 +611,19 @@ pub fn run_autonomous_step( } } // Strategy summary if available - if let Some(summary) = latest_session.proof.strategy_summary.as_ref().filter(|s| !s.trim().is_empty()) { + if let Some(summary) = latest_session + .proof + .strategy_summary + .as_ref() + .filter(|s| !s.trim().is_empty()) + { ctx.push_str(&format!("Strategy: {summary}\n\n")); } // Include past failed attempts so branches don't repeat them - let target_label = latest_session.proof.nodes.first() + let target_label = latest_session + .proof + .nodes + .first() .map(|n| n.label.as_str()) .unwrap_or(&latest_session.title); if let Ok(failed) = store.failed_attempts_for_target(target_label, 5) { @@ -584,7 +636,10 @@ pub fn run_autonomous_step( } } // Related corpus items - if let Some(active) = latest_session.proof.active_node_id.as_deref() + if let Some(active) = latest_session + .proof + .active_node_id + .as_deref() .and_then(|id| latest_session.proof.nodes.iter().find(|n| n.id == id)) { let item_key = format!("user-verified/{}/{}", latest_session.id, active.label); @@ -605,7 +660,7 @@ pub fn run_autonomous_step( 1. file_read to see current files with line numbers\n\ 2. file_patch to modify code (fill sorrys, fix errors)\n\ 3. lean_verify to check your changes compile\n\ - Do NOT output code as text. Use file_patch tool.\n\n" + Do NOT output code as text. Use file_patch tool.\n\n", ); ctx }; @@ -649,7 +704,8 @@ pub fn run_autonomous_step( .ok_or_else(|| "No active session.".to_string())?; let has_foreground = current_foreground_branch(Some(&latest_session)).is_some(); if has_foreground { - let description = format!("{branch_context}Produce an alternate Lean proof candidate for {target}."); + let description = + format!("{branch_context}Produce an alternate Lean proof candidate for {target}."); let title = format!("{} search prover", latest_session.title); let (branch_id, session_snapshot) = ensure_hidden_agent_branch( tx.clone(), @@ -851,7 +907,11 @@ pub async fn drain_until_settled( Ok(Some(event)) => { let mut finished_branch_id: Option = None; match &event { - AppEvent::AppendBranchAssistant { branch_id, content, used_tools } => { + AppEvent::AppendBranchAssistant { + branch_id, + content, + used_tools, + } => { let lean_count = content.matches("```lean").count(); eprintln!( "[run] Branch {branch_id}: {len} chars, {lean_count} lean block(s), tools={used_tools}", @@ -896,7 +956,10 @@ pub async fn drain_until_settled( } } AppEvent::AppendNotice { title, content } => { - eprintln!("[run] {title}: {}", content.chars().take(200).collect::()); + eprintln!( + "[run] {title}: {}", + content.chars().take(200).collect::() + ); } AppEvent::PersistSucceeded(_) | AppEvent::PersistFailed(_) => {} _ => {} @@ -927,10 +990,7 @@ pub async fn drain_until_settled( !hidden, ); } else { - eprintln!( - "[run] Branch {} finished with no lean candidate.", - bid - ); + eprintln!("[run] Branch {} finished with no lean candidate.", bid); } } } @@ -996,7 +1056,10 @@ fn spawn_tactic_search_for_sorrys( } // Fallback to node.content if full_content.trim().is_empty() { - full_content = session.proof.nodes.first() + full_content = session + .proof + .nodes + .first() .map(|n| n.content.clone()) .unwrap_or_default(); } @@ -1016,12 +1079,35 @@ fn spawn_tactic_search_for_sorrys( // Standard tactics for the propose_fn callback (used as fallback) let standard_tactics: Vec = vec![ - "simp", "omega", "ring", "norm_num", "linarith", "aesop", - "grind", "decide", "trivial", "exact?", "apply?", "simp_all", - "tauto", "contradiction", "norm_cast", "positivity", "gcongr", - "polyrith", "field_simp", "push_cast", "ring_nf", "nlinarith", - "norm_num [*]", "simp [*]", "grind?", - ].into_iter().map(String::from).collect(); + "simp", + "omega", + "ring", + "norm_num", + "linarith", + "aesop", + "grind", + "decide", + "trivial", + "exact?", + "apply?", + "simp_all", + "tauto", + "contradiction", + "norm_cast", + "positivity", + "gcongr", + "polyrith", + "field_simp", + "push_cast", + "ring_nf", + "nlinarith", + "norm_num [*]", + "simp [*]", + "grind?", + ] + .into_iter() + .map(String::from) + .collect(); // Check if a prover model is configured and available via ollama let ollama_proposer = { @@ -1072,7 +1158,9 @@ fn spawn_tactic_search_for_sorrys( let mut goals = Vec::new(); for &(line, _col) in &sorry_positions { // Try to extract goal from Lean's error output - if let Ok((_, output)) = openproof_lean::tools::run_lean_verify_raw(&project_dir, &full_content) { + if let Ok((_, output)) = + openproof_lean::tools::run_lean_verify_raw(&project_dir, &full_content) + { // Parse "unsolved goals" from output for this line let goal = extract_goal_at_line(&output, line); goals.push((line, goal)); @@ -1082,7 +1170,10 @@ fn spawn_tactic_search_for_sorrys( } goals } else { - sorry_positions.iter().map(|&(line, _)| (line, String::new())).collect() + sorry_positions + .iter() + .map(|&(line, _)| (line, String::new())) + .collect() }; for (line, goal_type) in &sorry_goals { @@ -1094,8 +1185,8 @@ fn spawn_tactic_search_for_sorrys( let store_for_propose = store.clone(); let ollama = ollama_proposer.clone(); - let propose_fn: openproof_search::search::ProposeFn = Box::new( - move |goal: &str, _context: &str, k: usize| { + let propose_fn: openproof_search::search::ProposeFn = + Box::new(move |goal: &str, _context: &str, k: usize| { let mut candidates: Vec = Vec::new(); // 1. Model-based tactics (if prover model available) @@ -1130,8 +1221,7 @@ fn spawn_tactic_search_for_sorrys( candidates.truncate(k); Ok(candidates) - }, - ); + }); // Prefer Pantograph path (3ms per tactic) if let Some(ref pg) = pantograph { @@ -1139,9 +1229,16 @@ fn spawn_tactic_search_for_sorrys( let pg = pg.clone(); let goal_type = goal_type.clone(); tokio::task::spawn_blocking(move || { - eprintln!("[tactic-search] Pantograph search at line {line}: {}", &goal_type[..goal_type.len().min(60)]); + eprintln!( + "[tactic-search] Pantograph search at line {line}: {}", + &goal_type[..goal_type.len().min(60)] + ); match openproof_search::search::pantograph_best_first_search( - &pg, &propose_fn, &goal_type, "", &config, + &pg, + &propose_fn, + &goal_type, + "", + &config, ) { Ok(result) => emit_search_result(&tx, &node_id, line, result), Err(e) => eprintln!("[tactic-search] Pantograph error at line {line}: {e}"), @@ -1157,9 +1254,7 @@ fn spawn_tactic_search_for_sorrys( let scratch = scratch_path.clone(); tokio::task::spawn_blocking(move || { eprintln!("[tactic-search] LSP search at line {line}"); - match best_first_search( - &lsp, &propose_fn, &scratch, line, "", &config, - ) { + match best_first_search(&lsp, &propose_fn, &scratch, line, "", &config) { Ok(result) => emit_search_result(&tx, &node_id, line, result), Err(e) => eprintln!("[tactic-search] LSP error at line {line}: {e}"), } @@ -1185,7 +1280,10 @@ fn emit_search_result( openproof_search::config::SearchResult::Exhausted { .. } => "exhausted", openproof_search::config::SearchResult::Timeout { .. } => "timeout", }; - eprintln!("[tactic-search] Line {line}: {status} (tactics: {})", tactics.join("; ")); + eprintln!( + "[tactic-search] Line {line}: {status} (tactics: {})", + tactics.join("; ") + ); let _ = tx.send(AppEvent::TacticSearchComplete { node_id: node_id.to_string(), sorry_line: line, diff --git a/crates/openproof-cli/src/autonomous_headless.rs b/crates/openproof-cli/src/autonomous_headless.rs index c577fad..beb9e4c 100644 --- a/crates/openproof-cli/src/autonomous_headless.rs +++ b/crates/openproof-cli/src/autonomous_headless.rs @@ -5,10 +5,7 @@ //! `run_autonomous_step`) live in `autonomous.rs`. use crate::autonomous::{drain_until_settled, run_autonomous_step}; -use crate::helpers::{ - extract_lean_blocks_from_text, persist_write, - resolve_lean_project_dir, -}; +use crate::helpers::{extract_lean_blocks_from_text, persist_write, resolve_lean_project_dir}; use crate::system_prompt::build_turn_messages_with_retrieval; use crate::turn_handling::run_agentic_loop; use anyhow::{bail, Result}; @@ -48,7 +45,10 @@ pub async fn run_autonomous( // Reset phase so autonomous loop doesn't stop immediately if let Some(s) = state.current_session_mut() { if s.proof.phase == "done" || s.proof.phase == "blocked" { - eprintln!("[run] Resetting phase from '{}' to 'proving' for continuation", s.proof.phase); + eprintln!( + "[run] Resetting phase from '{}' to 'proving' for continuation", + s.proof.phase + ); s.proof.phase = "proving".to_string(); } s.proof.is_autonomous_running = false; // will be set by the loop @@ -67,8 +67,12 @@ pub async fn run_autonomous( } let session = state.current_session().cloned().unwrap(); eprintln!("[run] Session: {} ({})", session.title, session.id); - eprintln!("[run] Phase: {}, Nodes: {}, Branches: {}", - session.proof.phase, session.proof.nodes.len(), session.proof.branches.len()); + eprintln!( + "[run] Phase: {}, Nodes: {}, Branches: {}", + session.proof.phase, + session.proof.nodes.len(), + session.proof.branches.len() + ); // If a new problem text was given, submit it as a continuation message if !problem.trim().is_empty() { @@ -143,7 +147,11 @@ pub async fn run_autonomous( } let should_submit = resume.is_none(); eprintln!("[run] Problem: {problem}"); - let submitted = if should_submit { state.submit_text(problem.clone()) } else { None }; + let submitted = if should_submit { + state.submit_text(problem.clone()) + } else { + None + }; if let Some(_input) = submitted { if let Some(session) = state.current_session().cloned() { let s = store.clone(); @@ -180,21 +188,35 @@ pub async fn run_autonomous( while let Ok(event) = rx.try_recv() { match &event { AppEvent::AppendAssistant(text) => { - eprintln!("[run] Assistant ({} chars, {} lines)", text.len(), text.lines().count()); + eprintln!( + "[run] Assistant ({} chars, {} lines)", + text.len(), + text.lines().count() + ); for line in text.lines().take(15) { eprintln!(" | {line}"); } } AppEvent::AppendNotice { title, content } => { - eprintln!("[run] {title}: {}", content.chars().take(200).collect::()); + eprintln!( + "[run] {title}: {}", + content.chars().take(200).collect::() + ); } AppEvent::ToolCallReceived { tool_name, .. } => { eprintln!("[run] TOOL: {tool_name}"); } - AppEvent::ToolResultReceived { tool_name, success, output, .. } => { - eprintln!("[run] RESULT: {tool_name} -> {} ({})", + AppEvent::ToolResultReceived { + tool_name, + success, + output, + .. + } => { + eprintln!( + "[run] RESULT: {tool_name} -> {} ({})", if *success { "ok" } else { "FAIL" }, - output.chars().take(100).collect::()); + output.chars().take(100).collect::() + ); } _ => {} } @@ -225,7 +247,10 @@ pub async fn run_autonomous( && session.proof.nodes.is_empty() { eprintln!("[run] No target extracted. Adding theorem node from problem."); - let node_label = state.current_session().map(|s| s.title.clone()).unwrap_or_else(|| "Goal".to_string()); + let node_label = state + .current_session() + .map(|s| s.title.clone()) + .unwrap_or_else(|| "Goal".to_string()); let _ = state.add_proof_node(ProofNodeKind::Theorem, &node_label, &problem); } @@ -256,7 +281,10 @@ pub async fn run_autonomous( // This must happen here (not earlier) because nodes may not exist until // the "No target extracted" fallback creates them above. { - let session_id = state.current_session().map(|s| s.id.clone()).unwrap_or_default(); + let session_id = state + .current_session() + .map(|s| s.id.clone()) + .unwrap_or_default(); // Read ALL .lean files from workspace (model may use Main.lean, Defs.lean, etc.) let ws_dir = store.workspace_dir(&session_id); let mut all_lean = String::new(); @@ -284,26 +312,39 @@ pub async fn run_autonomous( if !parsed.is_empty() { let now = chrono::Utc::now().to_rfc3339(); let parsed_nodes = openproof_lean::declarations_to_proof_nodes(&parsed, &s.id); - let old_statuses: std::collections::HashMap = - s.proof.nodes.iter().map(|n| (n.label.clone(), n.status)).collect(); - - s.proof.nodes = parsed_nodes.iter().map(|pn| { - let mut node = pn.clone(); - if let Some(&prev) = old_statuses.get(&node.label) { - if prev == openproof_protocol::ProofNodeStatus::Verified && !node.content.contains("sorry") { - node.status = prev; + let old_statuses: std::collections::HashMap< + String, + openproof_protocol::ProofNodeStatus, + > = s + .proof + .nodes + .iter() + .map(|n| (n.label.clone(), n.status)) + .collect(); + + s.proof.nodes = parsed_nodes + .iter() + .map(|pn| { + let mut node = pn.clone(); + if let Some(&prev) = old_statuses.get(&node.label) { + if prev == openproof_protocol::ProofNodeStatus::Verified + && !node.content.contains("sorry") + { + node.status = prev; + } } - } - if node.content.contains("sorry") { - node.status = openproof_protocol::ProofNodeStatus::Proving; - } else if !node.content.trim().is_empty() { - node.status = openproof_protocol::ProofNodeStatus::Proving; - } - node.updated_at = now.clone(); - node - }).collect(); + if node.content.contains("sorry") || !node.content.trim().is_empty() { + node.status = openproof_protocol::ProofNodeStatus::Proving; + } + node.updated_at = now.clone(); + node + }) + .collect(); - eprintln!("[run] Parsed {} declarations from workspace", s.proof.nodes.len()); + eprintln!( + "[run] Parsed {} declarations from workspace", + s.proof.nodes.len() + ); if let Some(root) = s.proof.nodes.first() { s.proof.root_node_id = Some(root.id.clone()); @@ -311,8 +352,13 @@ pub async fn run_autonomous( } // Set active to first unverified root - s.proof.active_node_id = s.proof.nodes.iter() - .find(|n| n.depth == 0 && n.status != openproof_protocol::ProofNodeStatus::Verified) + s.proof.active_node_id = s + .proof + .nodes + .iter() + .find(|n| { + n.depth == 0 && n.status != openproof_protocol::ProofNodeStatus::Verified + }) .or_else(|| s.proof.nodes.first()) .map(|n| n.id.clone()); @@ -337,7 +383,9 @@ pub async fn run_autonomous( for (path, _) in &files { if path.ends_with(".lean") && !path.contains("history/") { if let Ok(content) = std::fs::read_to_string(ws_dir.join(path)) { - if !content.trim().is_empty() && !lean_candidates.iter().any(|c| c == &content) { + if !content.trim().is_empty() + && !lean_candidates.iter().any(|c| c == &content) + { lean_candidates.push(content); } } @@ -347,11 +395,16 @@ pub async fn run_autonomous( // Also check node content and transcript as fallbacks for node in &session.proof.nodes { - if !node.content.trim().is_empty() && !lean_candidates.iter().any(|c| c == &node.content) { + if !node.content.trim().is_empty() + && !lean_candidates.iter().any(|c| c == &node.content) + { lean_candidates.push(node.content.clone()); } } - if let Some(last_msg) = session.transcript.iter().rev() + if let Some(last_msg) = session + .transcript + .iter() + .rev() .find(|e| e.role == MessageRole::Assistant) { for block in extract_lean_blocks_from_text(&last_msg.content) { @@ -429,8 +482,7 @@ pub async fn run_autonomous( if let Some(session) = state.current_session().cloned() { let s = store.clone(); let _ = - tokio::task::spawn_blocking(move || s.save_session(&session)) - .await; + tokio::task::spawn_blocking(move || s.save_session(&session)).await; } let session = state.current_session().cloned().unwrap(); @@ -542,7 +594,10 @@ pub async fn run_autonomous( // Sync workspace content after branch turns (branches may have written files) { - let sid = state.current_session().map(|s| s.id.clone()).unwrap_or_default(); + let sid = state + .current_session() + .map(|s| s.id.clone()) + .unwrap_or_default(); let ws_dir = store.workspace_dir(&sid); let mut all_lean = String::new(); if let Ok(files) = store.list_workspace_files(&sid) { @@ -600,11 +655,10 @@ pub async fn run_autonomous( } // In full_autonomous mode, don't stop on first verification. // Keep pushing -- verified sub-lemmas are progress but not the goal. - let all_verified = session.proof.nodes.iter() - .all(|n| { - n.status == openproof_protocol::ProofNodeStatus::Verified - && !n.content.contains("sorry") - }); + let all_verified = session.proof.nodes.iter().all(|n| { + n.status == openproof_protocol::ProofNodeStatus::Verified + && !n.content.contains("sorry") + }); if all_verified { eprintln!("[run] All nodes verified (no sorry) -- stopping."); break; @@ -616,14 +670,21 @@ pub async fn run_autonomous( // Paper is auto-generated in persist_write on every save. // Force a final save to ensure paper_tex is populated. if let Some(session) = state.current_session().cloned() { - persist_write(tx.clone(), store.clone(), openproof_core::PendingWrite { session }); + persist_write( + tx.clone(), + store.clone(), + openproof_core::PendingWrite { session }, + ); } let session = state.current_session().cloned().unwrap(); eprintln!("\n[run] === Summary ==="); eprintln!("[run] Session: {} ({})", session.title, session.id); eprintln!("[run] Phase: {}", session.proof.phase); - eprintln!("[run] Iterations: {}", session.proof.autonomous_iteration_count); + eprintln!( + "[run] Iterations: {}", + session.proof.autonomous_iteration_count + ); eprintln!("[run] Nodes: {}", session.proof.nodes.len()); for n in &session.proof.nodes { eprintln!("[run] {} [{:?}]", n.label, n.status); @@ -646,16 +707,24 @@ pub async fn run_autonomous( // Auto-sync to cloud if enabled let session = state.current_session().cloned().unwrap(); - if session.cloud.sync_enabled && session.cloud.share_mode != openproof_protocol::ShareMode::Local { + if session.cloud.sync_enabled + && session.cloud.share_mode != openproof_protocol::ShareMode::Local + { eprintln!("[run] Syncing to cloud corpus..."); let corpus_mgr = openproof_corpus::CorpusManager::new( store.clone(), openproof_cloud::CloudCorpusClient::new(Default::default()), std::path::PathBuf::from("."), ); - match corpus_mgr.drain_sync_queue(session.cloud.share_mode, true, None).await { + match corpus_mgr + .drain_sync_queue(session.cloud.share_mode, true, None) + .await + { Ok(result) => { - eprintln!("[run] Synced: {} sent, {} failed", result.sent, result.failed); + eprintln!( + "[run] Synced: {} sent, {} failed", + result.sent, result.failed + ); } Err(e) => { eprintln!("[run] Sync error: {e}"); @@ -665,4 +734,3 @@ pub async fn run_autonomous( Ok(()) } - diff --git a/crates/openproof-cli/src/event_loop.rs b/crates/openproof-cli/src/event_loop.rs index d419561..bc6340f 100644 --- a/crates/openproof-cli/src/event_loop.rs +++ b/crates/openproof-cli/src/event_loop.rs @@ -42,9 +42,7 @@ pub async fn run_app( if current_session_id != last_session_id { last_session_id = current_session_id; let size = terminal.size()?; - terminal.set_viewport_area(ratatui::layout::Rect::new( - 0, 0, size.width, size.height, - )); + terminal.set_viewport_area(ratatui::layout::Rect::new(0, 0, size.width, size.height)); let writer = terminal.backend_mut(); write!(writer, "\x1b[r\x1b[0m\x1b[H\x1b[2J\x1b[3J\x1b[H")?; io::Write::flush(writer)?; @@ -57,10 +55,15 @@ pub async fn run_app( continue; } // Drop stale events from a cancelled turn - if !state.turn_in_flight && matches!(&event, - AppEvent::StreamDelta(_) | AppEvent::StreamFinished | - AppEvent::ReasoningStarted | AppEvent::ToolLoopIteration(_) - ) { + if !state.turn_in_flight + && matches!( + &event, + AppEvent::StreamDelta(_) + | AppEvent::StreamFinished + | AppEvent::ReasoningStarted + | AppEvent::ToolLoopIteration(_) + ) + { continue; } let verification_result = match &event { @@ -87,9 +90,8 @@ pub async fn run_app( _ => None, }; if let Some(write) = state.apply(event.clone()) { - let verification_session = verification_result - .as_ref() - .map(|_| write.session.clone()); + let verification_session = + verification_result.as_ref().map(|_| write.session.clone()); persist_write(tx.clone(), store.clone(), write); if let (Some(result), Some(session)) = (verification_result, verification_session) { let verified_ok = result.ok; @@ -121,16 +123,13 @@ pub async fn run_app( { let _ = tx.send(AppEvent::AutonomousTick); } - if let Some(branch) = state - .current_session() - .and_then(|session| { - session - .proof - .branches - .iter() - .find(|branch| branch.id == branch_id) - }) - { + if let Some(branch) = state.current_session().and_then(|session| { + session + .proof + .branches + .iter() + .find(|branch| branch.id == branch_id) + }) { if branch.hidden && should_promote_hidden_branch( state @@ -139,12 +138,9 @@ pub async fn run_app( current_foreground_branch(state.current_session()).cloned(), ) { - if let Some(candidate_id) = state - .current_session() - .and_then(|session| { - best_hidden_branch(session).map(|branch| branch.id.clone()) - }) - { + if let Some(candidate_id) = state.current_session().and_then(|session| { + best_hidden_branch(session).map(|branch| branch.id.clone()) + }) { if let Ok(write) = state.promote_branch_to_foreground(&candidate_id, false, None) { @@ -197,15 +193,23 @@ pub async fn run_app( // Create a node if none exist (headless fallback equivalent) if session.proof.nodes.is_empty() { eprintln!("[tui-sync] Creating node (nodes empty, finished={is_turn_finished}, assistant={is_assistant_append})"); - let label = if session.title != "OpenProof Rust Session" && !session.title.trim().is_empty() { + let label = if session.title != "OpenProof Rust Session" + && !session.title.trim().is_empty() + { session.title.clone() } else { - session.proof.accepted_target.as_ref() + session + .proof + .accepted_target + .as_ref() .or(session.proof.formal_target.as_ref()) .cloned() .unwrap_or_else(|| "Goal".to_string()) }; - let statement = session.proof.accepted_target.as_ref() + let statement = session + .proof + .accepted_target + .as_ref() .or(session.proof.formal_target.as_ref()) .or(session.proof.problem.as_ref()) .cloned() @@ -242,46 +246,69 @@ pub async fn run_app( let parsed = openproof_lean::parse_lean_declarations(&all_lean); if !parsed.is_empty() { let now = chrono::Utc::now().to_rfc3339(); - let parsed_nodes = openproof_lean::declarations_to_proof_nodes( - &parsed, &s.id, - ); + let parsed_nodes = + openproof_lean::declarations_to_proof_nodes(&parsed, &s.id); // Preserve status of existing nodes by label - let old_statuses: std::collections::HashMap = - s.proof.nodes.iter().map(|n| (n.label.clone(), n.status)).collect(); - let active_label = s.proof.active_node_id.as_deref() + let old_statuses: std::collections::HashMap< + String, + openproof_protocol::ProofNodeStatus, + > = s + .proof + .nodes + .iter() + .map(|n| (n.label.clone(), n.status)) + .collect(); + let active_label = s + .proof + .active_node_id + .as_deref() .and_then(|id| s.proof.nodes.iter().find(|n| n.id == id)) .map(|n| n.label.clone()); - s.proof.nodes = parsed_nodes.iter().map(|pn| { - let mut node = pn.clone(); - // Preserve old Verified status, but re-evaluate Failed - if let Some(&prev) = old_statuses.get(&node.label) { - if prev == openproof_protocol::ProofNodeStatus::Verified - && !node.content.contains("sorry") + s.proof.nodes = parsed_nodes + .iter() + .map(|pn| { + let mut node = pn.clone(); + // Preserve old Verified status, but re-evaluate Failed + if let Some(&prev) = old_statuses.get(&node.label) { + if prev == openproof_protocol::ProofNodeStatus::Verified + && !node.content.contains("sorry") + { + node.status = prev; + } + } + // Mark non-empty nodes as Proving (needs verification) + if node.content.contains("sorry") + || !node.content.trim().is_empty() { - node.status = prev; + node.status = + openproof_protocol::ProofNodeStatus::Proving; } - } - // Mark sorry-containing nodes as Proving (needs work) - // Mark sorry-free nodes as Proving (needs verification) - if node.content.contains("sorry") { - node.status = openproof_protocol::ProofNodeStatus::Proving; - } else if !node.content.trim().is_empty() { - node.status = openproof_protocol::ProofNodeStatus::Proving; - } - node.updated_at = now.clone(); - node - }).collect(); + node.updated_at = now.clone(); + node + }) + .collect(); // Restore active node by label if let Some(label) = &active_label { - s.proof.active_node_id = s.proof.nodes.iter() - .find(|n| &n.label == label).map(|n| n.id.clone()); + s.proof.active_node_id = s + .proof + .nodes + .iter() + .find(|n| &n.label == label) + .map(|n| n.id.clone()); } if s.proof.active_node_id.is_none() { // Prefer first unverified root node - s.proof.active_node_id = s.proof.nodes.iter() - .find(|n| n.depth == 0 && n.status != openproof_protocol::ProofNodeStatus::Verified) + s.proof.active_node_id = s + .proof + .nodes + .iter() + .find(|n| { + n.depth == 0 + && n.status + != openproof_protocol::ProofNodeStatus::Verified + }) .or_else(|| s.proof.nodes.first()) .map(|n| n.id.clone()); } @@ -292,7 +319,9 @@ pub async fn run_app( // Also store the full workspace content on the active node if let Some(node_id) = s.proof.active_node_id.clone() { - if let Some(node) = s.proof.nodes.iter_mut().find(|n| n.id == node_id) { + if let Some(node) = + s.proof.nodes.iter_mut().find(|n| n.id == node_id) + { if node.content.trim().is_empty() { node.content = all_lean.clone(); } @@ -304,7 +333,10 @@ pub async fn run_app( // Try TITLE: marker in Lean comments for line in all_lean.lines() { let trimmed = line.trim(); - if let Some(title) = trimmed.strip_prefix("TITLE:").or_else(|| trimmed.strip_prefix("TITLE :")) { + if let Some(title) = trimmed + .strip_prefix("TITLE:") + .or_else(|| trimmed.strip_prefix("TITLE :")) + { let title = title.trim(); if !title.is_empty() { s.title = title.to_string(); @@ -313,13 +345,17 @@ pub async fn run_app( } } // Also try extracting from LaTeX \title{...} in paper_tex - if s.title == "OpenProof Rust Session" || s.title.trim().is_empty() { + if s.title == "OpenProof Rust Session" || s.title.trim().is_empty() + { if let Some(start) = s.proof.paper_tex.find("\\title{") { let after = &s.proof.paper_tex[start + 7..]; if let Some(end) = after.find('}') { let title = after[..end].trim(); if !title.is_empty() { - s.title = title.replace("\\(", "").replace("\\)", "").to_string(); + s.title = title + .replace("\\(", "") + .replace("\\)", "") + .to_string(); } } } @@ -329,7 +365,9 @@ pub async fn run_app( if let Some(session) = state.current_session().cloned() { let s = store.clone(); tokio::spawn(async move { - let _ = tokio::task::spawn_blocking(move || s.save_session(&session)).await; + let _ = + tokio::task::spawn_blocking(move || s.save_session(&session)) + .await; }); } } @@ -340,7 +378,10 @@ pub async fn run_app( if is_assistant_append && !state.verification_in_flight { // Extract what we need before mutating state. let verify_info = state.current_session().and_then(|s| { - let node = s.proof.active_node_id.as_deref() + let node = s + .proof + .active_node_id + .as_deref() .and_then(|id| s.proof.nodes.iter().find(|n| n.id == id))?; if node.status == openproof_protocol::ProofNodeStatus::Proving && !node.content.trim().is_empty() @@ -358,19 +399,21 @@ pub async fn run_app( tokio::spawn(async move { let result = tokio::task::spawn_blocking(move || { openproof_lean::verify_scratch_content( - &lean_dir, &node_content, None, &imports, + &lean_dir, + &node_content, + None, + &imports, ) }) .await .ok() .and_then(|r| r.ok()); - let summary = result.unwrap_or_else(|| { - openproof_protocol::LeanVerificationSummary { + let summary = + result.unwrap_or_else(|| openproof_protocol::LeanVerificationSummary { ok: false, error: Some("Lean verification failed to run".to_string()), ..Default::default() - } - }); + }); let _ = tx_v.send(AppEvent::LeanVerifyFinished(summary)); }); } @@ -383,17 +426,15 @@ pub async fn run_app( let transcript_len = session.transcript.len(); let flushable = transcript_len.saturating_sub(1); if flushable > state.flushed_turn_count { - let entries_to_flush: Vec<_> = session.transcript - [state.flushed_turn_count..flushable] - .to_vec(); + let entries_to_flush: Vec<_> = + session.transcript[state.flushed_turn_count..flushable].to_vec(); let mut lines = Vec::new(); for entry in &entries_to_flush { lines.extend(openproof_tui::render_entry(entry)); } if !lines.is_empty() { - let _ = openproof_tui::insert_history::insert_history_lines( - terminal, lines, - ); + let _ = + openproof_tui::insert_history::insert_history_lines(terminal, lines); } state.flushed_turn_count = flushable; } @@ -466,7 +507,10 @@ fn handle_normal_mode_key( KeyCode::BackTab => { // Shift+Tab: cycle autonomous mode (off -> normal -> full -> off) if let Some(session) = state.current_session_mut() { - let (new_running, new_full, label) = match (session.proof.is_autonomous_running, session.proof.full_autonomous) { + let (new_running, new_full, label) = match ( + session.proof.is_autonomous_running, + session.proof.full_autonomous, + ) { (false, _) => (true, false, "autonomous on"), (true, false) => (true, true, "full autonomous on"), (true, true) => (false, false, "autonomous off"), @@ -546,8 +590,7 @@ fn handle_normal_mode_key( Some(AppEvent::DeleteWordBackward) } KeyCode::Char('/') - if state.composer.is_empty() - && !key.modifiers.contains(KeyModifiers::CONTROL) => + if state.composer.is_empty() && !key.modifiers.contains(KeyModifiers::CONTROL) => { state.command_mode = true; state.command_buffer.clear(); diff --git a/crates/openproof-cli/src/export.rs b/crates/openproof-cli/src/export.rs index c43da0c..f1ab798 100644 --- a/crates/openproof-cli/src/export.rs +++ b/crates/openproof-cli/src/export.rs @@ -208,8 +208,8 @@ pub fn export_session_artifacts( .and_then(|id| session.proof.branches.iter().find(|branch| branch.id == id)) { if !branch.lean_snippet.trim().is_empty() { - let path = export_dir - .join(format!("{}_branch.lean", sanitize_file_stem(&branch.title))); + let path = + export_dir.join(format!("{}_branch.lean", sanitize_file_stem(&branch.title))); fs::write(&path, branch.lean_snippet.trim())?; written.push(path.display().to_string()); } diff --git a/crates/openproof-cli/src/helpers.rs b/crates/openproof-cli/src/helpers.rs index 131b115..d2e4bd1 100644 --- a/crates/openproof-cli/src/helpers.rs +++ b/crates/openproof-cli/src/helpers.rs @@ -10,18 +10,17 @@ use anyhow::Result; use openproof_core::{AppEvent, AppState, PendingWrite}; use openproof_protocol::{AgentRole, ProofBranch, SessionSnapshot, ShareMode}; use openproof_store::AppStore; -use std::{env, path::{Path, PathBuf}}; +use std::{ + env, + path::{Path, PathBuf}, +}; use tokio::sync::mpsc; // --------------------------------------------------------------------------- // Persist plumbing // --------------------------------------------------------------------------- -pub fn persist_write( - tx: mpsc::UnboundedSender, - store: AppStore, - write: PendingWrite, -) { +pub fn persist_write(tx: mpsc::UnboundedSender, store: AppStore, write: PendingWrite) { let session_id = write.session.id.clone(); // Paper.tex is a workspace file managed by the model via file_write/file_patch. // Read it from the workspace on every save so the dashboard has the latest. @@ -208,17 +207,17 @@ pub fn autonomous_stop_reason_with_mode( // Always need a target if session.proof.accepted_target.is_none() && session.proof.formal_target.is_none() { - return Some( - "Set or accept a formal target before running autonomous search.".to_string(), - ); + return Some("Set or accept a formal target before running autonomous search.".to_string()); } if full_autonomous { // Full autonomous: only stop if ALL nodes are verified (proof complete) let all_verified = !session.proof.nodes.is_empty() - && session.proof.nodes.iter().all(|n| { - n.status == openproof_protocol::ProofNodeStatus::Verified - }); + && session + .proof + .nodes + .iter() + .all(|n| n.status == openproof_protocol::ProofNodeStatus::Verified); if all_verified { return Some("All proof nodes verified.".to_string()); } @@ -366,9 +365,7 @@ pub fn index_verified_item(store: AppStore, identity_key: String, module_name: S let store_ref = store.clone(); let ik = identity_key.clone(); let mn = module_name.clone(); - let _ = tokio::task::spawn_blocking(move || { - store_ref.auto_tag_from_module(&ik, &mn) - }).await; + let _ = tokio::task::spawn_blocking(move || store_ref.auto_tag_from_module(&ik, &mn)).await; }); } @@ -384,8 +381,16 @@ pub fn embed_verified_item( artifact_content: String, ) { tokio::spawn(async move { - use openproof_store::embeddings::{build_embedding_text, generate_embedding, EmbeddingStore}; - let text = build_embedding_text(&label, &statement, &decl_kind, &module_name, &artifact_content); + use openproof_store::embeddings::{ + build_embedding_text, generate_embedding, EmbeddingStore, + }; + let text = build_embedding_text( + &label, + &statement, + &decl_kind, + &module_name, + &artifact_content, + ); let Some(embedding) = generate_embedding(&text).await else { return; // No API key or API error -- skip silently }; @@ -394,7 +399,15 @@ pub fn embed_verified_item( Err(_) => return, // Qdrant not running -- skip silently }; let _ = store - .upsert_item(&identity_key, &label, &statement, &decl_kind, &module_name, &artifact_content, embedding) + .upsert_item( + &identity_key, + &label, + &statement, + &decl_kind, + &module_name, + &artifact_content, + embedding, + ) .await; }); } @@ -408,7 +421,9 @@ pub fn populate_knowledge_graph(store: &AppStore, session_id: &str) { for (path, _) in &files { if path.ends_with(".lean") && !path.contains("history/") { if let Ok(content) = std::fs::read_to_string(ws_dir.join(path)) { - if !all_lean.is_empty() { all_lean.push_str("\n\n"); } + if !all_lean.is_empty() { + all_lean.push_str("\n\n"); + } all_lean.push_str(&content); } } @@ -422,15 +437,18 @@ pub fn populate_knowledge_graph(store: &AppStore, session_id: &str) { // Build identity keys matching the format used by record_verification_result: // user-verified/{session_id}/{label}/{hash_of_signature} let key_for = |name: &str, sig: &str| -> String { - format!("user-verified/{}/{}/{}", + format!( + "user-verified/{}/{}/{}", openproof_store::sanitize_identity_segment(session_id), openproof_store::sanitize_identity_segment(name), openproof_store::corpus_hash(sig), ) }; // Build a lookup from name -> (name, signature) - let sig_map: std::collections::HashMap<&str, &str> = parsed.iter() - .map(|d| (d.name.as_str(), d.signature.as_str())).collect(); + let sig_map: std::collections::HashMap<&str, &str> = parsed + .iter() + .map(|d| (d.name.as_str(), d.signature.as_str())) + .collect(); for decl in &parsed { let from_key = key_for(&decl.name, &decl.signature); for dep in openproof_lean::parse::extract_dependencies(&decl.body, &all_names, &decl.name) { @@ -442,4 +460,3 @@ pub fn populate_knowledge_graph(store: &AppStore, session_id: &str) { let _ = store.auto_tag_from_module(&from_key, &decl.name); } } - diff --git a/crates/openproof-cli/src/key_handling.rs b/crates/openproof-cli/src/key_handling.rs index b106d8d..59a7f1e 100644 --- a/crates/openproof-cli/src/key_handling.rs +++ b/crates/openproof-cli/src/key_handling.rs @@ -6,10 +6,10 @@ use crate::helpers::{emit_local_notice, persist_write}; use crossterm::event::{self, KeyCode, KeyModifiers}; +use openproof_core::AppEvent; use openproof_core::AppState; use openproof_store::AppStore; use tokio::sync::mpsc; -use openproof_core::AppEvent; pub fn handle_overlay_key( key: event::KeyEvent, @@ -43,13 +43,7 @@ pub fn handle_overlay_key( state.sync_question_selection(); } Err(e) => { - emit_local_notice( - tx.clone(), - state, - store.clone(), - "Resume Error", - e, - ); + emit_local_notice(tx.clone(), state, store.clone(), "Resume Error", e); } } } @@ -59,21 +53,22 @@ pub fn handle_overlay_key( state.overlay = Some(openproof_core::Overlay::SessionPicker { selected }); } }, - openproof_core::Overlay::FocusPicker { items, mut selected } => match key.code { + openproof_core::Overlay::FocusPicker { + items, + mut selected, + } => match key.code { KeyCode::Esc => { // Close without action. } KeyCode::Up => { selected = selected.saturating_sub(1); - state.overlay = - Some(openproof_core::Overlay::FocusPicker { items, selected }); + state.overlay = Some(openproof_core::Overlay::FocusPicker { items, selected }); } KeyCode::Down => { if selected + 1 < items.len() { selected += 1; } - state.overlay = - Some(openproof_core::Overlay::FocusPicker { items, selected }); + state.overlay = Some(openproof_core::Overlay::FocusPicker { items, selected }); } KeyCode::Enter => { if let Some((id, _label, _kind)) = items.get(selected) { @@ -90,20 +85,13 @@ pub fn handle_overlay_key( } Ok(None) => {} Err(e) => { - emit_local_notice( - tx.clone(), - state, - store.clone(), - "Focus Error", - e, - ); + emit_local_notice(tx.clone(), state, store.clone(), "Focus Error", e); } } } } _ => { - state.overlay = - Some(openproof_core::Overlay::FocusPicker { items, selected }); + state.overlay = Some(openproof_core::Overlay::FocusPicker { items, selected }); } }, } @@ -150,7 +138,7 @@ pub fn handle_command_mode_key( session: submission.session_snapshot.clone(), }, ); - handle_submission(tx.clone(), store.clone(), state, submission, prover.clone()); + handle_submission(tx.clone(), store.clone(), state, submission, prover.clone()); } } } @@ -197,8 +185,7 @@ pub fn handle_command_mode_key( KeyCode::Char('u') if key.modifiers.contains(KeyModifiers::CONTROL) => { state.command_buffer.drain(..state.command_cursor); state.command_cursor = 0; - state.command_completions = - openproof_core::command_completions(&state.command_buffer); + state.command_completions = openproof_core::command_completions(&state.command_buffer); state.completion_idx = None; } KeyCode::Char('w') if key.modifiers.contains(KeyModifiers::CONTROL) => { @@ -217,8 +204,7 @@ pub fn handle_command_mode_key( KeyCode::Char(c) if !key.modifiers.contains(KeyModifiers::CONTROL) => { state.command_buffer.insert(state.command_cursor, c); state.command_cursor += c.len_utf8(); - state.command_completions = - openproof_core::command_completions(&state.command_buffer); + state.command_completions = openproof_core::command_completions(&state.command_buffer); state.completion_idx = None; } KeyCode::Backspace => { diff --git a/crates/openproof-cli/src/main.rs b/crates/openproof-cli/src/main.rs index 70a19fc..dd31c3b 100644 --- a/crates/openproof-cli/src/main.rs +++ b/crates/openproof-cli/src/main.rs @@ -13,16 +13,28 @@ mod system_prompt; mod turn_handling; use anyhow::{bail, Result}; -use shell::{run_ask, run_dashboard, run_health, run_ingest_corpus, run_login, run_recluster_corpus, run_shell}; +use shell::{ + run_ask, run_dashboard, run_health, run_ingest_corpus, run_login, run_recluster_corpus, + run_shell, +}; use std::{env, path::PathBuf}; enum Command { Shell, Health, Login, - Ask { prompt: String }, - Run { problem: String, label: Option, resume: Option }, - Dashboard { open: bool, port: Option }, + Ask { + prompt: String, + }, + Run { + problem: String, + label: Option, + resume: Option, + }, + Dashboard { + open: bool, + port: Option, + }, ReclusterCorpus, IngestCorpus, Help, @@ -44,9 +56,11 @@ async fn main() -> Result<()> { Command::Health => run_health(options.launch_cwd).await, Command::Login => run_login().await, Command::Ask { prompt } => run_ask(prompt).await, - Command::Run { problem, label, resume } => { - autonomous_headless::run_autonomous(options.launch_cwd, problem, label, resume).await - } + Command::Run { + problem, + label, + resume, + } => autonomous_headless::run_autonomous(options.launch_cwd, problem, label, resume).await, Command::Dashboard { open, port } => run_dashboard(options.launch_cwd, open, port).await, Command::ReclusterCorpus => run_recluster_corpus().await, Command::IngestCorpus => run_ingest_corpus().await, @@ -99,8 +113,7 @@ fn parse_args(args: Vec) -> Result { }); } - if args.iter().any(|arg| arg == "--login") - || args.first().map(String::as_str) == Some("login") + if args.iter().any(|arg| arg == "--login") || args.first().map(String::as_str) == Some("login") { return Ok(CliOptions { command: Command::Login, @@ -193,7 +206,11 @@ fn parse_args(args: Vec) -> Result { bail!("openproof run requires a problem or --resume . Usage: openproof run \"\" [--label ] [--resume ]"); } return Ok(CliOptions { - command: Command::Run { problem, label, resume }, + command: Command::Run { + problem, + label, + resume, + }, launch_cwd, }); } diff --git a/crates/openproof-cli/src/setup/app.rs b/crates/openproof-cli/src/setup/app.rs index e021faa..4ed1e37 100644 --- a/crates/openproof-cli/src/setup/app.rs +++ b/crates/openproof-cli/src/setup/app.rs @@ -36,13 +36,20 @@ pub struct SetupApp { } pub const PROVIDERS: &[(&str, &str, bool)] = &[ - ("codex", "Codex (ChatGPT) -- uses existing openproof login", false), + ( + "codex", + "Codex (ChatGPT) -- uses existing openproof login", + false, + ), ("openai", "OpenAI API -- requires OPENAI_API_KEY", true), ("anthropic", "Anthropic -- requires ANTHROPIC_API_KEY", true), ]; pub const CORPUS_MODES: &[(&str, &str)] = &[ - ("cloud", "Cloud (recommended) -- faster proofs, larger search corpus"), + ( + "cloud", + "Cloud (recommended) -- faster proofs, larger search corpus", + ), ("local", "Local only -- auto-imports Mathlib, no network"), ]; diff --git a/crates/openproof-cli/src/setup/mod.rs b/crates/openproof-cli/src/setup/mod.rs index 5ae5703..c40a02d 100644 --- a/crates/openproof-cli/src/setup/mod.rs +++ b/crates/openproof-cli/src/setup/mod.rs @@ -37,12 +37,10 @@ pub fn is_setup_complete() -> bool { return false; } match std::fs::read_to_string(&path) { - Ok(content) => { - serde_json::from_str::(&content) - .ok() - .and_then(|v| v.get("setup_complete")?.as_bool()) - .unwrap_or(false) - } + Ok(content) => serde_json::from_str::(&content) + .ok() + .and_then(|v| v.get("setup_complete")?.as_bool()) + .unwrap_or(false), Err(_) => false, } } diff --git a/crates/openproof-cli/src/setup/ui.rs b/crates/openproof-cli/src/setup/ui.rs index ee28e24..cb7dc09 100644 --- a/crates/openproof-cli/src/setup/ui.rs +++ b/crates/openproof-cli/src/setup/ui.rs @@ -6,7 +6,7 @@ use ratatui::text::{Line, Span}; use ratatui::widgets::{Paragraph, Wrap}; use ratatui::Frame; -use super::app::{SetupApp, Step, CORPUS_MODES, PROVIDERS, PROVER_MODELS}; +use super::app::{SetupApp, Step, CORPUS_MODES, PROVER_MODELS, PROVIDERS}; pub fn draw(f: &mut Frame, app: &SetupApp) { let area = f.area(); @@ -14,7 +14,7 @@ pub fn draw(f: &mut Frame, app: &SetupApp) { .direction(Direction::Vertical) .constraints([ Constraint::Length(3), // title - Constraint::Min(10), // content + Constraint::Min(10), // content Constraint::Length(1), // footer ]) .split(area); @@ -87,7 +87,9 @@ fn draw_provider_step(f: &mut Frame, app: &SetupApp, area: Rect) { let selected = i == app.provider_selected; let marker = if selected { "> " } else { " " }; let style = if selected { - Style::default().fg(Color::Cyan).add_modifier(Modifier::BOLD) + Style::default() + .fg(Color::Cyan) + .add_modifier(Modifier::BOLD) } else { Style::default().fg(Color::White) }; @@ -141,7 +143,9 @@ fn draw_corpus_step(f: &mut Frame, app: &SetupApp, area: Rect) { let selected = i == app.corpus_selected; let marker = if selected { "> " } else { " " }; let style = if selected { - Style::default().fg(Color::Cyan).add_modifier(Modifier::BOLD) + Style::default() + .fg(Color::Cyan) + .add_modifier(Modifier::BOLD) } else { Style::default().fg(Color::White) }; @@ -179,7 +183,9 @@ fn draw_prover_step(f: &mut Frame, app: &SetupApp, area: Rect) { let selected = i == app.prover_selected; let marker = if selected { "> " } else { " " }; let style = if selected { - Style::default().fg(Color::Cyan).add_modifier(Modifier::BOLD) + Style::default() + .fg(Color::Cyan) + .add_modifier(Modifier::BOLD) } else { Style::default().fg(Color::White) }; diff --git a/crates/openproof-cli/src/shell.rs b/crates/openproof-cli/src/shell.rs index cf79554..12a374c 100644 --- a/crates/openproof-cli/src/shell.rs +++ b/crates/openproof-cli/src/shell.rs @@ -119,7 +119,10 @@ pub async fn run_shell(launch_cwd: PathBuf) -> Result<()> { loop { match cloud.fetch_all_user_verified(500, offset).await { Ok((items, total)) => { - eprintln!("[corpus-module] Cloud: fetched {} items (total: {total})", items.len()); + eprintln!( + "[corpus-module] Cloud: fetched {} items (total: {total})", + items.len() + ); let n = items.len(); for item in items { all_items.push(openproof_lean::corpus_module::CorpusDeclaration { @@ -128,7 +131,9 @@ pub async fn run_shell(launch_cwd: PathBuf) -> Result<()> { artifact_content: item.artifact_content, }); } - if n < 500 { break; } + if n < 500 { + break; + } offset += 500; } Err(e) => { @@ -142,12 +147,15 @@ pub async fn run_shell(launch_cwd: PathBuf) -> Result<()> { // Always supplement with local user-verified items (may have items not yet synced) let local_result = tokio::task::spawn_blocking(move || { store_for_corpus.list_user_verified_with_artifacts() - }).await; + }) + .await; if let Ok(Ok(local_items)) = local_result { for (label, statement, content) in local_items { if !all_items.iter().any(|i| i.label == label) { all_items.push(openproof_lean::corpus_module::CorpusDeclaration { - label, statement, artifact_content: content, + label, + statement, + artifact_content: content, }); } } @@ -158,18 +166,23 @@ pub async fn run_shell(launch_cwd: PathBuf) -> Result<()> { return; } - eprintln!("[corpus-module] Building module with {} declarations", all_items.len()); + eprintln!( + "[corpus-module] Building module with {} declarations", + all_items.len() + ); let _ = tokio::task::spawn_blocking(move || { openproof_lean::corpus_module::build_corpus_module(&pd, &all_items) - }).await; + }) + .await; }); } // Spawn Pantograph in background (loads Mathlib ~18s). // TUI launches immediately. Tool calls wait for it via the OnceCell. let lean_project_dir = resolve_lean_project_dir(); - let session_prover: std::sync::Arc> = - std::sync::Arc::new(std::sync::OnceLock::new()); + let session_prover: std::sync::Arc< + std::sync::OnceLock, + > = std::sync::Arc::new(std::sync::OnceLock::new()); { let slot = session_prover.clone(); let pd = lean_project_dir.clone(); @@ -190,8 +203,19 @@ pub async fn run_shell(launch_cwd: PathBuf) -> Result<()> { let mut terminal = openproof_tui::custom_terminal::CustomTerminal::with_options(backend)?; let size = terminal.size()?; terminal.set_viewport_area(ratatui::layout::Rect::new(0, 0, size.width, size.height)); - let app_result = run_app(&mut terminal, store, &mut state, tx, &mut rx, session_prover.clone()).await; - let _ = crossterm::execute!(terminal.backend_mut(), crossterm::event::DisableBracketedPaste); + let app_result = run_app( + &mut terminal, + store, + &mut state, + tx, + &mut rx, + session_prover.clone(), + ) + .await; + let _ = crossterm::execute!( + terminal.backend_mut(), + crossterm::event::DisableBracketedPaste + ); disable_raw_mode()?; terminal.show_cursor()?; terminal.clear()?; @@ -245,7 +269,10 @@ pub async fn run_ask(prompt: String) -> Result<()> { let response = run_codex_turn(CodexTurnRequest { session_id: &session_id, messages: &[ - TurnMessage::chat("system", "You are openproof, a concise formal math assistant."), + TurnMessage::chat( + "system", + "You are openproof, a concise formal math assistant.", + ), TurnMessage::chat("user", prompt), ], model: "gpt-5.4", @@ -287,9 +314,9 @@ pub async fn run_ingest_corpus() -> Result<()> { let store = AppStore::open(StorePaths::detect()?)?; let lean_root = crate::helpers::resolve_lean_project_dir(); eprintln!("Ingesting library seeds from {}...", lean_root.display()); - let results = tokio::task::spawn_blocking(move || { - store.ingest_default_library_seeds(&lean_root) - }).await??; + let results = + tokio::task::spawn_blocking(move || store.ingest_default_library_seeds(&lean_root)) + .await??; if results.is_empty() { eprintln!("No library seed packages found."); } else { diff --git a/crates/openproof-cli/src/slash_autonomous.rs b/crates/openproof-cli/src/slash_autonomous.rs index 1414a46..2939e97 100644 --- a/crates/openproof-cli/src/slash_autonomous.rs +++ b/crates/openproof-cli/src/slash_autonomous.rs @@ -14,7 +14,11 @@ pub fn cmd_autonomous( store: AppStore, arg_text: &str, ) { - let subcommand = if arg_text.is_empty() { "status" } else { arg_text }; + let subcommand = if arg_text.is_empty() { + "status" + } else { + arg_text + }; match subcommand { "status" => { let content = state @@ -118,10 +122,8 @@ pub fn cmd_autonomous( return; } }; - if let Some(reason) = - crate::helpers::autonomous_stop_reason(&session).filter(|reason| { - !reason.contains("completed the current proof run") - }) + if let Some(reason) = crate::helpers::autonomous_stop_reason(&session) + .filter(|reason| !reason.contains("completed the current proof run")) { emit_local_notice(tx, state, store, "Autonomous Error", reason); return; @@ -169,7 +171,13 @@ pub fn cmd_autonomous( let session = match state.current_session().cloned() { Some(s) => s, None => { - emit_local_notice(tx, state, store, "Autonomous Error", "No active session.".to_string()); + emit_local_notice( + tx, + state, + store, + "Autonomous Error", + "No active session.".to_string(), + ); return; } }; @@ -177,10 +185,18 @@ pub fn cmd_autonomous( match state.set_autonomous_run_state(AutonomousRunPatch { is_autonomous_running: Some(true), autonomous_started_at: Some(Some( - session.proof.autonomous_started_at.clone().unwrap_or(now.clone()), + session + .proof + .autonomous_started_at + .clone() + .unwrap_or(now.clone()), )), autonomous_last_progress_at: Some( - session.proof.autonomous_last_progress_at.clone().or(Some(now)), + session + .proof + .autonomous_last_progress_at + .clone() + .or(Some(now)), ), autonomous_pause_reason: Some(None), autonomous_stop_reason: Some(None), @@ -216,12 +232,10 @@ pub fn cmd_autonomous( } Err(error) => emit_local_notice(tx, state, store, "Autonomous Error", error), }, - "step" => { - match crate::autonomous::run_autonomous_step(tx.clone(), store.clone(), state) { - Ok(message) => emit_local_notice(tx, state, store, "Autonomous", message), - Err(error) => emit_local_notice(tx, state, store, "Autonomous Error", error), - } - } + "step" => match crate::autonomous::run_autonomous_step(tx.clone(), store.clone(), state) { + Ok(message) => emit_local_notice(tx, state, store, "Autonomous", message), + Err(error) => emit_local_notice(tx, state, store, "Autonomous Error", error), + }, _ => emit_local_notice( tx, state, @@ -281,7 +295,13 @@ pub fn cmd_answer( session: submitted.session_snapshot.clone(), }, ); - handle_submission(tx, store, state, submitted, std::sync::Arc::new(std::sync::OnceLock::new())); + handle_submission( + tx, + store, + state, + submitted, + std::sync::Arc::new(std::sync::OnceLock::new()), + ); } else { emit_local_notice( tx, @@ -334,7 +354,13 @@ pub fn start_verify_active_node( let session = match state.current_session().cloned() { Some(session) => session, None => { - emit_local_notice(tx, state, store, "Verify Error", "No active session.".to_string()); + emit_local_notice( + tx, + state, + store, + "Verify Error", + "No active session.".to_string(), + ); return; } }; diff --git a/crates/openproof-cli/src/slash_commands.rs b/crates/openproof-cli/src/slash_commands.rs index bbc9e85..a43c605 100644 --- a/crates/openproof-cli/src/slash_commands.rs +++ b/crates/openproof-cli/src/slash_commands.rs @@ -10,7 +10,9 @@ //! - `slash_autonomous`: `/autonomous`, `/answer`, `/theorem`, `/lemma`, `/verify` use crate::export::{append_memory_entry, export_session_artifacts}; -use crate::helpers::{emit_local_notice, parse_agent_role, persist_write, resolve_lean_project_dir}; +use crate::helpers::{ + emit_local_notice, parse_agent_role, persist_write, resolve_lean_project_dir, +}; use crate::slash_autonomous::{ apply_statement_command, cmd_answer, cmd_autonomous, start_verify_active_node, }; @@ -89,8 +91,11 @@ pub fn apply_local_command( emit_local_notice(tx, state, store, "Tasks", state.tasks_report()); } "/new" => { - let write = - state.create_session(if arg_text.is_empty() { None } else { Some(arg_text) }); + let write = state.create_session(if arg_text.is_empty() { + None + } else { + Some(arg_text) + }); persist_write(tx.clone(), store.clone(), write); emit_local_notice( tx, @@ -107,8 +112,11 @@ pub fn apply_local_command( ); } "/clear" => { - let write = - state.create_session(if arg_text.is_empty() { None } else { Some(arg_text) }); + let write = state.create_session(if arg_text.is_empty() { + None + } else { + Some(arg_text) + }); persist_write(tx.clone(), store.clone(), write); emit_local_notice( tx, @@ -144,9 +152,7 @@ pub fn apply_local_command( .unwrap_or_else(|| arg_text.to_string()) ), ), - Err(error) => { - emit_local_notice(tx, state, store, "Session Error", error) - } + Err(error) => emit_local_notice(tx, state, store, "Session Error", error), } } } @@ -165,10 +171,8 @@ pub fn apply_local_command( "No focusable targets (no nodes or branches).".to_string(), ); } else { - state.overlay = Some(openproof_core::Overlay::FocusPicker { - items, - selected: 0, - }); + state.overlay = + Some(openproof_core::Overlay::FocusPicker { items, selected: 0 }); } } else if arg_text == "clear" { match state.focus_target(None) { @@ -273,7 +277,10 @@ pub fn apply_local_command( format!("History: {} files", history.len()), ]; if let Some(v) = verification { - lines.push(format!("Last check: {}", if v.ok { "OK" } else { "FAILED" })); + lines.push(format!( + "Last check: {}", + if v.ok { "OK" } else { "FAILED" } + )); if !v.ok { for line in v.stderr.lines().take(3) { lines.push(format!(" {line}")); @@ -303,11 +310,7 @@ pub fn apply_local_command( state, store.clone(), "Paper", - format!( - "{}\n\nWritten to: {}", - state.paper_report(), - path.display() - ), + format!("{}\n\nWritten to: {}", state.paper_report(), path.display()), ); } else { emit_local_notice(tx, state, store, "Paper", state.paper_report()); diff --git a/crates/openproof-cli/src/slash_share_corpus.rs b/crates/openproof-cli/src/slash_share_corpus.rs index a7a2e18..b3b65dc 100644 --- a/crates/openproof-cli/src/slash_share_corpus.rs +++ b/crates/openproof-cli/src/slash_share_corpus.rs @@ -24,7 +24,11 @@ pub fn cmd_share( format!("Share mode: {}", share_mode_label(session.cloud.share_mode)), format!( "Sync enabled: {}", - if session.cloud.sync_enabled { "yes" } else { "no" } + if session.cloud.sync_enabled { + "yes" + } else { + "no" + } ), format!( "Private overlay community: {}", @@ -155,9 +159,7 @@ pub fn cmd_corpus( ] .join("\n"), ), - Err(error) => { - emit_local_notice(tx, state, store, "Corpus Error", error.to_string()) - } + Err(error) => emit_local_notice(tx, state, store, "Corpus Error", error.to_string()), }, "search" => { if rest.is_empty() { @@ -221,9 +223,7 @@ pub fn cmd_corpus( } else { results .into_iter() - .map(|(package, count)| { - format!("{package}: {count} declarations") - }) + .map(|(package, count)| format!("{package}: {count} declarations")) .collect::>() .join("\n") }; @@ -279,7 +279,11 @@ pub fn cmd_sync( store: AppStore, arg_text: &str, ) { - let subcommand = if arg_text.is_empty() { "status" } else { arg_text }; + let subcommand = if arg_text.is_empty() { + "status" + } else { + arg_text + }; match subcommand { "status" => match store.get_sync_summary() { Ok(summary) => { @@ -290,7 +294,11 @@ pub fn cmd_sync( format!("Share mode: {}", share_mode_label(session.cloud.share_mode)), format!( "Sync enabled: {}", - if session.cloud.sync_enabled { "yes" } else { "no" } + if session.cloud.sync_enabled { + "yes" + } else { + "no" + } ), format!("Pending jobs: {}", summary.pending_count), format!("Failed jobs: {}", summary.failed_count), @@ -357,7 +365,13 @@ pub fn start_sync_drain( store: AppStore, ) { let Some(session) = state.current_session().cloned() else { - emit_local_notice(tx, state, store, "Sync Error", "No active session.".to_string()); + emit_local_notice( + tx, + state, + store, + "Sync Error", + "No active session.".to_string(), + ); return; }; if !session.cloud.sync_enabled { @@ -394,7 +408,10 @@ pub fn start_sync_drain( let sync_enabled = session.cloud.sync_enabled; tokio::spawn(async move { let corpus = openproof_corpus::CorpusManager::new(store, cloud_client, PathBuf::from(".")); - match corpus.drain_sync_queue(share_mode, sync_enabled, None).await { + match corpus + .drain_sync_queue(share_mode, sync_enabled, None) + .await + { Ok(result) => { if result.sent > 0 { let _ = tx.send(AppEvent::SyncCompleted); diff --git a/crates/openproof-cli/src/system_prompt.rs b/crates/openproof-cli/src/system_prompt.rs index 280cbc7..45985aa 100644 --- a/crates/openproof-cli/src/system_prompt.rs +++ b/crates/openproof-cli/src/system_prompt.rs @@ -308,9 +308,16 @@ pub async fn retrieval_context(store: &AppStore, session: Option<&SessionSnapsho let mut corpus_hits: Vec<(String, String, String)> = Vec::new(); if session.cloud.share_mode != ShareMode::Local { let client = openproof_cloud::CloudCorpusClient::new(Default::default()); - if let Ok(remote) = client.search_verified_remote(&query, 10, session.cloud.share_mode, None).await { + if let Ok(remote) = client + .search_verified_remote(&query, 10, session.cloud.share_mode, None) + .await + { for hit in &remote { - corpus_hits.push((hit.label.clone(), hit.statement.clone(), "cloud".to_string())); + corpus_hits.push(( + hit.label.clone(), + hit.statement.clone(), + "cloud".to_string(), + )); } } } @@ -365,7 +372,10 @@ pub async fn retrieval_context(store: &AppStore, session: Option<&SessionSnapsho "Semantically similar verified lemmas:\n{}", new_hits .iter() - .map(|h| format!("- {} (similarity: {:.2}) :: {}", h.label, h.score, h.statement)) + .map(|h| format!( + "- {} (similarity: {:.2}) :: {}", + h.label, h.score, h.statement + )) .collect::>() .join("\n") )); @@ -404,8 +414,11 @@ pub fn transcript_entry_to_turn_message( MessageRole::User => "user", MessageRole::Assistant => "assistant", MessageRole::System => "system", - MessageRole::Notice | MessageRole::ToolCall | MessageRole::ToolResult - | MessageRole::Diff | MessageRole::Thought => return None, + MessageRole::Notice + | MessageRole::ToolCall + | MessageRole::ToolResult + | MessageRole::Diff + | MessageRole::Thought => return None, }; Some(TurnMessage::chat(role, entry.content)) } @@ -497,26 +510,33 @@ pub async fn build_branch_turn_messages( }, ] .join("\n\n"))]; - messages.push(TurnMessage::chat("user", format!( + messages.push(TurnMessage::chat( + "user", + format!( "Continue the branch task now.\nRole: {}\nTask: {}", agent_role_label(role), title - ))); + ), + )); // Include ALL workspace .lean files so branches see current codebase if let Ok(files) = store.list_workspace_files(&session.id) { let ws_dir = store.workspace_dir(&session.id); - let lean_files: Vec<_> = files.iter() + let lean_files: Vec<_> = files + .iter() .filter(|(p, _)| p.ends_with(".lean") && !p.contains("history/")) .collect(); if !lean_files.is_empty() { for (path, _) in &lean_files { if let Ok(content) = std::fs::read_to_string(ws_dir.join(path)) { if !content.trim().is_empty() && content.lines().count() <= 200 { - messages.push(TurnMessage::chat("user", format!( - "File: {path} ({} lines):\n```lean\n{content}\n```", - content.lines().count() - ))); + messages.push(TurnMessage::chat( + "user", + format!( + "File: {path} ({} lines):\n```lean\n{content}\n```", + content.lines().count() + ), + )); } } } @@ -527,14 +547,17 @@ pub async fn build_branch_turn_messages( } // Include active node status so branches know verification state - if let Some(node) = session.proof.nodes.iter() + if let Some(node) = session + .proof + .nodes + .iter() .find(|n| Some(n.id.as_str()) == session.proof.active_node_id.as_deref()) { if !node.content.trim().is_empty() { - messages.push(TurnMessage::chat("user", format!( - "Active node '{}' status: {:?}", - node.label, node.status - ))); + messages.push(TurnMessage::chat( + "user", + format!("Active node '{}' status: {:?}", node.label, node.status), + )); } } diff --git a/crates/openproof-cli/src/turn_handling.rs b/crates/openproof-cli/src/turn_handling.rs index 24067e9..7b010b1 100644 --- a/crates/openproof-cli/src/turn_handling.rs +++ b/crates/openproof-cli/src/turn_handling.rs @@ -13,12 +13,10 @@ use crate::system_prompt::{build_branch_turn_messages, build_turn_messages_with_ use openproof_core::{AppEvent, AppState, PendingWrite, SubmittedInput}; use openproof_lean::lsp_mcp::LeanLspMcp; use openproof_lean::tools::{execute_tool, ToolContext, ToolOutput}; -use std::sync::{Arc, Mutex}; -use openproof_model::{ - run_codex_turn_with_events, CodexTurnRequest, StreamEvent, TurnMessage, -}; +use openproof_model::{run_codex_turn_with_events, CodexTurnRequest, StreamEvent, TurnMessage}; use openproof_protocol::{AgentRole, AgentStatus, BranchQueueState, SessionSnapshot}; use openproof_store::AppStore; +use std::sync::{Arc, Mutex}; use tokio::sync::mpsc; /// Maximum number of tool-loop iterations per turn. @@ -116,7 +114,7 @@ pub async fn run_agentic_loop( messages: &messages, model: "gpt-5.4", reasoning_effort: "high", - include_tools: true, + include_tools: true, }, move |event| match event { StreamEvent::TextDelta(delta) => { @@ -176,7 +174,9 @@ pub async fn run_agentic_loop( let output = if call.name == "corpus_get" { let label = serde_json::from_str::(&call.arguments) .ok() - .and_then(|v| v.get("label").and_then(|q| q.as_str()).map(str::to_string)) + .and_then(|v| { + v.get("label").and_then(|q| q.as_str()).map(str::to_string) + }) .unwrap_or_default(); match store.get_artifact_content(&label) { Ok(Some(code)) => ToolOutput { @@ -191,7 +191,9 @@ pub async fn run_agentic_loop( } else if call.name == "corpus_search" { let query = serde_json::from_str::(&call.arguments) .ok() - .and_then(|v| v.get("query").and_then(|q| q.as_str()).map(str::to_string)) + .and_then(|v| { + v.get("query").and_then(|q| q.as_str()).map(str::to_string) + }) .unwrap_or_default(); let mut results = Vec::new(); @@ -217,14 +219,18 @@ pub async fn run_agentic_loop( // Cloud expansion is only useful when the local corpus doesn't have the answer. if !has_verified_proof { // Cloud semantic search + edge expansion - let cloud_client = openproof_cloud::CloudCorpusClient::new(Default::default()); + let cloud_client = + openproof_cloud::CloudCorpusClient::new(Default::default()); let _ = cloud_client.availability(); let mut cloud_identity_keys: Vec = Vec::new(); match cloud_client.search_semantic(&query, 10).await { Ok(semantic_hits) => { for hit in &semantic_hits { cloud_identity_keys.push(hit.identity_key.clone()); - let line = format!("- {} (sim:{:.2}) :: {}", hit.label, hit.score, hit.statement); + let line = format!( + "- {} (sim:{:.2}) :: {}", + hit.label, hit.score, hit.statement + ); if !results.iter().any(|r| r.contains(&hit.label)) { results.push(line); } @@ -253,13 +259,27 @@ pub async fn run_agentic_loop( if let Ok(failures) = cloud_client.search_failures(&query, 5).await { if !failures.is_empty() { results.push(String::new()); - results.push("KNOWN FAILURES (do NOT repeat these approaches):".to_string()); + results.push( + "KNOWN FAILURES (do NOT repeat these approaches):" + .to_string(), + ); for f in &failures { - let class = f.get("failureClass").and_then(|v| v.as_str()).unwrap_or(""); - let snippet = f.get("snippet").and_then(|v| v.as_str()).unwrap_or(""); - let diag = f.get("diagnostic").and_then(|v| v.as_str()).unwrap_or(""); + let class = f + .get("failureClass") + .and_then(|v| v.as_str()) + .unwrap_or(""); + let snippet = + f.get("snippet").and_then(|v| v.as_str()).unwrap_or(""); + let diag = f + .get("diagnostic") + .and_then(|v| v.as_str()) + .unwrap_or(""); if !snippet.is_empty() || !diag.is_empty() { - results.push(format!(" [{class}] {} -> {}", &snippet[..snippet.len().min(120)], &diag[..diag.len().min(120)])); + results.push(format!( + " [{class}] {} -> {}", + &snippet[..snippet.len().min(120)], + &diag[..diag.len().min(120)] + )); } } } @@ -267,9 +287,15 @@ pub async fn run_agentic_loop( } if results.is_empty() { - ToolOutput { success: true, content: "No results found.".to_string() } + ToolOutput { + success: true, + content: "No results found.".to_string(), + } } else { - ToolOutput { success: true, content: results.join("\n") } + ToolOutput { + success: true, + content: results.join("\n"), + } } } else { // All other tools: execute on a blocking thread @@ -318,10 +344,7 @@ pub async fn run_agentic_loop( }); // Append the tool result to messages for the next API call. - messages.push(TurnMessage::tool_result( - &call.call_id, - &output.content, - )); + messages.push(TurnMessage::tool_result(&call.call_id, &output.content)); } // Continue the loop: call the API again with tool results. } @@ -444,12 +467,16 @@ pub fn start_agent_branch_turn( let output = if call.name == "corpus_get" { let label = serde_json::from_str::(&call.arguments) .ok() - .and_then(|v| v.get("label").and_then(|q| q.as_str()).map(str::to_string)) + .and_then(|v| { + v.get("label").and_then(|q| q.as_str()).map(str::to_string) + }) .unwrap_or_default(); match store.get_artifact_content(&label) { Ok(Some(code)) => ToolOutput { success: true, - content: format!("Full proof code for `{label}`:\n```lean\n{code}\n```"), + content: format!( + "Full proof code for `{label}`:\n```lean\n{code}\n```" + ), }, _ => ToolOutput { success: false, @@ -459,7 +486,9 @@ pub fn start_agent_branch_turn( } else if call.name == "corpus_search" { let query = serde_json::from_str::(&call.arguments) .ok() - .and_then(|v| v.get("query").and_then(|q| q.as_str()).map(str::to_string)) + .and_then(|v| { + v.get("query").and_then(|q| q.as_str()).map(str::to_string) + }) .unwrap_or_default(); let mut results = Vec::new(); if let Ok(hits) = store.search_verified_corpus(&query, 10) { @@ -473,7 +502,10 @@ pub fn start_agent_branch_turn( for h in &hits { cloud_keys.push(h.identity_key.clone()); if !results.iter().any(|r| r.contains(&h.label)) { - results.push(format!("- {} (sim:{:.2}) :: {}", h.label, h.score, h.statement)); + results.push(format!( + "- {} (sim:{:.2}) :: {}", + h.label, h.score, h.statement + )); } } } @@ -482,7 +514,10 @@ pub fn start_agent_branch_turn( if let Ok(related) = cloud.get_related_items(key, 5).await { for item in &related { if !results.iter().any(|r| r.contains(&item.label)) { - results.push(format!("- {} ({}) :: {}", item.label, item.edge_type, item.statement)); + results.push(format!( + "- {} ({}) :: {}", + item.label, item.edge_type, item.statement + )); } } } @@ -493,18 +528,33 @@ pub fn start_agent_branch_turn( results.push(String::new()); results.push("KNOWN FAILURES (do NOT repeat):".to_string()); for f in &failures { - let class = f.get("failureClass").and_then(|v| v.as_str()).unwrap_or(""); - let snippet = f.get("snippet").and_then(|v| v.as_str()).unwrap_or(""); - let diag = f.get("diagnostic").and_then(|v| v.as_str()).unwrap_or(""); + let class = f + .get("failureClass") + .and_then(|v| v.as_str()) + .unwrap_or(""); + let snippet = + f.get("snippet").and_then(|v| v.as_str()).unwrap_or(""); + let diag = f + .get("diagnostic") + .and_then(|v| v.as_str()) + .unwrap_or(""); if !snippet.is_empty() || !diag.is_empty() { - results.push(format!(" [{class}] {} -> {}", &snippet[..snippet.len().min(120)], &diag[..diag.len().min(120)])); + results.push(format!( + " [{class}] {} -> {}", + &snippet[..snippet.len().min(120)], + &diag[..diag.len().min(120)] + )); } } } } ToolOutput { success: true, - content: if results.is_empty() { "No results.".to_string() } else { results.join("\n") }, + content: if results.is_empty() { + "No results.".to_string() + } else { + results.join("\n") + }, } } else { tokio::task::spawn_blocking({ @@ -540,10 +590,7 @@ pub fn start_agent_branch_turn( last_verify_ok = true; } } - all_messages.push(TurnMessage::tool_result( - &call.call_id, - &output.content, - )); + all_messages.push(TurnMessage::tool_result(&call.call_id, &output.content)); } } Err(error) => { @@ -639,8 +686,7 @@ pub fn start_branch_verification( .nodes .iter() .find(|n| { - Some(n.id.as_str()) - == verification_session.proof.active_node_id.as_deref() + Some(n.id.as_str()) == verification_session.proof.active_node_id.as_deref() }) .unwrap_or(&verification_session.proof.nodes[0]), ), @@ -660,8 +706,7 @@ pub fn start_branch_verification( .nodes .iter() .find(|n| { - Some(n.id.as_str()) - == verification_clone.proof.active_node_id.as_deref() + Some(n.id.as_str()) == verification_clone.proof.active_node_id.as_deref() }) .unwrap_or(&verification_clone.proof.nodes[0]), scratch.as_deref(), @@ -681,8 +726,7 @@ pub fn start_branch_verification( let embed_ok = result.ok; tokio::spawn(async move { let persisted = tokio::task::spawn_blocking(move || { - persist_store - .record_verification_result(&persist_session, &persist_result) + persist_store.record_verification_result(&persist_session, &persist_result) }) .await .ok() @@ -695,7 +739,10 @@ pub fn start_branch_verification( } // Embed + index verified items (fire-and-forget) if embed_ok { - if let Some(node) = embed_session.proof.active_node_id.as_deref() + if let Some(node) = embed_session + .proof + .active_node_id + .as_deref() .and_then(|id| embed_session.proof.nodes.iter().find(|n| n.id == id)) { let ik = format!("session/{}/{}", embed_session.id, node.id); @@ -826,8 +873,7 @@ pub fn ensure_hidden_agent_branch( return Ok((branch_id, snapshot)); } - let (write, branch_id, _task_id) = - state.spawn_agent_branch(role, title, description, true)?; + let (write, branch_id, _task_id) = state.spawn_agent_branch(role, title, description, true)?; let snapshot = write.session.clone(); persist_write(tx, store, write); Ok((branch_id, snapshot)) @@ -861,7 +907,13 @@ pub fn submit_selected_question_option( session: submitted.session_snapshot.clone(), }, ); - handle_submission(tx, store, state, submitted, std::sync::Arc::new(std::sync::OnceLock::new())); + handle_submission( + tx, + store, + state, + submitted, + std::sync::Arc::new(std::sync::OnceLock::new()), + ); } } @@ -873,15 +925,14 @@ pub fn persist_verification_result( ) { tokio::spawn(async move { let store2 = store.clone(); - let outcome = - tokio::task::spawn_blocking(move || { - let res = store.record_verification_result(&session, &result); - if result.ok { - crate::helpers::populate_knowledge_graph(&store2, &session.id); - } - res - }) - .await; + let outcome = tokio::task::spawn_blocking(move || { + let res = store.record_verification_result(&session, &result); + if result.ok { + crate::helpers::populate_knowledge_graph(&store2, &session.id); + } + res + }) + .await; match outcome { Ok(Ok(())) => {} Ok(Err(e)) => { diff --git a/crates/openproof-cloud/src/lib.rs b/crates/openproof-cloud/src/lib.rs index fb17ac3..e0bfca9 100644 --- a/crates/openproof-cloud/src/lib.rs +++ b/crates/openproof-cloud/src/lib.rs @@ -17,9 +17,7 @@ fn normalize_base_url(value: &str) -> Option { None } else { // Strip trailing /api or /api/ to prevent doubled paths like /api/api/v1/... - let cleaned = trimmed - .trim_end_matches('/') - .trim_end_matches("/api"); + let cleaned = trimmed.trim_end_matches('/').trim_end_matches("/api"); Some(cleaned.to_string()) } } @@ -152,7 +150,10 @@ impl CloudCorpusClient { headers.insert("content-type", val); } } - if let Some(token) = auth.and_then(|a| a.bearer_token.as_deref()).filter(|t| !t.trim().is_empty()) { + if let Some(token) = auth + .and_then(|a| a.bearer_token.as_deref()) + .filter(|t| !t.trim().is_empty()) + { if let Ok(val) = HeaderValue::from_str(&format!("Bearer {token}")) { headers.insert("authorization", val); } @@ -200,14 +201,11 @@ impl CloudCorpusClient { if share_mode == ShareMode::Local { return Ok(Vec::new()); } - let clamped_limit = limit.max(1).min(32); + let clamped_limit = limit.clamp(1, 32); let response = self .client .get(format!("{base_url}/api/v1/search")) - .query(&[ - ("query", query), - ("limit", &clamped_limit.to_string()), - ]) + .query(&[("query", query), ("limit", &clamped_limit.to_string())]) .headers(self.build_headers(auth, None)) .send() .await @@ -218,10 +216,8 @@ impl CloudCorpusClient { response.status().as_u16() ); } - let payload: CloudCorpusSearchResponse = response - .json() - .await - .context("parsing search response")?; + let payload: CloudCorpusSearchResponse = + response.json().await.context("parsing search response")?; Ok(payload.hits) } @@ -253,10 +249,7 @@ impl CloudCorpusClient { response.status().as_u16() ); } - response - .json() - .await - .context("parsing upload response") + response.json().await.context("parsing upload response") } /// Fetch a single artifact by ID. @@ -288,10 +281,8 @@ impl CloudCorpusClient { response.status().as_u16() ); } - let payload: CloudCorpusArtifactResponse = response - .json() - .await - .context("parsing artifact response")?; + let payload: CloudCorpusArtifactResponse = + response.json().await.context("parsing artifact response")?; Ok(Some(payload)) } @@ -317,10 +308,8 @@ impl CloudCorpusClient { response.status().as_u16() ); } - let payload: CloudCorpusPackagesResponse = response - .json() - .await - .context("parsing packages response")?; + let payload: CloudCorpusPackagesResponse = + response.json().await.context("parsing packages response")?; Ok(payload.packages) } @@ -335,7 +324,7 @@ impl CloudCorpusClient { Some(url) => url, None => return Ok(Vec::new()), }; - let clamped_limit = limit.max(1).min(32); + let clamped_limit = limit.clamp(1, 32); let response = match self .client .get(format!("{base_url}/api/v1/search/semantic")) @@ -351,7 +340,8 @@ impl CloudCorpusClient { if !response.status().is_success() { return Ok(Vec::new()); } - let payload: serde_json::Value = response.json().await.context("parsing semantic response")?; + let payload: serde_json::Value = + response.json().await.context("parsing semantic response")?; let hits = payload .get("hits") .and_then(|v| v.as_array()) @@ -361,7 +351,11 @@ impl CloudCorpusClient { Some(SemanticSearchHit { identity_key: h.get("identity_key")?.as_str()?.to_string(), label: h.get("label")?.as_str()?.to_string(), - statement: h.get("statement").and_then(|v| v.as_str()).unwrap_or("").to_string(), + statement: h + .get("statement") + .and_then(|v| v.as_str()) + .unwrap_or("") + .to_string(), score: h.get("score").and_then(|v| v.as_f64()).unwrap_or(0.0) as f32, }) }) @@ -372,10 +366,7 @@ impl CloudCorpusClient { } /// Upload a failed attempt to the cloud. - pub async fn upload_failed_attempt( - &self, - attempt: serde_json::Value, - ) -> Result<()> { + pub async fn upload_failed_attempt(&self, attempt: serde_json::Value) -> Result<()> { let base_url = match self.base_url() { Some(url) => url, None => return Ok(()), @@ -478,10 +469,7 @@ impl CloudCorpusClient { } /// Upload corpus edges to cloud. - pub async fn upload_corpus_edges( - &self, - edges: serde_json::Value, - ) -> Result<()> { + pub async fn upload_corpus_edges(&self, edges: serde_json::Value) -> Result<()> { let base_url = match self.base_url() { Some(url) => url, None => return Ok(()), @@ -523,14 +511,9 @@ impl CloudCorpusClient { response.status().as_u16() ); } - let payload: serde_json::Value = response - .json() - .await - .context("parsing export response")?; - let total = payload - .get("total") - .and_then(|v| v.as_u64()) - .unwrap_or(0) as usize; + let payload: serde_json::Value = + response.json().await.context("parsing export response")?; + let total = payload.get("total").and_then(|v| v.as_u64()).unwrap_or(0) as usize; let items = payload .get("items") .and_then(|v| v.as_array()) diff --git a/crates/openproof-core/src/apply.rs b/crates/openproof-core/src/apply.rs index bc77ac8..70febac 100644 --- a/crates/openproof-core/src/apply.rs +++ b/crates/openproof-core/src/apply.rs @@ -86,14 +86,23 @@ impl AppState { promote, result, } => { - return self.apply_branch_verify_finished(branch_id, focus_node_id, promote, result); + return self.apply_branch_verify_finished( + branch_id, + focus_node_id, + promote, + result, + ); } // --- Content appending --- AppEvent::AppendAssistant(content) => { return self.apply_append_assistant(content); } - AppEvent::AppendBranchAssistant { branch_id, content, used_tools } => { + AppEvent::AppendBranchAssistant { + branch_id, + content, + used_tools, + } => { return self.apply_append_branch_assistant(branch_id, content, used_tools); } AppEvent::FinishBranch { @@ -228,7 +237,12 @@ impl AppState { AppEvent::ProofGoalUpdated(goal) => { if let Some(session) = self.current_session_mut() { // Update existing goal or insert new one - if let Some(existing) = session.proof.proof_goals.iter_mut().find(|g| g.id == goal.id) { + if let Some(existing) = session + .proof + .proof_goals + .iter_mut() + .find(|g| g.id == goal.id) + { *existing = goal; } else { session.proof.proof_goals.push(goal); @@ -260,28 +274,29 @@ impl AppState { }; if let Some(session) = self.current_session_mut() { - session.transcript.push(openproof_protocol::TranscriptEntry { - id: format!("tactic_{sorry_line}_{}", chrono::Utc::now().timestamp_millis()), - role: openproof_protocol::MessageRole::Notice, - title: Some("Tactic Search".to_string()), - content: notice.clone(), - created_at: chrono::Utc::now().to_rfc3339(), - }); + session + .transcript + .push(openproof_protocol::TranscriptEntry { + id: format!( + "tactic_{sorry_line}_{}", + chrono::Utc::now().timestamp_millis() + ), + role: openproof_protocol::MessageRole::Notice, + title: Some("Tactic Search".to_string()), + content: notice.clone(), + created_at: chrono::Utc::now().to_rfc3339(), + }); } if solved && !tactics.is_empty() { let tactic_text = tactics.join("\n "); - self.status = format!( - "Tactic search solved line {sorry_line}: {tactic_text}" - ); + self.status = format!("Tactic search solved line {sorry_line}: {tactic_text}"); if let Some(session) = self.current_session_mut() { - if let Some(node) = session.proof.nodes.iter_mut().find(|n| n.id == node_id) { - let patched = replace_sorry_at_line( - &node.content, - sorry_line, - &tactic_text, - ); + if let Some(node) = session.proof.nodes.iter_mut().find(|n| n.id == node_id) + { + let patched = + replace_sorry_at_line(&node.content, sorry_line, &tactic_text); if patched != node.content { node.content = patched; node.updated_at = chrono::Utc::now().to_rfc3339(); diff --git a/crates/openproof-core/src/apply_content.rs b/crates/openproof-core/src/apply_content.rs index 81cc061..67f004b 100644 --- a/crates/openproof-core/src/apply_content.rs +++ b/crates/openproof-core/src/apply_content.rs @@ -28,7 +28,11 @@ impl AppState { if let Some(title) = parsed.title.as_ref().filter(|item| !item.trim().is_empty()) { session.title = title.trim().to_string(); } - if let Some(problem) = parsed.problem.as_ref().filter(|item| !item.trim().is_empty()) { + if let Some(problem) = parsed + .problem + .as_ref() + .filter(|item| !item.trim().is_empty()) + { session.proof.problem = Some(problem.trim().to_string()); } if let Some(formal_target) = parsed @@ -67,8 +71,7 @@ impl AppState { session.proof.paper_tex = tex.clone(); } if let Some(question) = parsed.question.clone() { - session.proof.status_line = - format!("Awaiting clarification: {}", question.prompt); + session.proof.status_line = format!("Awaiting clarification: {}", question.prompt); session.proof.phase = "formalizing".to_string(); session.proof.pending_question = Some(question); session.proof.awaiting_clarification = true; @@ -76,7 +79,8 @@ impl AppState { for created in &parsed.created_nodes { // Sub-lemmas are children of the current active node let parent = session.proof.active_node_id.clone(); - let depth = parent.as_deref() + let depth = parent + .as_deref() .and_then(|pid| session.proof.nodes.iter().find(|n| n.id == pid)) .map(|p| p.depth + 1) .unwrap_or(0); @@ -392,10 +396,13 @@ impl AppState { } // Add a visible notice to the main transcript so the user sees branch activity let role_label = crate::helpers::agent_role_label( - session.proof.branches.iter() + session + .proof + .branches + .iter() .find(|b| b.id == branch_id) .map(|b| b.role) - .unwrap_or(openproof_protocol::AgentRole::Prover) + .unwrap_or(openproof_protocol::AgentRole::Prover), ); let notice_content = match status { AgentStatus::Done => format!("{role_label}: {summary}"), @@ -480,14 +487,20 @@ impl AppState { // Push to session activity log let activity_msg = self.activity_label.clone(); if let Some(session) = self.current_session_mut() { - session.proof.activity_log.push(openproof_protocol::ActivityEntry { - timestamp: Utc::now().to_rfc3339(), - kind: "tool".to_string(), - message: activity_msg, - }); + session + .proof + .activity_log + .push(openproof_protocol::ActivityEntry { + timestamp: Utc::now().to_rfc3339(), + kind: "tool".to_string(), + message: activity_msg, + }); // Cap at 50 entries if session.proof.activity_log.len() > 50 { - session.proof.activity_log.drain(..session.proof.activity_log.len() - 50); + session + .proof + .activity_log + .drain(..session.proof.activity_log.len() - 50); } } let entry = TranscriptEntry { diff --git a/crates/openproof-core/src/apply_input.rs b/crates/openproof-core/src/apply_input.rs index 1e656a4..73488b0 100644 --- a/crates/openproof-core/src/apply_input.rs +++ b/crates/openproof-core/src/apply_input.rs @@ -69,7 +69,10 @@ impl AppState { pub(crate) fn apply_delete_forward(&mut self) { if self.focus == FocusPane::Composer && self.composer_cursor < self.composer.len() { - let deleted_char = self.composer[self.composer_cursor..].chars().next().unwrap(); + let deleted_char = self.composer[self.composer_cursor..] + .chars() + .next() + .unwrap(); if deleted_char == PASTE_MARKER { let marker_index = self.composer[..self.composer_cursor] .chars() diff --git a/crates/openproof-core/src/apply_streaming.rs b/crates/openproof-core/src/apply_streaming.rs index 5efced1..bb26a43 100644 --- a/crates/openproof-core/src/apply_streaming.rs +++ b/crates/openproof-core/src/apply_streaming.rs @@ -4,7 +4,7 @@ use openproof_protocol::{ }; use crate::helpers::{agent_role_label, next_id, summarize_lean_error}; -use crate::state::{AppState, AppEvent, PendingWrite}; +use crate::state::{AppEvent, AppState, PendingWrite}; impl AppState { pub(crate) fn apply_turn_started(&mut self) { @@ -95,33 +95,42 @@ impl AppState { // wipe multi-theorem sessions. let parsed_decls = openproof_lean::parse_lean_declarations(&result.rendered_scratch); if !parsed_decls.is_empty() && parsed_decls.len() >= session.proof.nodes.len() { - let parsed_nodes = openproof_lean::declarations_to_proof_nodes( - &parsed_decls, - &session.id, - ); + let parsed_nodes = + openproof_lean::declarations_to_proof_nodes(&parsed_decls, &session.id); let old_statuses: std::collections::HashMap = session - .proof.nodes.iter() + .proof + .nodes + .iter() .map(|n| (n.label.clone(), n.status)) .collect(); - let active_label = session.proof.active_node_id.as_deref() + let active_label = session + .proof + .active_node_id + .as_deref() .and_then(|id| session.proof.nodes.iter().find(|n| n.id == id)) .map(|n| n.label.clone()); - session.proof.nodes = parsed_nodes.iter().map(|pn| { - let mut node = pn.clone(); - if result.ok { - if let Some(&prev_status) = old_statuses.get(&node.label) { - if prev_status != ProofNodeStatus::Pending { - node.status = prev_status; + session.proof.nodes = parsed_nodes + .iter() + .map(|pn| { + let mut node = pn.clone(); + if result.ok { + if let Some(&prev_status) = old_statuses.get(&node.label) { + if prev_status != ProofNodeStatus::Pending { + node.status = prev_status; + } } } - } - node.updated_at = now.clone(); - node - }).collect(); + node.updated_at = now.clone(); + node + }) + .collect(); if let Some(label) = &active_label { - session.proof.active_node_id = session.proof.nodes.iter() + session.proof.active_node_id = session + .proof + .nodes + .iter() .find(|n| &n.label == label) .map(|n| n.id.clone()); } @@ -153,10 +162,17 @@ impl AppState { } // Phase from aggregate status - let all_verified = session.proof.nodes.iter() + let all_verified = session + .proof + .nodes + .iter() .all(|n| n.status == ProofNodeStatus::Verified); - let verified_count = session.proof.nodes.iter() - .filter(|n| n.status == ProofNodeStatus::Verified).count(); + let verified_count = session + .proof + .nodes + .iter() + .filter(|n| n.status == ProofNodeStatus::Verified) + .count(); let total = session.proof.nodes.len(); session.proof.phase = if all_verified && total > 0 { "done".to_string() @@ -244,14 +260,15 @@ impl AppState { if let Some(snapshot) = self.current_session_mut().map(|session| { // Parse Lean declarations from the rendered scratch to build proof tree if !result.rendered_scratch.is_empty() { - let parsed_decls = openproof_lean::parse_lean_declarations(&result.rendered_scratch); + let parsed_decls = + openproof_lean::parse_lean_declarations(&result.rendered_scratch); if !parsed_decls.is_empty() { - let parsed_nodes = openproof_lean::declarations_to_proof_nodes( - &parsed_decls, - &session.id, - ); + let parsed_nodes = + openproof_lean::declarations_to_proof_nodes(&parsed_decls, &session.id); for pn in &parsed_nodes { - if let Some(existing) = session.proof.nodes.iter_mut().find(|n| n.label == pn.label) { + if let Some(existing) = + session.proof.nodes.iter_mut().find(|n| n.label == pn.label) + { existing.content = pn.content.clone(); existing.statement = pn.statement.clone(); existing.kind = pn.kind; @@ -370,7 +387,9 @@ impl AppState { if root_target_verified { 100.0 } else { - branch.score.max(72.0 + (branch.attempt_count.min(8) as f32 * 3.0)) + branch + .score + .max(72.0 + (branch.attempt_count.min(8) as f32 * 3.0)) } } else { (branch.score - 4.0).max(0.0) @@ -396,13 +415,7 @@ impl AppState { }; session.proof.goal_summary = focus_node_id .as_deref() - .and_then(|node_id| { - session - .proof - .nodes - .iter() - .find(|node| node.id == node_id) - }) + .and_then(|node_id| session.proof.nodes.iter().find(|node| node.id == node_id)) .map(|node| node.statement.clone()) .or_else(|| session.proof.goal_summary.clone()); session.proof.status_line = status_line.clone(); @@ -432,8 +445,9 @@ impl AppState { if let Some(promote_branch_id) = promote_target { let previous_active = session.proof.active_foreground_branch_id.clone(); - if let Some(previous_id) = - previous_active.as_deref().filter(|id| *id != promote_branch_id) + if let Some(previous_id) = previous_active + .as_deref() + .filter(|id| *id != promote_branch_id) { if let Some(previous) = session .proof diff --git a/crates/openproof-core/src/helpers.rs b/crates/openproof-core/src/helpers.rs index d452e41..00b7642 100644 --- a/crates/openproof-core/src/helpers.rs +++ b/crates/openproof-core/src/helpers.rs @@ -66,11 +66,7 @@ pub fn summarize_lean_error(result: &LeanVerificationSummary) -> String { } else { "Lean verification failed." }; - message - .lines() - .take(12) - .collect::>() - .join("\n") + message.lines().take(12).collect::>().join("\n") } pub fn default_session_with_workspace( diff --git a/crates/openproof-core/src/lib.rs b/crates/openproof-core/src/lib.rs index b65a612..e940945 100644 --- a/crates/openproof-core/src/lib.rs +++ b/crates/openproof-core/src/lib.rs @@ -10,7 +10,9 @@ mod reports; mod session; mod state; -pub use commands::{build_focus_items, command_completions, delete_word_backward_pos, SLASH_COMMANDS}; +pub use commands::{ + build_focus_items, command_completions, delete_word_backward_pos, SLASH_COMMANDS, +}; pub use helpers::default_session_with_workspace; pub use parser::{ derive_goal_label, extract_latex_block, extract_lean_code_block, extract_lean_code_blocks, @@ -113,7 +115,11 @@ theorem PrimeGapTarget : ∀ C : ℝ, 0 ≤ C → True := by ); assert_eq!(session.proof.paper_notes.len(), 1); assert_eq!( - session.proof.nodes.first().map(|node| node.content.contains("theorem PrimeGapTarget")), + session + .proof + .nodes + .first() + .map(|node| node.content.contains("theorem PrimeGapTarget")), Some(true) ); } @@ -140,7 +146,9 @@ RECOMMENDED_OPTION: B assert!(state.has_open_question()); assert_eq!( - state.selected_question_option().map(|option| option.id.as_str()), + state + .selected_question_option() + .map(|option| option.id.as_str()), Some("B") ); } diff --git a/crates/openproof-core/src/parser.rs b/crates/openproof-core/src/parser.rs index cb2a650..ec0dbc1 100644 --- a/crates/openproof-core/src/parser.rs +++ b/crates/openproof-core/src/parser.rs @@ -120,7 +120,10 @@ pub fn parse_assistant_output(text: &str) -> ParsedAssistantOutput { continue; } if let Some((option_id, target)) = parse_option_target(line) { - if let Some(existing) = question_options.iter_mut().find(|option| option.id == option_id) { + if let Some(existing) = question_options + .iter_mut() + .find(|option| option.id == option_id) + { existing.formal_target = target; } else { question_options.push(ProofQuestionOption { @@ -207,7 +210,12 @@ pub fn derive_goal_label(title: &str) -> String { label = label.trim_matches('_').to_string(); if label.is_empty() { "goal".to_string() - } else if label.chars().next().map(|ch| ch.is_ascii_digit()).unwrap_or(false) { + } else if label + .chars() + .next() + .map(|ch| ch.is_ascii_digit()) + .unwrap_or(false) + { format!("goal_{label}") } else { label diff --git a/crates/openproof-core/src/proof.rs b/crates/openproof-core/src/proof.rs index ff24d57..9e88ef4 100644 --- a/crates/openproof-core/src/proof.rs +++ b/crates/openproof-core/src/proof.rs @@ -30,7 +30,8 @@ impl AppState { // If adding a sub-lemma, set parent to the current active node let parent = session.proof.active_node_id.clone(); let depth = if kind == ProofNodeKind::Lemma { - parent.as_deref() + parent + .as_deref() .and_then(|pid| session.proof.nodes.iter().find(|n| n.id == pid)) .map(|p| p.depth + 1) .unwrap_or(0) @@ -200,8 +201,7 @@ impl AppState { }); session.updated_at = timestamp; session.proof.hidden_branch_count = hidden.len(); - session.proof.hidden_best_branch_id = - hidden.first().map(|branch| branch.id.clone()); + session.proof.hidden_best_branch_id = hidden.first().map(|branch| branch.id.clone()); if let Some(value) = active_retrieval_summary { session.proof.active_retrieval_summary = value; } @@ -227,9 +227,7 @@ impl AppState { return Err("No active session.".to_string()); }; let previous_active = session.proof.active_foreground_branch_id.clone(); - if let Some(previous_id) = - previous_active.as_deref().filter(|id| *id != branch_id) - { + if let Some(previous_id) = previous_active.as_deref().filter(|id| *id != branch_id) { if let Some(previous) = session .proof .branches @@ -275,23 +273,16 @@ impl AppState { let promoted_id = branch.id.clone(); let promoted_role = branch.role; let promoted_focus_node_id = branch.focus_node_id.clone(); - let promoted_goal_summary = branch - .latest_goals - .clone() - .or_else(|| { - (!branch.goal_summary.trim().is_empty()) - .then(|| branch.goal_summary.clone()) - }); + let promoted_goal_summary = branch.latest_goals.clone().or_else(|| { + (!branch.goal_summary.trim().is_empty()).then(|| branch.goal_summary.clone()) + }); let promoted_latest_diagnostics = if resolved { None } else { - branch - .latest_diagnostics - .clone() - .or_else(|| { - (!branch.last_lean_diagnostic.trim().is_empty()) - .then(|| branch.last_lean_diagnostic.clone()) - }) + branch.latest_diagnostics.clone().or_else(|| { + (!branch.last_lean_diagnostic.trim().is_empty()) + .then(|| branch.last_lean_diagnostic.clone()) + }) }; session.updated_at = timestamp.clone(); @@ -328,8 +319,7 @@ impl AppState { .then_with(|| right.updated_at.cmp(&left.updated_at)) }); session.proof.hidden_branch_count = hidden.len(); - session.proof.hidden_best_branch_id = - hidden.first().map(|item| item.id.clone()); + session.proof.hidden_best_branch_id = hidden.first().map(|item| item.id.clone()); session.clone() }; self.pending_writes += 1; @@ -452,10 +442,7 @@ impl AppState { Ok((PendingWrite { session: snapshot }, branch_id, task_id)) } - pub fn focus_target( - &mut self, - target: Option<&str>, - ) -> Result, String> { + pub fn focus_target(&mut self, target: Option<&str>) -> Result, String> { let Some(target) = target.filter(|value| !value.trim().is_empty()) else { let timestamp = Utc::now().to_rfc3339(); let snapshot = { diff --git a/crates/openproof-core/src/reports.rs b/crates/openproof-core/src/reports.rs index 773380c..94a586f 100644 --- a/crates/openproof-core/src/reports.rs +++ b/crates/openproof-core/src/reports.rs @@ -29,7 +29,14 @@ impl AppState { [ format!("Session: {}", session.title), format!("Share mode: {:?}", session.cloud.share_mode), - format!("Sync enabled: {}", if session.cloud.sync_enabled { "yes" } else { "no" }), + format!( + "Sync enabled: {}", + if session.cloud.sync_enabled { + "yes" + } else { + "no" + } + ), format!("Proof phase: {}", session.proof.phase), format!("Status: {}", session.proof.status_line), format!( @@ -65,16 +72,17 @@ impl AppState { format!( "Active branch: {}", active_branch - .map(|branch| format!("{} [{}]", branch.title, format_agent_status(branch.status))) + .map(|branch| format!( + "{} [{}]", + branch.title, + format_agent_status(branch.status) + )) .unwrap_or_else(|| "none".to_string()) ), format!("Proof nodes: {}", session.proof.nodes.len()), format!("Branches: {}", session.proof.branches.len()), format!("Agents: {}", session.proof.agents.len()), - format!( - "Paper notes: {}", - session.proof.paper_notes.len() - ), + format!("Paper notes: {}", session.proof.paper_notes.len()), format!( "Pending question: {}", session @@ -86,7 +94,11 @@ impl AppState { ), format!( "Awaiting clarification: {}", - if session.proof.awaiting_clarification { "yes" } else { "no" } + if session.proof.awaiting_clarification { + "yes" + } else { + "no" + } ), format!( "Autonomous: {}", @@ -114,7 +126,11 @@ impl AppState { format!("Failed nodes: {}", failing), format!( "Assistant turn: {}", - if self.turn_in_flight { "running" } else { "idle" } + if self.turn_in_flight { + "running" + } else { + "idle" + } ), format!( "Lean verify: {}", @@ -127,7 +143,10 @@ impl AppState { format!( "Auth: {}", if self.auth.logged_in { - self.auth.email.clone().unwrap_or_else(|| "logged in".to_string()) + self.auth + .email + .clone() + .unwrap_or_else(|| "logged in".to_string()) } else { "logged out".to_string() } diff --git a/crates/openproof-core/src/session.rs b/crates/openproof-core/src/session.rs index 0a393a7..48c4797 100644 --- a/crates/openproof-core/src/session.rs +++ b/crates/openproof-core/src/session.rs @@ -28,9 +28,7 @@ impl AppState { pub fn has_open_question(&self) -> bool { self.pending_question() - .map(|question| { - question.status != "resolved" && !question.options.is_empty() - }) + .map(|question| question.status != "resolved" && !question.options.is_empty()) .unwrap_or(false) } @@ -223,10 +221,7 @@ impl AppState { Ok(PendingWrite { session: snapshot }) } - pub fn set_private_overlay_community( - &mut self, - enabled: bool, - ) -> Result { + pub fn set_private_overlay_community(&mut self, enabled: bool) -> Result { let timestamp = Utc::now().to_rfc3339(); let snapshot = { let Some(session) = self.current_session_mut() else { diff --git a/crates/openproof-core/src/state.rs b/crates/openproof-core/src/state.rs index 07a2fbc..873ce51 100644 --- a/crates/openproof-core/src/state.rs +++ b/crates/openproof-core/src/state.rs @@ -1,6 +1,5 @@ use openproof_protocol::{ - AuthSummary, LeanHealth, LeanVerificationSummary, AgentStatus, SessionSnapshot, - TranscriptEntry, + AgentStatus, AuthSummary, LeanHealth, LeanVerificationSummary, SessionSnapshot, TranscriptEntry, }; use crate::helpers::default_session_with_workspace; @@ -71,7 +70,11 @@ pub enum AppEvent { StreamFinished, ReasoningStarted, AppendAssistant(String), - AppendBranchAssistant { branch_id: String, content: String, used_tools: bool }, + AppendBranchAssistant { + branch_id: String, + content: String, + used_tools: bool, + }, FinishBranch { branch_id: String, status: AgentStatus, @@ -79,7 +82,10 @@ pub enum AppEvent { output: String, }, AutonomousTick, - AppendNotice { title: String, content: String }, + AppendNotice { + title: String, + content: String, + }, ToolCallReceived { call_id: String, tool_name: String, @@ -94,7 +100,10 @@ pub enum AppEvent { ToolLoopIteration(usize), /// Sync workspace file content into the active proof node. /// Emitted after a tool-using turn so node.content reflects what tools wrote. - WorkspaceContentSync { content: String, verified: bool }, + WorkspaceContentSync { + content: String, + verified: bool, + }, FocusNext, ToggleProofPane, SelectPrevQuestionOption, diff --git a/crates/openproof-corpus/src/ingest.rs b/crates/openproof-corpus/src/ingest.rs index 46dfd09..50135f2 100644 --- a/crates/openproof-corpus/src/ingest.rs +++ b/crates/openproof-corpus/src/ingest.rs @@ -6,11 +6,11 @@ use std::path::Path; use tokio::io::{AsyncBufReadExt, BufReader}; use tokio::process::Command; +use crate::manifest::read_lake_manifest; use crate::packages::{ collect_seed_packages, decl_namespace, environment_fingerprint, package_revision_set_hash, resolve_package_for_module, }; -use crate::manifest::read_lake_manifest; #[derive(Debug, Clone, serde::Deserialize)] #[serde(tag = "recordType", rename_all = "camelCase")] @@ -161,7 +161,9 @@ pub async fn run_library_seed_ingestion( let store = store.clone(); let run_id = run_id.clone(); let msg = msg.clone(); - move || store.finish_ingestion_run(&run_id, "failed", &serde_json::json!({}), Some(&msg)) + move || { + store.finish_ingestion_run(&run_id, "failed", &serde_json::json!({}), Some(&msg)) + } }) .await??; anyhow::bail!("{msg}"); @@ -301,7 +303,9 @@ pub async fn run_library_seed_ingestion( let store = store.clone(); let run_id = run_id.clone(); let msg = msg.clone(); - move || store.finish_ingestion_run(&run_id, "failed", &serde_json::json!({}), Some(&msg)) + move || { + store.finish_ingestion_run(&run_id, "failed", &serde_json::json!({}), Some(&msg)) + } }) .await??; anyhow::bail!("{msg}"); @@ -310,8 +314,7 @@ pub async fn run_library_seed_ingestion( // Rebuild search index { let store = store.clone(); - tokio::task::spawn_blocking(move || store.rebuild_corpus_search_index()) - .await??; + tokio::task::spawn_blocking(move || store.rebuild_corpus_search_index()).await??; } // Finish run @@ -355,7 +358,7 @@ struct DeclarationRecord { } async fn flush_declarations(store: &AppStore, batch: &mut Vec) -> Result<()> { - let items: Vec = batch.drain(..).collect(); + let items: Vec = std::mem::take(batch); let store = store.clone(); tokio::task::spawn_blocking(move || { let conn = store.connect_for_bulk()?; diff --git a/crates/openproof-corpus/src/lib.rs b/crates/openproof-corpus/src/lib.rs index afc2f57..2acc7c1 100644 --- a/crates/openproof-corpus/src/lib.rs +++ b/crates/openproof-corpus/src/lib.rs @@ -10,8 +10,7 @@ pub use search::*; use openproof_cloud::CloudCorpusClient; use openproof_protocol::{ - CloudCorpusAuthContext, CloudCorpusSearchHit, IngestLibrarySeedResult, - ShareMode, + CloudCorpusAuthContext, CloudCorpusSearchHit, IngestLibrarySeedResult, ShareMode, }; use openproof_store::AppStore; use std::path::PathBuf; diff --git a/crates/openproof-corpus/src/manifest.rs b/crates/openproof-corpus/src/manifest.rs index 2a3385e..fdad0cb 100644 --- a/crates/openproof-corpus/src/manifest.rs +++ b/crates/openproof-corpus/src/manifest.rs @@ -22,7 +22,7 @@ pub fn read_lake_manifest(lean_project_dir: &Path) -> Result<(LakeManifest, Stri let manifest_path = lean_project_dir.join("lake-manifest.json"); let raw = std::fs::read_to_string(&manifest_path) .with_context(|| format!("reading {}", manifest_path.display()))?; - let manifest: LakeManifest = - serde_json::from_str(&raw).with_context(|| format!("parsing {}", manifest_path.display()))?; + let manifest: LakeManifest = serde_json::from_str(&raw) + .with_context(|| format!("parsing {}", manifest_path.display()))?; Ok((manifest, raw)) } diff --git a/crates/openproof-corpus/src/packages.rs b/crates/openproof-corpus/src/packages.rs index 8e5c0dd..978090e 100644 --- a/crates/openproof-corpus/src/packages.rs +++ b/crates/openproof-corpus/src/packages.rs @@ -196,7 +196,10 @@ pub fn environment_fingerprint( manifest_text: &str, packages: &[PackageSeedInfo], ) -> String { - let mut parts = vec![lean_project_dir.trim().to_string(), manifest_text.trim().to_string()]; + let mut parts = vec![ + lean_project_dir.trim().to_string(), + manifest_text.trim().to_string(), + ]; let mut pkg_parts: Vec = packages .iter() .flat_map(|pkg| { diff --git a/crates/openproof-corpus/src/search.rs b/crates/openproof-corpus/src/search.rs index 2d22505..6976f2a 100644 --- a/crates/openproof-corpus/src/search.rs +++ b/crates/openproof-corpus/src/search.rs @@ -25,8 +25,7 @@ pub async fn search_shared_corpus( return Ok(Vec::new()); } - let mut scopes: Vec<(ShareMode, Option<&CloudCorpusAuthContext>)> = - vec![(share_mode, auth)]; + let mut scopes: Vec<(ShareMode, Option<&CloudCorpusAuthContext>)> = vec![(share_mode, auth)]; if share_mode == ShareMode::Private && include_community_overlay { scopes.push((ShareMode::Community, auth)); } @@ -145,12 +144,12 @@ pub async fn drain_sync_queue( let jobs = { let store = store.clone(); - tokio::task::spawn_blocking(move || store.list_sync_jobs_full(200)) - .await?? + tokio::task::spawn_blocking(move || store.list_sync_jobs_full(200)).await?? }; // Sync failed attempts first (independent of verified items) - let failure_jobs: Vec<_> = jobs.iter() + let failure_jobs: Vec<_> = jobs + .iter() .filter(|j| j.status == "pending" && j.queue_type == "attempt.failure") .cloned() .collect(); @@ -164,11 +163,11 @@ pub async fn drain_sync_queue( } let store = store.clone(); let jid = job.id.clone(); - let _ = tokio::task::spawn_blocking(move || store.mark_sync_job_status(&jid, "sent")) - .await; + let _ = tokio::task::spawn_blocking(move || store.mark_sync_job_status(&jid, "sent")).await; } // Sync corpus edges - let edge_jobs: Vec<_> = jobs.iter() + let edge_jobs: Vec<_> = jobs + .iter() .filter(|j| j.status == "pending" && j.queue_type == "corpus.edges") .cloned() .collect(); @@ -178,8 +177,7 @@ pub async fn drain_sync_queue( } let store = store.clone(); let jid = job.id.clone(); - let _ = tokio::task::spawn_blocking(move || store.mark_sync_job_status(&jid, "sent")) - .await; + let _ = tokio::task::spawn_blocking(move || store.mark_sync_job_status(&jid, "sent")).await; } let pending_jobs: Vec<_> = jobs @@ -228,10 +226,8 @@ pub async fn drain_sync_queue( let store = store.clone(); let keys = identity_keys.clone(); let vis = visibility_scope.to_string(); - tokio::task::spawn_blocking(move || { - store.list_verified_upload_candidates(256, &keys, &vis) - }) - .await?? + tokio::task::spawn_blocking(move || store.list_verified_upload_candidates(256, &keys, &vis)) + .await?? }; if candidates.is_empty() { @@ -239,8 +235,8 @@ pub async fn drain_sync_queue( for job in &pending_jobs { let store = store.clone(); let jid = job.id.clone(); - let _ = tokio::task::spawn_blocking(move || store.mark_sync_job_status(&jid, "sent")) - .await; + let _ = + tokio::task::spawn_blocking(move || store.mark_sync_job_status(&jid, "sent")).await; } return Ok(DrainSyncResult { sent: 0, @@ -281,10 +277,9 @@ pub async fn drain_sync_queue( for job in &pending_jobs { let store = store.clone(); let jid = job.id.clone(); - let _ = tokio::task::spawn_blocking(move || { - store.mark_sync_job_status(&jid, "sent") - }) - .await; + let _ = + tokio::task::spawn_blocking(move || store.mark_sync_job_status(&jid, "sent")) + .await; } DrainSyncResult { sent: candidates.len(), @@ -296,10 +291,9 @@ pub async fn drain_sync_queue( for job in &pending_jobs { let store = store.clone(); let jid = job.id.clone(); - let _ = tokio::task::spawn_blocking(move || { - store.mark_sync_job_status(&jid, "failed") - }) - .await; + let _ = + tokio::task::spawn_blocking(move || store.mark_sync_job_status(&jid, "failed")) + .await; } DrainSyncResult { sent: 0, diff --git a/crates/openproof-dashboard/src/lib.rs b/crates/openproof-dashboard/src/lib.rs index 89eeca7..10f503a 100644 --- a/crates/openproof-dashboard/src/lib.rs +++ b/crates/openproof-dashboard/src/lib.rs @@ -265,11 +265,17 @@ async fn workspace_files( for (path, _size) in entries { if path.ends_with(".lean") && !path.contains("history/") { let content = std::fs::read_to_string(ws_dir.join(&path)).unwrap_or_default(); - if !first { result.push(','); } + if !first { + result.push(','); + } first = false; // Manual JSON to avoid serde_json dependency - let escaped = content.replace('\\', "\\\\").replace('"', "\\\"") - .replace('\n', "\\n").replace('\r', "\\r").replace('\t', "\\t"); + let escaped = content + .replace('\\', "\\\\") + .replace('"', "\\\"") + .replace('\n', "\\n") + .replace('\r', "\\r") + .replace('\t', "\\t"); result.push_str(&format!( "{{\"path\":\"{path}\",\"content\":\"{escaped}\"}}" )); @@ -325,7 +331,8 @@ fn generate_tex(session: &SessionSnapshot) -> String { doc.push_str("\\date{\\today}\n\n"); doc.push_str("\\begin{document}\n\\maketitle\n\n"); // Strip [language=Lean] etc. -- listings doesn't know Lean. - let sanitized = proof.paper_tex + let sanitized = proof + .paper_tex .replace("[language=Lean]", "") .replace("[language=lean]", "") .replace("[language=lean4]", "") @@ -346,7 +353,7 @@ fn generate_tex(session: &SessionSnapshot) -> String { doc.push_str("\\newtheorem{theorem}{Theorem}\n"); doc.push_str("\\newtheorem{lemma}[theorem]{Lemma}\n"); doc.push_str("\\newtheorem{proposition}[theorem]{Proposition}\n"); - doc.push_str("\n"); + doc.push('\n'); doc.push_str(&format!("\\title{{{}}}\n", tex_escape(title))); doc.push_str("\\author{OpenProof}\n"); doc.push_str("\\date{\\today}\n"); @@ -381,9 +388,15 @@ fn generate_tex(session: &SessionSnapshot) -> String { _ => "proposition", }; let status_marker = match node.status { - openproof_protocol::ProofNodeStatus::Verified => " \\textnormal{[\\textcolor{green!70!black}{verified}]}", - openproof_protocol::ProofNodeStatus::Failed => " \\textnormal{[\\textcolor{red}{failed}]}", - openproof_protocol::ProofNodeStatus::Proving => " \\textnormal{[\\textcolor{orange}{proving}]}", + openproof_protocol::ProofNodeStatus::Verified => { + " \\textnormal{[\\textcolor{green!70!black}{verified}]}" + } + openproof_protocol::ProofNodeStatus::Failed => { + " \\textnormal{[\\textcolor{red}{failed}]}" + } + openproof_protocol::ProofNodeStatus::Proving => { + " \\textnormal{[\\textcolor{orange}{proving}]}" + } _ => "", }; doc.push_str(&format!( @@ -392,7 +405,7 @@ fn generate_tex(session: &SessionSnapshot) -> String { )); if !node.statement.is_empty() { doc.push_str(&tex_escape(&node.statement)); - doc.push_str("\n"); + doc.push('\n'); } doc.push_str(&format!("\\end{{{env}}}\n\n")); diff --git a/crates/openproof-lean/src/corpus_module.rs b/crates/openproof-lean/src/corpus_module.rs index c795774..4d87adf 100644 --- a/crates/openproof-lean/src/corpus_module.rs +++ b/crates/openproof-lean/src/corpus_module.rs @@ -62,7 +62,10 @@ pub fn build_corpus_module( } // Check first declaration keyword let first_word = clean.split_whitespace().next().unwrap_or(""); - if !matches!(first_word, "theorem" | "lemma" | "def" | "noncomputable" | "instance" | "abbrev" | "set_option") { + if !matches!( + first_word, + "theorem" | "lemma" | "def" | "noncomputable" | "instance" | "abbrev" | "set_option" + ) { continue; } // Split into individual declaration blocks and dedup each @@ -70,7 +73,9 @@ pub fn build_corpus_module( let mut new_blocks = Vec::new(); for block in &blocks { let block = block.trim(); - if block.is_empty() { continue; } + if block.is_empty() { + continue; + } if let Some(name) = extract_decl_name(block) { if seen_decl_names.contains(name) { continue; @@ -104,15 +109,11 @@ pub fn build_corpus_module( } // Write new Corpus.lean - std::fs::create_dir_all(corpus_path.parent().unwrap()) - .context("creating OpenProof dir")?; - std::fs::write(&corpus_path, &content) - .context("writing OpenProof/Corpus.lean")?; + std::fs::create_dir_all(corpus_path.parent().unwrap()).context("creating OpenProof dir")?; + std::fs::write(&corpus_path, &content).context("writing OpenProof/Corpus.lean")?; // Compile with lake build - eprintln!( - "[corpus-module] Building OpenProof.Corpus ({decl_count} declarations)..." - ); + eprintln!("[corpus-module] Building OpenProof.Corpus ({decl_count} declarations)..."); let output = std::process::Command::new("lake") .arg("build") .arg("OpenProof.Corpus") @@ -146,7 +147,9 @@ fn extract_decl_name(block: &str) -> Option<&str> { ]; for prefix in &prefixes { if let Some(rest) = first_line.trim().strip_prefix(prefix) { - return rest.split(|c: char| !c.is_alphanumeric() && c != '_').next(); + return rest + .split(|c: char| !c.is_alphanumeric() && c != '_') + .next(); } } None diff --git a/crates/openproof-lean/src/goals.rs b/crates/openproof-lean/src/goals.rs index e9e1c45..5b7e2a0 100644 --- a/crates/openproof-lean/src/goals.rs +++ b/crates/openproof-lean/src/goals.rs @@ -32,8 +32,10 @@ pub fn extract_sorry_goals(project_dir: &Path, content: &str) -> Result Result Result> { // Replace the first `sorry` with the search tactic let modified = if let Some(pos) = content.find("sorry") { - format!("{}{}{}", + format!( + "{}{}{}", &content[..pos], tactic, - &content[pos + "sorry".len()..]) + &content[pos + "sorry".len()..] + ) } else { format!("{content}\n#check {tactic}") }; @@ -96,7 +102,10 @@ pub fn run_tactic_suggestions( let trimmed = line.trim(); if let Some(rest) = trimmed.strip_prefix("Try this:") { suggestions.push(rest.trim().to_string()); - } else if trimmed.starts_with("[exact]") || trimmed.starts_with("[apply]") || trimmed.starts_with("[rw]") { + } else if trimmed.starts_with("[exact]") + || trimmed.starts_with("[apply]") + || trimmed.starts_with("[rw]") + { if let Some(pos) = trimmed.find(']') { suggestions.push(trimmed[pos + 1..].trim().to_string()); } @@ -131,15 +140,20 @@ pub fn extract_grounding_from_lean_output(stderr: &str, stdout: &str) -> Vec 10 && trimmed.len() < 500 { facts.push(format!("LEAN REPORTS: {trimmed}")); diff --git a/crates/openproof-lean/src/lib.rs b/crates/openproof-lean/src/lib.rs index 712dd8b..60a5193 100644 --- a/crates/openproof-lean/src/lib.rs +++ b/crates/openproof-lean/src/lib.rs @@ -6,8 +6,8 @@ pub mod goals; pub mod lsp_mcp; pub mod pantograph; pub mod parse; -pub mod proof_tree; pub mod patch; +pub mod proof_tree; pub mod render; pub mod tools; pub mod verify; diff --git a/crates/openproof-lean/src/lsp_mcp.rs b/crates/openproof-lean/src/lsp_mcp.rs index 3e0aa6d..ff4a2d9 100644 --- a/crates/openproof-lean/src/lsp_mcp.rs +++ b/crates/openproof-lean/src/lsp_mcp.rs @@ -45,7 +45,9 @@ impl LeanLspMcp { .env("LEAN_PROJECT_PATH", project_dir) .spawn() }) - .context("Failed to spawn lean-lsp-mcp. Install: uv tool install lean-lsp-mcp --python 3.12")?; + .context( + "Failed to spawn lean-lsp-mcp. Install: uv tool install lean-lsp-mcp --python 3.12", + )?; let stdin = child.stdin.take().context("No stdin on child")?; let stdout = child.stdout.take().context("No stdout on child")?; @@ -164,8 +166,7 @@ impl LeanLspMcp { let result = self.call_tool("lean_diagnostic_messages", args)?; let text = extract_text_content(&result)?; - serde_json::from_str(&text) - .context("Failed to parse DiagnosticsResult") + serde_json::from_str(&text).context("Failed to parse DiagnosticsResult") } /// Get hover info (type signature, documentation) at a position. @@ -291,7 +292,11 @@ impl Drop for LeanLspMcp { /// MCP returns `{"content": [{"type": "text", "text": "..."}], "isError": false}`. fn extract_text_content(result: &Value) -> Result { // Check for error - if result.get("isError").and_then(|v| v.as_bool()).unwrap_or(false) { + if result + .get("isError") + .and_then(|v| v.as_bool()) + .unwrap_or(false) + { let text = result .get("content") .and_then(|c| c.as_array()) diff --git a/crates/openproof-lean/src/pantograph.rs b/crates/openproof-lean/src/pantograph.rs index a5b7ac0..6dce59f 100644 --- a/crates/openproof-lean/src/pantograph.rs +++ b/crates/openproof-lean/src/pantograph.rs @@ -45,8 +45,7 @@ impl Pantograph { let repl_path = Self::find_repl(project_dir)?; // Get LEAN_PATH from the project - let lean_path = crate::tools::resolve_lean_path(project_dir) - .unwrap_or_default(); + let lean_path = crate::tools::resolve_lean_path(project_dir).unwrap_or_default(); // Pass "Mathlib" as argument so Pantograph preloads the environment. // This takes ~18s but subsequent operations are milliseconds. @@ -68,7 +67,10 @@ impl Pantograph { let mut ready_line = String::new(); reader.read_line(&mut ready_line)?; if !ready_line.trim().starts_with("ready") { - anyhow::bail!("Pantograph did not send ready signal: {}", ready_line.trim()); + anyhow::bail!( + "Pantograph did not send ready signal: {}", + ready_line.trim() + ); } Ok(Self { @@ -98,7 +100,9 @@ impl Pantograph { } } - anyhow::bail!("Pantograph REPL not found. Build it: cd vendor/Pantograph && lake build repl") + anyhow::bail!( + "Pantograph REPL not found. Build it: cd vendor/Pantograph && lake build repl" + ) } /// Send a command and read the JSON response. @@ -112,7 +116,7 @@ impl Pantograph { let mut response_line = String::new(); self.reader.read_line(&mut response_line)?; - serde_json::from_str(&response_line.trim()) + serde_json::from_str(response_line.trim()) .with_context(|| format!("parsing Pantograph response: {}", response_line.trim())) } @@ -124,12 +128,15 @@ impl Pantograph { /// Verify a Lean file by processing its content. /// Returns diagnostics and whether it compiled successfully. pub fn verify_content(&mut self, content: &str) -> Result { - let response = self.send_command("frontend.process", json!({ - "file": content, - "readHeader": true, - "inheritEnv": false, - "newConstants": true, - }))?; + let response = self.send_command( + "frontend.process", + json!({ + "file": content, + "readHeader": true, + "inheritEnv": false, + "newConstants": true, + }), + )?; let mut messages = Vec::new(); let mut has_error = false; @@ -178,9 +185,12 @@ impl Pantograph { /// Start a proof goal from a type expression. /// Returns a state ID that can be used with `try_tactic`. pub fn start_goal(&mut self, expr: &str) -> Result> { - let response = self.send_command("goal.start", json!({ - "expr": expr, - }))?; + let response = self.send_command( + "goal.start", + json!({ + "expr": expr, + }), + )?; if let Some(id) = response.get("stateId").and_then(|v| v.as_u64()) { Ok(Some(id)) @@ -191,12 +201,20 @@ impl Pantograph { /// Try a tactic on a goal state. Returns whether it succeeded /// and any remaining goals. - pub fn try_tactic(&mut self, state_id: u64, goal_id: u64, tactic: &str) -> Result { - let response = self.send_command("goal.tactic", json!({ - "stateId": state_id, - "goalId": goal_id, - "tactic": tactic, - }))?; + pub fn try_tactic( + &mut self, + state_id: u64, + goal_id: u64, + tactic: &str, + ) -> Result { + let response = self.send_command( + "goal.tactic", + json!({ + "stateId": state_id, + "goalId": goal_id, + "tactic": tactic, + }), + )?; if let Some(err) = response.get("parseError").and_then(|v| v.as_str()) { return Ok(TacticTestResult { @@ -209,7 +227,8 @@ impl Pantograph { if let Some(errors) = response.get("tacticErrors").and_then(|v| v.as_array()) { if !errors.is_empty() { - let err_msgs: Vec = errors.iter() + let err_msgs: Vec = errors + .iter() .filter_map(|e| e.as_str().map(String::from)) .collect(); return Ok(TacticTestResult { @@ -225,7 +244,8 @@ impl Pantograph { .get("nextStateId") .or_else(|| response.get("stateId")) .and_then(|v| v.as_u64()); - let goals: Vec = response.get("goals") + let goals: Vec = response + .get("goals") .and_then(|v| v.as_array()) .map(|arr| { arr.iter() @@ -258,12 +278,19 @@ impl Pantograph { /// Inspect an environment symbol. pub fn inspect(&mut self, name: &str) -> Result> { - let response = self.send_command("env.inspect", json!({ - "name": name, - "value": false, - }))?; - - if let Some(ty) = response.get("type").and_then(|v| v.get("pp")).and_then(|v| v.as_str()) { + let response = self.send_command( + "env.inspect", + json!({ + "name": name, + "value": false, + }), + )?; + + if let Some(ty) = response + .get("type") + .and_then(|v| v.get("pp")) + .and_then(|v| v.as_str()) + { Ok(Some(ty.to_string())) } else { Ok(None) diff --git a/crates/openproof-lean/src/parse.rs b/crates/openproof-lean/src/parse.rs index 98b4749..88e9062 100644 --- a/crates/openproof-lean/src/parse.rs +++ b/crates/openproof-lean/src/parse.rs @@ -51,7 +51,8 @@ pub fn parse_lean_declarations(content: &str) -> Vec { let mut body_lines = vec![lines[i].to_string()]; let mut j = i + 1; - let mut _found_body = trimmed.contains(":=") || trimmed.contains(" by") || trimmed.contains(" where"); + let mut _found_body = + trimmed.contains(":=") || trimmed.contains(" by") || trimmed.contains(" where"); while j < lines.len() { let next = lines[j]; let next_trimmed = next.trim(); @@ -60,7 +61,8 @@ pub fn parse_lean_declarations(content: &str) -> Vec { && !next.starts_with(' ') && !next.starts_with('\t') && keywords.iter().any(|&kw| { - next_trimmed.starts_with(kw) && next_trimmed[kw.len()..].starts_with(|c: char| c.is_whitespace()) + next_trimmed.starts_with(kw) + && next_trimmed[kw.len()..].starts_with(|c: char| c.is_whitespace()) }) { break; @@ -76,7 +78,10 @@ pub fn parse_lean_declarations(content: &str) -> Vec { } body_lines.push(next.to_string()); - if next_trimmed.contains(":=") || next_trimmed.contains(" by") || next_trimmed.contains(" where") { + if next_trimmed.contains(":=") + || next_trimmed.contains(" by") + || next_trimmed.contains(" where") + { _found_body = true; } j += 1; @@ -113,10 +118,7 @@ pub fn parse_lean_declarations(content: &str) -> Vec { /// Convert parsed Lean declarations into ProofNode entries for the proof tree. /// The first theorem/lemma becomes the root; subsequent ones are children. -pub fn declarations_to_proof_nodes( - decls: &[LeanDeclaration], - session_id: &str, -) -> Vec { +pub fn declarations_to_proof_nodes(decls: &[LeanDeclaration], session_id: &str) -> Vec { let now = Utc::now().to_rfc3339(); let mut nodes = Vec::new(); let mut current_root_id: Option = None; @@ -146,7 +148,11 @@ pub fn declarations_to_proof_nodes( current_root_id = Some(id.clone()); } - let parent_id = if is_root { None } else { current_root_id.clone() }; + let parent_id = if is_root { + None + } else { + current_root_id.clone() + }; let depth = if is_root { 0 } else { 1 }; // Extract dependencies: which other declarations does this one reference? @@ -181,10 +187,18 @@ pub fn extract_dependencies(body: &str, all_names: &[&str], self_name: &str) -> if body.contains(name) { // Verify it's a word boundary (not a substring of a longer name) for (i, _) in body.match_indices(name) { - let before = if i > 0 { body.as_bytes().get(i - 1).copied() } else { Some(b' ') }; + let before = if i > 0 { + body.as_bytes().get(i - 1).copied() + } else { + Some(b' ') + }; let after = body.as_bytes().get(i + name.len()).copied(); - let is_word = before.map(|b| !b.is_ascii_alphanumeric() && b != b'_').unwrap_or(true) - && after.map(|b| !b.is_ascii_alphanumeric() && b != b'_').unwrap_or(true); + let is_word = before + .map(|b| !b.is_ascii_alphanumeric() && b != b'_') + .unwrap_or(true) + && after + .map(|b| !b.is_ascii_alphanumeric() && b != b'_') + .unwrap_or(true); if is_word { deps.push(name.to_string()); break; diff --git a/crates/openproof-lean/src/render.rs b/crates/openproof-lean/src/render.rs index 899fd23..72c214a 100644 --- a/crates/openproof-lean/src/render.rs +++ b/crates/openproof-lean/src/render.rs @@ -39,12 +39,20 @@ pub fn render_node_scratch(session: &SessionSnapshot, node: &ProofNode) -> Strin if sibling_content.is_empty() { continue; } - lines.push(format!("-- openproof: {} :: {}", escape_comment(&sibling.label), escape_comment(&sibling.statement))); + lines.push(format!( + "-- openproof: {} :: {}", + escape_comment(&sibling.label), + escape_comment(&sibling.statement) + )); lines.push(sibling_content.to_string()); lines.push(String::new()); } - lines.push(format!("-- openproof: {} :: {}", escape_comment(&node.label), escape_comment(&node.statement))); + lines.push(format!( + "-- openproof: {} :: {}", + escape_comment(&node.label), + escape_comment(&node.statement) + )); lines.push(String::new()); lines.push(content.to_string()); lines.join("\n") diff --git a/crates/openproof-lean/src/tools.rs b/crates/openproof-lean/src/tools.rs index d593db1..d3ed129 100644 --- a/crates/openproof-lean/src/tools.rs +++ b/crates/openproof-lean/src/tools.rs @@ -72,8 +72,7 @@ fn tool_lean_verify(args: &Value, ctx: &ToolContext) -> Result { .and_then(Value::as_str) .unwrap_or("Scratch.lean"); let target = sanitize_path(ctx.workspace_dir, file)?; - let content = fs::read_to_string(&target) - .with_context(|| format!("reading {file}"))?; + let content = fs::read_to_string(&target).with_context(|| format!("reading {file}"))?; let full_content = build_compilation_unit(&content, ctx); @@ -97,7 +96,8 @@ fn build_compilation_unit(content: &str, ctx: &ToolContext) -> String { let mut body_start = 0; for line in content.lines() { let trimmed = line.trim(); - if trimmed.starts_with("import ") || trimmed.starts_with("open ") || trimmed.is_empty() { + if trimmed.starts_with("import ") || trimmed.starts_with("open ") || trimmed.is_empty() + { imports.push(line.to_string()); body_start += line.len() + 1; // +1 for newline } else { @@ -155,8 +155,8 @@ fn tool_lean_goals(args: &Value, ctx: &ToolContext) -> Result { if let Some(ref lsp) = ctx.lsp_mcp { if let Ok(mut mcp) = lsp.lock() { if mcp.is_alive() { - let content = fs::read_to_string(&target) - .with_context(|| format!("reading {file}"))?; + let content = + fs::read_to_string(&target).with_context(|| format!("reading {file}"))?; // Write to project dir so MCP can find it let project_scratch = ctx.project_dir.join("Scratch.lean"); let _ = fs::write(&project_scratch, &content); @@ -173,13 +173,13 @@ fn tool_lean_goals(args: &Value, ctx: &ToolContext) -> Result { for (line, _col) in &sorry_positions { match mcp.get_goals(&project_scratch, *line, None) { Ok(goal_state) => { - let goals = goal_state.goals_before.as_ref() + let goals = goal_state + .goals_before + .as_ref() .or(goal_state.goals.as_ref()) .map(|g| g.join("\n---\n")) .unwrap_or_else(|| "(no goals)".to_string()); - output_parts.push(format!( - "Line {line}:\n{goals}" - )); + output_parts.push(format!("Line {line}:\n{goals}")); } Err(e) => { output_parts.push(format!("Line {line}: error: {e}")); @@ -196,8 +196,7 @@ fn tool_lean_goals(args: &Value, ctx: &ToolContext) -> Result { } // Fallback: use regex-based goal extraction - let content = fs::read_to_string(&target) - .with_context(|| format!("reading {file}"))?; + let content = fs::read_to_string(&target).with_context(|| format!("reading {file}"))?; let full_content = if content.trim_start().starts_with("import ") { content @@ -258,10 +257,11 @@ fn tool_lean_screen_tactics(args: &Value, ctx: &ToolContext) -> Result>() .join("\n"); @@ -289,8 +289,13 @@ fn tool_lean_screen_tactics(args: &Value, ctx: &ToolContext) -> Result Result Result Result Vec<(usize, usize)> { while let Some(pos) = line[start..].find("sorry") { let abs_pos = start + pos; // Check it's a word boundary (not part of a larger identifier) - let before_ok = abs_pos == 0 - || !line.as_bytes()[abs_pos - 1].is_ascii_alphanumeric(); + let before_ok = abs_pos == 0 || !line.as_bytes()[abs_pos - 1].is_ascii_alphanumeric(); let after_pos = abs_pos + 5; - let after_ok = after_pos >= line.len() - || !line.as_bytes()[after_pos].is_ascii_alphanumeric(); + let after_ok = + after_pos >= line.len() || !line.as_bytes()[after_pos].is_ascii_alphanumeric(); if before_ok && after_ok { positions.push((i + 1, abs_pos + 1)); // 1-indexed } @@ -459,8 +460,7 @@ fn tool_lean_search_tactic(args: &Value, ctx: &ToolContext) -> Result Result { .and_then(Value::as_str) .context("missing 'path' argument")?; let target = sanitize_path(ctx.workspace_dir, path)?; - let content = fs::read_to_string(&target) - .with_context(|| format!("reading {path}"))?; + let content = fs::read_to_string(&target).with_context(|| format!("reading {path}"))?; // Add line numbers. let numbered: String = content .lines() @@ -543,8 +542,7 @@ fn tool_file_write(args: &Value, ctx: &ToolContext) -> Result { if let Some(parent) = target.parent() { fs::create_dir_all(parent)?; } - fs::write(&target, content) - .with_context(|| format!("writing {path}"))?; + fs::write(&target, content).with_context(|| format!("writing {path}"))?; let size = content.len(); Ok(ToolOutput { success: true, @@ -562,8 +560,8 @@ fn tool_file_patch(args: &Value, ctx: &ToolContext) -> Result { .and_then(Value::as_str) .context("missing 'patch' argument")?; let target = sanitize_path(ctx.workspace_dir, path)?; - let original = fs::read_to_string(&target) - .with_context(|| format!("reading {path} for patching"))?; + let original = + fs::read_to_string(&target).with_context(|| format!("reading {path} for patching"))?; match crate::patch::apply_patch(&original, patch_text) { Some(result) => { @@ -577,7 +575,8 @@ fn tool_file_patch(args: &Value, ctx: &ToolContext) -> Result { // Extract diff lines from the patch text for display for line in patch_text.lines() { let trimmed = line.trim(); - if trimmed.starts_with('+') || trimmed.starts_with('-') || trimmed.starts_with("@@") { + if trimmed.starts_with('+') || trimmed.starts_with('-') || trimmed.starts_with("@@") + { output.push('\n'); output.push_str(trimmed); } @@ -631,10 +630,7 @@ fn sanitize_path(workspace_dir: &Path, relative: &str) -> Result { } fn write_temp_file(content: &str) -> Result { - let dir = std::env::temp_dir().join(format!( - "openproof-lean-{}", - std::process::id() - )); + let dir = std::env::temp_dir().join(format!("openproof-lean-{}", std::process::id())); fs::create_dir_all(&dir)?; let path = dir.join("Scratch.lean"); fs::write(&path, content)?; @@ -682,7 +678,11 @@ pub fn resolve_lean_path(project_dir: &Path) -> Option { .ok() .and_then(|out| { let path = String::from_utf8_lossy(&out.stdout).trim().to_string(); - if path.is_empty() { None } else { Some(path) } + if path.is_empty() { + None + } else { + Some(path) + } }) }) .clone() @@ -729,17 +729,27 @@ fn wait_with_timeout( loop { match child.try_wait()? { Some(status) => { - let stdout = child.stdout.map(|mut s| { - let mut buf = Vec::new(); - std::io::Read::read_to_end(&mut s, &mut buf).ok(); - buf - }).unwrap_or_default(); - let stderr = child.stderr.map(|mut s| { - let mut buf = Vec::new(); - std::io::Read::read_to_end(&mut s, &mut buf).ok(); - buf - }).unwrap_or_default(); - return Ok(std::process::Output { status, stdout, stderr }); + let stdout = child + .stdout + .map(|mut s| { + let mut buf = Vec::new(); + std::io::Read::read_to_end(&mut s, &mut buf).ok(); + buf + }) + .unwrap_or_default(); + let stderr = child + .stderr + .map(|mut s| { + let mut buf = Vec::new(); + std::io::Read::read_to_end(&mut s, &mut buf).ok(); + buf + }) + .unwrap_or_default(); + return Ok(std::process::Output { + status, + stdout, + stderr, + }); } None => { if start.elapsed() > timeout { @@ -842,4 +852,3 @@ fn tool_shell_run(args: &Value, ctx: &ToolContext) -> Result { content: truncate_output(&combined), }) } - diff --git a/crates/openproof-lean/src/verify.rs b/crates/openproof-lean/src/verify.rs index 10c2642..3301c69 100644 --- a/crates/openproof-lean/src/verify.rs +++ b/crates/openproof-lean/src/verify.rs @@ -209,7 +209,8 @@ pub(crate) fn verify_scratch( } pub(crate) fn write_temp_scratch(rendered_scratch: &str) -> Result { - let dir = std::env::temp_dir().join(format!("openproof-lean-{}", Utc::now().timestamp_millis())); + let dir = + std::env::temp_dir().join(format!("openproof-lean-{}", Utc::now().timestamp_millis())); fs::create_dir_all(&dir).with_context(|| format!("creating {}", dir.display()))?; let scratch_path = dir.join("Scratch.lean"); fs::write(&scratch_path, rendered_scratch) diff --git a/crates/openproof-model/src/lib.rs b/crates/openproof-model/src/lib.rs index dda4188..3c050a0 100644 --- a/crates/openproof-model/src/lib.rs +++ b/crates/openproof-model/src/lib.rs @@ -202,7 +202,11 @@ pub enum TurnMessage { /// A regular chat message (user, assistant, system/developer). Chat { role: String, content: String }, /// A function call the model made (must be included before the result). - FunctionCall { call_id: String, name: String, arguments: String }, + FunctionCall { + call_id: String, + name: String, + arguments: String, + }, /// A tool result returned after executing a tool call. ToolResult { call_id: String, output: String }, } @@ -329,7 +333,11 @@ fn serialize_turn_message(message: &TurnMessage) -> Value { }) } } - TurnMessage::FunctionCall { call_id, name, arguments } => { + TurnMessage::FunctionCall { + call_id, + name, + arguments, + } => { json!({ "type": "function_call", "call_id": call_id, @@ -451,7 +459,11 @@ pub enum StreamEvent { /// Streaming arguments delta for an in-progress tool call. ToolCallArgsDelta { call_id: String, delta: String }, /// A tool call is complete with its full arguments. - ToolCallDone { call_id: String, name: String, arguments: String }, + ToolCallDone { + call_id: String, + name: String, + arguments: String, + }, } async fn read_event_stream_with_callback( @@ -508,11 +520,17 @@ pub async fn run_codex_turn_with_events( .context("Missing ChatGPT tokens in synced auth state.")?; response = client .post(format!("{OPENAI_CODEX_BASE_URL}/responses")) - .header("authorization", format!("Bearer {}", retry_tokens.access_token)) + .header( + "authorization", + format!("Bearer {}", retry_tokens.access_token), + ) .header("content-type", "application/json") .header("accept", "text/event-stream") .header("originator", DEFAULT_ORIGINATOR) - .header("chatgpt-account-id", retry_tokens.account_id.clone().unwrap_or_default()) + .header( + "chatgpt-account-id", + retry_tokens.account_id.clone().unwrap_or_default(), + ) .header("session_id", request.session_id) .json(&payload) .send() @@ -564,9 +582,11 @@ async fn read_event_stream_with_events( } // Text output delta - if let Some(delta) = event.get("delta").and_then(Value::as_str).filter(|_| { - event_type == "response.output_text.delta" - }) { + if let Some(delta) = event + .get("delta") + .and_then(Value::as_str) + .filter(|_| event_type == "response.output_text.delta") + { full_text.push_str(delta); on_event(StreamEvent::TextDelta(delta.to_string())); } @@ -576,10 +596,24 @@ async fn read_event_stream_with_events( if let Some(item) = event.get("item") { let item_type = item.get("type").and_then(Value::as_str).unwrap_or(""); if item_type == "function_call" { - let call_id = item.get("call_id").and_then(Value::as_str).unwrap_or("").to_string(); - let name = item.get("name").and_then(Value::as_str).unwrap_or("").to_string(); - let output_index = event.get("output_index").and_then(Value::as_u64).unwrap_or(0); - pending_calls.insert(output_index, (call_id.clone(), name.clone(), String::new())); + let call_id = item + .get("call_id") + .and_then(Value::as_str) + .unwrap_or("") + .to_string(); + let name = item + .get("name") + .and_then(Value::as_str) + .unwrap_or("") + .to_string(); + let output_index = event + .get("output_index") + .and_then(Value::as_u64) + .unwrap_or(0); + pending_calls.insert( + output_index, + (call_id.clone(), name.clone(), String::new()), + ); on_event(StreamEvent::ToolCallStart { call_id, name }); } } @@ -587,7 +621,10 @@ async fn read_event_stream_with_events( // Tool call: streaming argument deltas if event_type == "response.function_call_arguments.delta" { - let output_index = event.get("output_index").and_then(Value::as_u64).unwrap_or(0); + let output_index = event + .get("output_index") + .and_then(Value::as_u64) + .unwrap_or(0); let delta = event.get("delta").and_then(Value::as_str).unwrap_or(""); if let Some(entry) = pending_calls.get_mut(&output_index) { entry.2.push_str(delta); @@ -600,7 +637,10 @@ async fn read_event_stream_with_events( // Tool call: arguments complete if event_type == "response.function_call_arguments.done" { - let output_index = event.get("output_index").and_then(Value::as_u64).unwrap_or(0); + let output_index = event + .get("output_index") + .and_then(Value::as_u64) + .unwrap_or(0); if let Some((call_id, name, args)) = pending_calls.remove(&output_index) { let final_args = event .get("arguments") @@ -691,10 +731,26 @@ fn extract_tool_calls(value: &Value) -> Vec { for item in output { let item_type = item.get("type").and_then(Value::as_str).unwrap_or(""); if item_type == "function_call" { - let call_id = item.get("call_id").and_then(Value::as_str).unwrap_or("").to_string(); - let name = item.get("name").and_then(Value::as_str).unwrap_or("").to_string(); - let arguments = item.get("arguments").and_then(Value::as_str).unwrap_or("{}").to_string(); - calls.push(ToolCall { call_id, name, arguments }); + let call_id = item + .get("call_id") + .and_then(Value::as_str) + .unwrap_or("") + .to_string(); + let name = item + .get("name") + .and_then(Value::as_str) + .unwrap_or("") + .to_string(); + let arguments = item + .get("arguments") + .and_then(Value::as_str) + .unwrap_or("{}") + .to_string(); + calls.push(ToolCall { + call_id, + name, + arguments, + }); } } calls diff --git a/crates/openproof-search/src/config.rs b/crates/openproof-search/src/config.rs index 1d28785..c515a0c 100644 --- a/crates/openproof-search/src/config.rs +++ b/crates/openproof-search/src/config.rs @@ -52,9 +52,7 @@ pub enum SearchResult { file_content: String, }, /// No progress possible -- all candidates exhausted. - Exhausted { - expansions: usize, - }, + Exhausted { expansions: usize }, /// Time limit hit. Timeout { best_tactics: Vec, diff --git a/crates/openproof-search/src/ollama.rs b/crates/openproof-search/src/ollama.rs index 0d2d87d..35bd961 100644 --- a/crates/openproof-search/src/ollama.rs +++ b/crates/openproof-search/src/ollama.rs @@ -41,6 +41,12 @@ pub struct OllamaProposer { top_p: f64, } +impl Default for OllamaProposer { + fn default() -> Self { + Self::new() + } +} + impl OllamaProposer { /// Create a new proposer with default settings. pub fn new() -> Self { @@ -185,8 +191,7 @@ pub fn make_model_propose_fn( } // Fill remaining slots with standard tactics - let mut seen: std::collections::HashSet = - candidates.iter().cloned().collect(); + let mut seen: std::collections::HashSet = candidates.iter().cloned().collect(); for t in &fallback_tactics { if candidates.len() >= k { break; @@ -219,23 +224,20 @@ mod tests { #[test] fn test_filter_tactic_banned_substrings() { assert_eq!(filter_tactic("rcases h with ?_ | ?_"), None); - assert_eq!(filter_tactic("rcases h with h1 | h2"), Some("rcases h with h1 | h2".to_string())); + assert_eq!( + filter_tactic("rcases h with h1 | h2"), + Some("rcases h with h1 | h2".to_string()) + ); } #[test] fn test_filter_tactic_multiline() { // Model might generate multi-line; take only first line - assert_eq!( - filter_tactic("ring\n -- done"), - Some("ring".to_string()) - ); + assert_eq!(filter_tactic("ring\n -- done"), Some("ring".to_string())); } #[test] fn test_filter_tactic_separator() { - assert_eq!( - filter_tactic("omega:::"), - Some("omega".to_string()) - ); + assert_eq!(filter_tactic("omega:::"), Some("omega".to_string())); } } diff --git a/crates/openproof-search/src/search.rs b/crates/openproof-search/src/search.rs index fab614b..84b90b5 100644 --- a/crates/openproof-search/src/search.rs +++ b/crates/openproof-search/src/search.rs @@ -36,10 +36,21 @@ struct SearchNode { } impl SearchNode { - fn new(goals: Vec, tactics: Vec, sorry_line: usize, length_penalty: f64) -> Self { + fn new( + goals: Vec, + tactics: Vec, + sorry_line: usize, + length_penalty: f64, + ) -> Self { let score = goals.len(); let priority = ((score as f64 + length_penalty * tactics.len() as f64) * 1000.0) as u64; - Self { priority, score, tactics, goals, sorry_line } + Self { + priority, + score, + tactics, + goals, + sorry_line, + } } } @@ -275,20 +286,31 @@ impl PantographNode { ) -> Self { let score = goal_descriptions.len(); let priority = ((score as f64 + length_penalty * tactics.len() as f64) * 1000.0) as u64; - Self { priority, score, state_id, tactics, goal_descriptions } + Self { + priority, + score, + state_id, + tactics, + goal_descriptions, + } } } impl PartialEq for PantographNode { - fn eq(&self, other: &Self) -> bool { self.priority == other.priority } + fn eq(&self, other: &Self) -> bool { + self.priority == other.priority + } } impl Eq for PantographNode {} impl PartialOrd for PantographNode { - fn partial_cmp(&self, other: &Self) -> Option { Some(self.cmp(other)) } + fn partial_cmp(&self, other: &Self) -> Option { + Some(self.cmp(other)) + } } impl Ord for PantographNode { fn cmp(&self, other: &Self) -> std::cmp::Ordering { - Reverse(self.priority).cmp(&Reverse(other.priority)) + Reverse(self.priority) + .cmp(&Reverse(other.priority)) .then_with(|| self.tactics.len().cmp(&other.tactics.len())) } } @@ -313,12 +335,18 @@ pub fn pantograph_best_first_search( // Start the proof goal let initial_state_id = { - let mut pg = pantograph.lock().map_err(|e| anyhow::anyhow!("lock: {e}"))?; + let mut pg = pantograph + .lock() + .map_err(|e| anyhow::anyhow!("lock: {e}"))?; if !pg.is_alive() { bail!("Pantograph process is not running"); } - pg.start_goal(type_expr)? - .ok_or_else(|| anyhow::anyhow!("goal.start failed for: {}", &type_expr[..type_expr.len().min(100)]))? + pg.start_goal(type_expr)?.ok_or_else(|| { + anyhow::anyhow!( + "goal.start failed for: {}", + &type_expr[..type_expr.len().min(100)] + ) + })? }; allocated_states.push(initial_state_id); @@ -364,7 +392,11 @@ pub fn pantograph_best_first_search( } // Focus on the first goal description for tactic proposal - let goal_text = node.goal_descriptions.first().map(|s| s.as_str()).unwrap_or(""); + let goal_text = node + .goal_descriptions + .first() + .map(|s| s.as_str()) + .unwrap_or(""); if goal_text.is_empty() { continue; } @@ -378,7 +410,9 @@ pub fn pantograph_best_first_search( // Test each candidate tactic via Pantograph (3ms each) for tactic in &candidates { let result = { - let mut pg = pantograph.lock().map_err(|e| anyhow::anyhow!("lock: {e}"))?; + let mut pg = pantograph + .lock() + .map_err(|e| anyhow::anyhow!("lock: {e}"))?; if !pg.is_alive() { cleanup_states(pantograph, &allocated_states); bail!("Pantograph died during search"); @@ -387,7 +421,7 @@ pub fn pantograph_best_first_search( }; expansions += 1; - if !result.error.is_none() || result.new_state_id.is_none() { + if result.error.is_some() || result.new_state_id.is_none() { continue; // tactic failed } diff --git a/crates/openproof-search/tests/minif2f_bench.rs b/crates/openproof-search/tests/minif2f_bench.rs index 1d64699..ba881dd 100644 --- a/crates/openproof-search/tests/minif2f_bench.rs +++ b/crates/openproof-search/tests/minif2f_bench.rs @@ -53,7 +53,9 @@ fn extract_type_expr(content: &str) -> Option { } if in_theorem { theorem_lines.push(line); - if trimmed.contains(":= by sorry") || trimmed.contains(":= by") && trimmed.contains("sorry") { + if trimmed.contains(":= by sorry") + || trimmed.contains(":= by") && trimmed.contains("sorry") + { break; } } @@ -74,7 +76,9 @@ fn extract_type_expr(content: &str) -> Option { // Skip the name (first word after "theorem") let rest = &theorem_block[idx..]; // The name ends at first space or newline or ( - let name_end = rest.find(|c: char| c.is_whitespace() || c == '(').unwrap_or(rest.len()); + let name_end = rest + .find(|c: char| c.is_whitespace() || c == '(') + .unwrap_or(rest.len()); rest[name_end..].trim() } else { return None; @@ -129,11 +133,31 @@ fn extract_type_expr(content: &str) -> Option { fn standard_tactics() -> Vec { vec![ - "simp", "omega", "ring", "norm_num", "linarith", "aesop", - "grind", "decide", "trivial", "exact?", "apply?", "simp_all", - "tauto", "contradiction", "norm_cast", "positivity", "gcongr", - "polyrith", "field_simp", "push_cast", "ring_nf", "nlinarith", - "norm_num [*]", "simp [*]", "grind?", + "simp", + "omega", + "ring", + "norm_num", + "linarith", + "aesop", + "grind", + "decide", + "trivial", + "exact?", + "apply?", + "simp_all", + "tauto", + "contradiction", + "norm_cast", + "positivity", + "gcongr", + "polyrith", + "field_simp", + "push_cast", + "ring_nf", + "nlinarith", + "norm_num [*]", + "simp [*]", + "grind?", ] .into_iter() .map(String::from) @@ -141,9 +165,7 @@ fn standard_tactics() -> Vec { } fn make_propose_fn(tactics: Vec) -> ProposeFn { - Box::new(move |_goal: &str, _ctx: &str, k: usize| { - Ok(tactics.iter().take(k).cloned().collect()) - }) + Box::new(move |_goal: &str, _ctx: &str, k: usize| Ok(tactics.iter().take(k).cloned().collect())) } #[test] @@ -254,17 +276,33 @@ fn minif2f_tactic_search_benchmark() { solved_problems.push((name.clone(), tactics.clone(), elapsed.as_secs_f64())); format!("SOLVED {:.2}s {:?}", elapsed.as_secs_f64(), tactics) } - Ok(Ok(SearchResult::Partial { remaining_goals, .. })) => { + Ok(Ok(SearchResult::Partial { + remaining_goals, .. + })) => { failed += 1; - format!("PARTIAL {:.2}s {} goals remain", elapsed.as_secs_f64(), remaining_goals) + format!( + "PARTIAL {:.2}s {} goals remain", + elapsed.as_secs_f64(), + remaining_goals + ) } Ok(Ok(SearchResult::Exhausted { expansions })) => { failed += 1; - format!("EXHAUST {:.2}s {} expansions", elapsed.as_secs_f64(), expansions) + format!( + "EXHAUST {:.2}s {} expansions", + elapsed.as_secs_f64(), + expansions + ) } - Ok(Ok(SearchResult::Timeout { remaining_goals, .. })) => { + Ok(Ok(SearchResult::Timeout { + remaining_goals, .. + })) => { failed += 1; - format!("TIMEOUT {:.2}s {} goals remain", elapsed.as_secs_f64(), remaining_goals) + format!( + "TIMEOUT {:.2}s {} goals remain", + elapsed.as_secs_f64(), + remaining_goals + ) } Ok(Err(e)) => { errored += 1; @@ -285,11 +323,18 @@ fn minif2f_tactic_search_benchmark() { println!("RESULTS"); println!("========================================"); println!("Total: {}", total); - println!("Solved: {} ({:.1}%)", solved, 100.0 * solved as f64 / total as f64); + println!( + "Solved: {} ({:.1}%)", + solved, + 100.0 * solved as f64 / total as f64 + ); println!("Failed: {}", failed); println!("Errors: {}", errored); println!("Wall time: {:.1}s", wall_time.as_secs_f64()); - println!("Avg time: {:.2}s/problem", total_time.as_secs_f64() / total as f64); + println!( + "Avg time: {:.2}s/problem", + total_time.as_secs_f64() / total as f64 + ); if !solved_problems.is_empty() { println!("\n--- Solved Problems ---"); @@ -298,5 +343,10 @@ fn minif2f_tactic_search_benchmark() { } } - println!("\npass@1 = {:.1}% ({}/{})", 100.0 * solved as f64 / total as f64, solved, total); + println!( + "\npass@1 = {:.1}% ({}/{})", + 100.0 * solved as f64 / total as f64, + solved, + total + ); } diff --git a/crates/openproof-search/tests/search_integration.rs b/crates/openproof-search/tests/search_integration.rs index 43dfe38..6d253f6 100644 --- a/crates/openproof-search/tests/search_integration.rs +++ b/crates/openproof-search/tests/search_integration.rs @@ -26,11 +26,31 @@ fn lean_project_dir() -> PathBuf { fn standard_tactics() -> Vec { vec![ - "simp", "omega", "ring", "norm_num", "linarith", "aesop", - "grind", "decide", "trivial", "exact?", "apply?", "simp_all", - "tauto", "contradiction", "norm_cast", "positivity", "gcongr", - "polyrith", "field_simp", "push_cast", "ring_nf", "nlinarith", - "norm_num [*]", "simp [*]", "grind?", + "simp", + "omega", + "ring", + "norm_num", + "linarith", + "aesop", + "grind", + "decide", + "trivial", + "exact?", + "apply?", + "simp_all", + "tauto", + "contradiction", + "norm_cast", + "positivity", + "gcongr", + "polyrith", + "field_simp", + "push_cast", + "ring_nf", + "nlinarith", + "norm_num [*]", + "simp [*]", + "grind?", ] .into_iter() .map(String::from) @@ -38,9 +58,7 @@ fn standard_tactics() -> Vec { } fn make_propose_fn(tactics: Vec) -> ProposeFn { - Box::new(move |_goal: &str, _ctx: &str, k: usize| { - Ok(tactics.iter().take(k).cloned().collect()) - }) + Box::new(move |_goal: &str, _ctx: &str, k: usize| Ok(tactics.iter().take(k).cloned().collect())) } /// Write a Lean file, spawn LSP, and warm it up by retrying get_diagnostics @@ -51,7 +69,10 @@ fn setup_lsp_test(content: &str) -> (Mutex, PathBuf, Vec<(usize, usi std::fs::write(&scratch_path, content).expect("write scratch file"); let sorrys = find_sorry_positions(content); - assert!(!sorrys.is_empty(), "Test content must have at least one sorry"); + assert!( + !sorrys.is_empty(), + "Test content must have at least one sorry" + ); // Spawn LSP and warm up with retries (first elaboration takes 30-90s) println!("Spawning lean-lsp-mcp and warming up (first load may take 60-90s)..."); @@ -61,8 +82,7 @@ fn setup_lsp_test(content: &str) -> (Mutex, PathBuf, Vec<(usize, usi let max_retries = 4; let mut lsp = None; for attempt in 1..=max_retries { - let client = LeanLspMcp::spawn(&project_dir) - .expect("Failed to spawn lean-lsp-mcp"); + let client = LeanLspMcp::spawn(&project_dir).expect("Failed to spawn lean-lsp-mcp"); let mut client = client; // Try a diagnostics call to trigger elaboration @@ -110,14 +130,27 @@ fn print_result(result: &SearchResult) { SearchResult::Solved { tactics, .. } => { println!(" SOLVED with {} tactics: {:?}", tactics.len(), tactics); } - SearchResult::Partial { tactics, remaining_goals, .. } => { - println!(" PARTIAL: {} goals remain, tactics: {:?}", remaining_goals, tactics); + SearchResult::Partial { + tactics, + remaining_goals, + .. + } => { + println!( + " PARTIAL: {} goals remain, tactics: {:?}", + remaining_goals, tactics + ); } SearchResult::Exhausted { expansions } => { println!(" EXHAUSTED after {} expansions", expansions); } - SearchResult::Timeout { best_tactics, remaining_goals } => { - println!(" TIMEOUT: {} goals remain, best: {:?}", remaining_goals, best_tactics); + SearchResult::Timeout { + best_tactics, + remaining_goals, + } => { + println!( + " TIMEOUT: {} goals remain, best: {:?}", + remaining_goals, best_tactics + ); } } } @@ -254,7 +287,10 @@ theorem e2e_test (n : Nat) : n + 0 = n := by let start = Instant::now(); let result = best_first_search(&lsp, &propose_fn, &scratch_path, line, "", &config) .expect("search failed"); - println!("[e2e] Search completed in {:.2}s", start.elapsed().as_secs_f64()); + println!( + "[e2e] Search completed in {:.2}s", + start.elapsed().as_secs_f64() + ); print_result(&result); let tactics = match &result { @@ -269,8 +305,8 @@ theorem e2e_test (n : Nat) : n + 0 = n := by ); println!("[e2e] Verifying filled proof:\n{}", content_filled); - let (ok, output) = run_lean_verify_raw(&project_dir, &content_filled) - .expect("lean verify filled"); + let (ok, output) = + run_lean_verify_raw(&project_dir, &content_filled).expect("lean verify filled"); if !output.is_empty() { println!("[e2e] Lean output: {}", &output[..output.len().min(500)]); } @@ -352,9 +388,16 @@ theorem test_penalty (n : Nat) : 0 + n = n := by print_result(&result); if let SearchResult::Solved { tactics, .. } = &result { - assert!(tactics.len() <= 2, "High penalty should produce short proof, got {} steps", tactics.len()); + assert!( + tactics.len() <= 2, + "High penalty should produce short proof, got {} steps", + tactics.len() + ); } - assert!(result.is_solved(), "Expected Solved even with high length penalty"); + assert!( + result.is_solved(), + "Expected Solved even with high length penalty" + ); } // ----------------------------------------------------------------------- @@ -380,8 +423,8 @@ fn pantograph_solves_simp_goal() { let goal = "forall (n : Nat), n + 0 = n"; println!("Goal: {goal}"); let start = Instant::now(); - let result = pantograph_best_first_search(&pg, &propose_fn, goal, "", &config) - .expect("search failed"); + let result = + pantograph_best_first_search(&pg, &propose_fn, goal, "", &config).expect("search failed"); println!("Completed in {:.3}s", start.elapsed().as_secs_f64()); print_result(&result); assert!(result.is_solved()); @@ -399,8 +442,8 @@ fn pantograph_solves_with_grind() { let goal = "forall (a b c : Nat), a = b -> b = c -> a = c"; println!("Goal (grind-only): {goal}"); let start = Instant::now(); - let result = pantograph_best_first_search(&pg, &propose_fn, goal, "", &config) - .expect("search failed"); + let result = + pantograph_best_first_search(&pg, &propose_fn, goal, "", &config).expect("search failed"); println!("Completed in {:.3}s", start.elapsed().as_secs_f64()); print_result(&result); assert!(result.is_solved(), "grind should solve transitivity"); @@ -417,7 +460,10 @@ fn pantograph_solves_multi_goals() { ("forall (n : Nat), 0 + n = n", "0+n=n"), ("forall (a b : Nat), a + b = b + a", "add_comm"), ("forall (n : Nat), n * 1 = n", "mul_one"), - ("forall (x : Int), (x + 1) * (x + 1) = x * x + 2 * x + 1", "ring_id"), + ( + "forall (x : Int), (x + 1) * (x + 1) = x * x + 2 * x + 1", + "ring_id", + ), ("forall (n : Nat), n < n + 1", "lt_succ"), ]; diff --git a/crates/openproof-store/src/corpus.rs b/crates/openproof-store/src/corpus.rs index 3eafdbf..443bc5a 100644 --- a/crates/openproof-store/src/corpus.rs +++ b/crates/openproof-store/src/corpus.rs @@ -74,7 +74,11 @@ fn classify_failure(result: &LeanVerificationSummary) -> String { "sorry-placeholder".to_string() } else if combined.contains("timeout") { "timeout".to_string() - } else if let Some(error) = result.error.as_ref().filter(|value| !value.trim().is_empty()) { + } else if let Some(error) = result + .error + .as_ref() + .filter(|value| !value.trim().is_empty()) + { error.trim().to_string() } else { "lean-error".to_string() @@ -87,7 +91,10 @@ pub(crate) fn summarize_lean_diagnostic(result: &LeanVerificationSummary) -> Str } else if !result.stdout.trim().is_empty() { result.stdout.trim() } else { - result.error.as_deref().unwrap_or("Lean verification failed.") + result + .error + .as_deref() + .unwrap_or("Lean verification failed.") }; primary.lines().take(12).collect::>().join("\n") } @@ -200,18 +207,24 @@ impl AppStore { if !seen_labels.insert(sibling.label.clone()) { continue; } - let clean = sibling.content.lines() + let clean = sibling + .content + .lines() .filter(|l| !l.trim().starts_with("import ") && !l.trim().starts_with("open ")) - .collect::>().join("\n"); + .collect::>() + .join("\n"); if !clean.trim().is_empty() { parts.push_str(clean.trim()); parts.push_str("\n\n"); } } // Add the active node - let clean_node = node.content.lines() + let clean_node = node + .content + .lines() .filter(|l| !l.trim().starts_with("import ") && !l.trim().starts_with("open ")) - .collect::>().join("\n"); + .collect::>() + .join("\n"); parts.push_str(clean_node.trim()); parts }; @@ -335,9 +348,12 @@ impl AppStore { if sibling.id == node.id || sibling.content.trim().is_empty() { continue; } - let sib_clean = sibling.content.lines() + let sib_clean = sibling + .content + .lines() .filter(|l| !l.trim().starts_with("import ") && !l.trim().starts_with("open ")) - .collect::>().join("\n"); + .collect::>() + .join("\n"); let sib_clean = sib_clean.trim(); if sib_clean.is_empty() { continue; @@ -409,18 +425,26 @@ impl AppStore { if !seen_labels.insert(sibling.label.clone()) { continue; } - let clean = sibling.content.lines() - .filter(|l| !l.trim().starts_with("import ") && !l.trim().starts_with("open ")) - .collect::>().join("\n"); + let clean = sibling + .content + .lines() + .filter(|l| { + !l.trim().starts_with("import ") && !l.trim().starts_with("open ") + }) + .collect::>() + .join("\n"); if !clean.trim().is_empty() { full_content.push_str(clean.trim()); full_content.push_str("\n\n"); } } // Add the active node - let clean_node = node.content.lines() + let clean_node = node + .content + .lines() .filter(|l| !l.trim().starts_with("import ") && !l.trim().starts_with("open ")) - .collect::>().join("\n"); + .collect::>() + .join("\n"); full_content.push_str(clean_node.trim()); let payload = serde_json::json!({ @@ -604,8 +628,16 @@ impl AppStore { let mut update_item = update_item; let mut insert_cluster = insert_cluster; - for (id, label, statement, decl_kind, is_theorem_like, content_hash, created_at, updated_at) in - items + for ( + id, + label, + statement, + decl_kind, + is_theorem_like, + content_hash, + created_at, + updated_at, + ) in items { let cluster_key = compute_corpus_cluster_key( &statement, @@ -674,7 +706,9 @@ impl AppStore { let conn = self.connect()?; // Extract keywords (3+ chars, skip common words) and search with AND logic. - let skip = ["the", "that", "this", "with", "from", "prove", "show", "for", "and", "not"]; + let skip = [ + "the", "that", "this", "with", "from", "prove", "show", "for", "and", "not", + ]; let keywords: Vec = query .split(|c: char| !c.is_alphanumeric() && c != '_') .filter(|w| w.len() >= 3 && !skip.contains(&w.to_lowercase().as_str())) @@ -686,7 +720,8 @@ impl AppStore { } // Build WHERE clause: search_text LIKE %kw1% AND search_text LIKE %kw2% ... - let conditions: Vec = keywords.iter() + let conditions: Vec = keywords + .iter() .map(|_| "search_text LIKE ?".to_string()) .collect(); let where_clause = conditions.join(" AND "); @@ -702,9 +737,10 @@ impl AppStore { .collect(); params.push(Box::new(limit as i64)); - let rows = stmt.query_map(rusqlite::params_from_iter(params.iter().map(|p| p.as_ref())), |row| { - Ok((row.get(0)?, row.get(1)?, row.get(2)?)) - })?; + let rows = stmt.query_map( + rusqlite::params_from_iter(params.iter().map(|p| p.as_ref())), + |row| Ok((row.get(0)?, row.get(1)?, row.get(2)?)), + )?; let mut items = Vec::new(); let mut seen_labels = std::collections::HashSet::new(); for row in rows { @@ -716,7 +752,11 @@ impl AppStore { // Graph expansion: find premises that the direct hits depend on. if !items.is_empty() { let direct_labels: Vec = items.iter().map(|i| i.0.clone()).collect(); - let placeholders = direct_labels.iter().map(|_| "?").collect::>().join(","); + let placeholders = direct_labels + .iter() + .map(|_| "?") + .collect::>() + .join(","); let edge_sql = format!( r#"SELECT DISTINCT v.label, v.statement, v.visibility FROM corpus_edges e @@ -734,13 +774,17 @@ impl AppStore { edge_params.push(Box::new(limit as i64)); if let Ok(edge_rows) = edge_stmt.query_map( rusqlite::params_from_iter(edge_params.iter().map(|p| p.as_ref())), - |row| Ok((row.get::<_, String>(0)?, row.get::<_, String>(1)?, row.get::<_, String>(2)?)), + |row| { + Ok(( + row.get::<_, String>(0)?, + row.get::<_, String>(1)?, + row.get::<_, String>(2)?, + )) + }, ) { - for row in edge_rows { - if let Ok(item) = row { - if seen_labels.insert(item.0.clone()) { - items.push(item); - } + for item in edge_rows.flatten() { + if seen_labels.insert(item.0.clone()) { + items.push(item); } } } @@ -761,14 +805,10 @@ impl AppStore { WHERE v.origin = 'user-verified' ORDER BY v.created_at ASC"#, )?; - let rows = stmt.query_map([], |row| { - Ok((row.get(0)?, row.get(1)?, row.get(2)?)) - })?; + let rows = stmt.query_map([], |row| Ok((row.get(0)?, row.get(1)?, row.get(2)?)))?; let mut items = Vec::new(); - for row in rows { - if let Ok(item) = row { - items.push(item); - } + for item in rows.flatten() { + items.push(item); } Ok(items) } @@ -783,7 +823,9 @@ impl AppStore { WHERE v.label = ? AND v.origin = 'user-verified' LIMIT 1"#, )?; - let result = stmt.query_row(rusqlite::params![label], |row| row.get(0)).ok(); + let result = stmt + .query_row(rusqlite::params![label], |row| row.get(0)) + .ok(); Ok(result) } } diff --git a/crates/openproof-store/src/corpus_seed.rs b/crates/openproof-store/src/corpus_seed.rs index 05926cb..631082f 100644 --- a/crates/openproof-store/src/corpus_seed.rs +++ b/crates/openproof-store/src/corpus_seed.rs @@ -87,10 +87,7 @@ pub(crate) fn extract_library_seed_items(source: &str) -> Vec { && index + 1 < lines.len() { let next = lines[index + 1].trim(); - if next.is_empty() - || parse_decl_header(next).is_some() - || next.starts_with("/--") - { + if next.is_empty() || parse_decl_header(next).is_some() || next.starts_with("/--") { break; } header.push(' '); @@ -203,8 +200,8 @@ impl AppStore { ) })?; let module_name = lean_module_name(relative); - let contents = fs::read_to_string(&file) - .with_context(|| format!("reading {}", file.display()))?; + let contents = + fs::read_to_string(&file).with_context(|| format!("reading {}", file.display()))?; for item in extract_library_seed_items(&contents) { let artifact_hash = stable_hash(&item.statement); let artifact_id = format!("seed_artifact_{artifact_hash}"); @@ -353,7 +350,14 @@ impl AppStore { SET status = ?, stats_json = ?, error = ?, updated_at = ?, completed_at = ? WHERE id = ? "#, - rusqlite::params![status, serde_json::to_string(stats)?, error, &now, &now, run_id], + rusqlite::params![ + status, + serde_json::to_string(stats)?, + error, + &now, + &now, + run_id + ], )?; Ok(()) } diff --git a/crates/openproof-store/src/corpus_sync.rs b/crates/openproof-store/src/corpus_sync.rs index 4bff42a..387de33 100644 --- a/crates/openproof-store/src/corpus_sync.rs +++ b/crates/openproof-store/src/corpus_sync.rs @@ -460,9 +460,7 @@ impl AppStore { /// Get items by domain tag. pub fn items_by_tag(&self, tag: &str, limit: usize) -> Result> { let conn = self.connect()?; - let mut stmt = conn.prepare( - "SELECT item_key FROM corpus_tags WHERE tag = ? LIMIT ?", - )?; + let mut stmt = conn.prepare("SELECT item_key FROM corpus_tags WHERE tag = ? LIMIT ?")?; let rows = stmt.query_map(rusqlite::params![tag, limit as i64], |row| row.get(0))?; let mut results = Vec::new(); for row in rows { @@ -475,12 +473,30 @@ impl AppStore { pub fn auto_tag_from_module(&self, item_key: &str, module_name: &str) -> Result<()> { let lower = module_name.to_lowercase(); let tags: Vec<&str> = [ - ("algebra", &["algebra", "group", "ring", "field", "module", "linear"][..]), - ("topology", &["topology", "topological", "metric", "continuous"]), - ("analysis", &["analysis", "measure", "integral", "derivative", "limit"]), - ("number_theory", &["number", "prime", "divisib", "factorial", "modular", "zmod"]), - ("combinatorics", &["combinat", "finset", "card", "pigeonhole", "ramsey"]), - ("geometry", &["geometry", "euclid", "triangle", "circle", "angle"]), + ( + "algebra", + &["algebra", "group", "ring", "field", "module", "linear"][..], + ), + ( + "topology", + &["topology", "topological", "metric", "continuous"], + ), + ( + "analysis", + &["analysis", "measure", "integral", "derivative", "limit"], + ), + ( + "number_theory", + &["number", "prime", "divisib", "factorial", "modular", "zmod"], + ), + ( + "combinatorics", + &["combinat", "finset", "card", "pigeonhole", "ramsey"], + ), + ( + "geometry", + &["geometry", "euclid", "triangle", "circle", "angle"], + ), ("logic", &["logic", "propositional", "decidab", "classical"]), ("order", &["order", "lattice", "partial", "total"]), ("category", &["category", "functor", "natural", "monad"]), diff --git a/crates/openproof-store/src/embeddings.rs b/crates/openproof-store/src/embeddings.rs index ac798d2..3e5d698 100644 --- a/crates/openproof-store/src/embeddings.rs +++ b/crates/openproof-store/src/embeddings.rs @@ -88,6 +88,7 @@ impl EmbeddingStore { } /// Upsert a verified corpus item into the vector store. + #[allow(clippy::too_many_arguments)] pub async fn upsert_item( &self, identity_key: &str, @@ -243,10 +244,7 @@ pub fn build_embedding_text( module_name: &str, artifact_content: &str, ) -> String { - let mut parts = vec![ - format!("{decl_kind}: {label}"), - statement.to_string(), - ]; + let mut parts = vec![format!("{decl_kind}: {label}"), statement.to_string()]; if !module_name.is_empty() { parts.push(format!("module: {module_name}")); } diff --git a/crates/openproof-store/src/extract.rs b/crates/openproof-store/src/extract.rs index 8fa09f9..eea8487 100644 --- a/crates/openproof-store/src/extract.rs +++ b/crates/openproof-store/src/extract.rs @@ -239,8 +239,14 @@ fn extract_string_array(value: &Value) -> Option> { } fn extract_pending_question(value: &Value) -> Option { - let raw = value.get("proof").and_then(|item| item.get("pendingQuestion"))?; - let prompt = raw.get("prompt").and_then(Value::as_str)?.trim().to_string(); + let raw = value + .get("proof") + .and_then(|item| item.get("pendingQuestion"))?; + let prompt = raw + .get("prompt") + .and_then(Value::as_str)? + .trim() + .to_string(); if prompt.is_empty() { return None; } @@ -303,7 +309,11 @@ fn extract_proof_nodes(value: &Value) -> Vec { nodes .iter() .filter_map(|node| { - let kind = match node.get("kind").and_then(Value::as_str).unwrap_or("theorem") { + let kind = match node + .get("kind") + .and_then(Value::as_str) + .unwrap_or("theorem") + { "lemma" => ProofNodeKind::Lemma, "theorem" => ProofNodeKind::Theorem, "artifact" => ProofNodeKind::Artifact, @@ -311,7 +321,11 @@ fn extract_proof_nodes(value: &Value) -> Vec { "conjecture" => ProofNodeKind::Conjecture, _ => return None, }; - let label = node.get("label").and_then(Value::as_str)?.trim().to_string(); + let label = node + .get("label") + .and_then(Value::as_str)? + .trim() + .to_string(); let statement = node .get("statement") .and_then(Value::as_str) @@ -363,12 +377,14 @@ fn extract_proof_nodes(value: &Value) -> Vec { .get("dependsOn") .or_else(|| node.get("depends_on")) .and_then(Value::as_array) - .map(|arr| arr.iter().filter_map(Value::as_str).map(str::to_string).collect()) + .map(|arr| { + arr.iter() + .filter_map(Value::as_str) + .map(str::to_string) + .collect() + }) .unwrap_or_default(), - depth: node - .get("depth") - .and_then(Value::as_u64) - .unwrap_or(0) as usize, + depth: node.get("depth").and_then(Value::as_u64).unwrap_or(0) as usize, updated_at: node .get("updatedAt") .and_then(Value::as_str) @@ -380,7 +396,9 @@ fn extract_proof_nodes(value: &Value) -> Vec { } pub(crate) fn extract_last_verification(value: &Value) -> Option { - let raw = value.get("runtime").and_then(|item| item.get("lastLeanCheck"))?; + let raw = value + .get("runtime") + .and_then(|item| item.get("lastLeanCheck"))?; Some(LeanVerificationSummary { ok: raw.get("ok").and_then(Value::as_bool).unwrap_or(false), code: raw diff --git a/crates/openproof-store/src/lib.rs b/crates/openproof-store/src/lib.rs index 9d5d91b..bf64a68 100644 --- a/crates/openproof-store/src/lib.rs +++ b/crates/openproof-store/src/lib.rs @@ -9,8 +9,8 @@ mod schema; mod sessions; mod store; +pub use corpus::{sanitize_identity_segment, stable_hash as corpus_hash}; pub use store::{AppStore, StorePaths}; -pub use corpus::{stable_hash as corpus_hash, sanitize_identity_segment}; #[cfg(test)] mod tests { diff --git a/crates/openproof-store/src/schema.rs b/crates/openproof-store/src/schema.rs index 1c04356..7084392 100644 --- a/crates/openproof-store/src/schema.rs +++ b/crates/openproof-store/src/schema.rs @@ -307,7 +307,7 @@ pub(crate) fn open_connection(db_path: &Path) -> Result { DROP TABLE corpus_edges; ALTER TABLE corpus_edges_new RENAME TO corpus_edges; CREATE INDEX IF NOT EXISTS idx_corpus_edges_from ON corpus_edges(from_item_key); - CREATE INDEX IF NOT EXISTS idx_corpus_edges_to ON corpus_edges(to_item_key);" + CREATE INDEX IF NOT EXISTS idx_corpus_edges_to ON corpus_edges(to_item_key);", ); } } diff --git a/crates/openproof-store/src/sessions.rs b/crates/openproof-store/src/sessions.rs index f64bfb4..555d5e9 100644 --- a/crates/openproof-store/src/sessions.rs +++ b/crates/openproof-store/src/sessions.rs @@ -117,8 +117,7 @@ impl AppStore { pub(crate) fn ensure_default_session(&self) -> Result<()> { let conn = self.connect()?; - let count: i64 = - conn.query_row("SELECT COUNT(*) FROM sessions", [], |row| row.get(0))?; + let count: i64 = conn.query_row("SELECT COUNT(*) FROM sessions", [], |row| row.get(0))?; if count > 0 { return Ok(()); } @@ -137,10 +136,10 @@ impl AppStore { } fn import_legacy_session_file(&self, path: &std::path::Path) -> Result { - let raw = fs::read_to_string(path) - .with_context(|| format!("reading {}", path.display()))?; - let value: Value = serde_json::from_str(&raw) - .with_context(|| format!("parsing {}", path.display()))?; + let raw = + fs::read_to_string(path).with_context(|| format!("reading {}", path.display()))?; + let value: Value = + serde_json::from_str(&raw).with_context(|| format!("parsing {}", path.display()))?; let Some(id) = value.get("id").and_then(Value::as_str).map(str::to_string) else { return Ok(false); }; @@ -217,7 +216,11 @@ impl AppStore { Ok(None) } - pub(crate) fn upsert_session(&self, conn: &Connection, session: &SessionSnapshot) -> Result<()> { + pub(crate) fn upsert_session( + &self, + conn: &Connection, + session: &SessionSnapshot, + ) -> Result<()> { let transcript_json = serde_json::to_string(&session.transcript)?; let cloud_json = serde_json::to_string(&session.cloud)?; let proof_json = serde_json::to_string(&session.proof)?; diff --git a/crates/openproof-store/src/store.rs b/crates/openproof-store/src/store.rs index 17a55fb..0e0d755 100644 --- a/crates/openproof-store/src/store.rs +++ b/crates/openproof-store/src/store.rs @@ -78,7 +78,12 @@ impl AppStore { /// Write the Scratch.lean file for a session. /// Archives the previous version to history/NNN_attempt.lean first. /// Write a patch diff alongside the attempt archive. - pub fn write_patch_diff(&self, session_id: &str, attempt_number: usize, diff: &str) -> Result<()> { + pub fn write_patch_diff( + &self, + session_id: &str, + attempt_number: usize, + diff: &str, + ) -> Result<()> { let dir = self.session_dir(session_id)?; let history_dir = dir.join("history"); let diff_path = history_dir.join(format!("{:03}_patch.diff", attempt_number)); @@ -97,11 +102,7 @@ impl AppStore { .map(|entries| { entries .filter_map(|e| e.ok()) - .filter(|e| { - e.file_name() - .to_string_lossy() - .ends_with("_attempt.lean") - }) + .filter(|e| e.file_name().to_string_lossy().ends_with("_attempt.lean")) .collect() }) .unwrap_or_default(); @@ -129,7 +130,11 @@ impl AppStore { /// Read the current Scratch.lean content for a session. pub fn read_scratch(&self, session_id: &str) -> Option { - let path = self.paths.sessions_dir.join(session_id).join("Scratch.lean"); + let path = self + .paths + .sessions_dir + .join(session_id) + .join("Scratch.lean"); fs::read_to_string(path).ok() } @@ -168,11 +173,7 @@ impl AppStore { Ok(files) } - fn walk_workspace( - base: &Path, - current: &Path, - out: &mut Vec<(String, u64)>, - ) -> Result<()> { + fn walk_workspace(base: &Path, current: &Path, out: &mut Vec<(String, u64)>) -> Result<()> { let entries = fs::read_dir(current) .with_context(|| format!("reading workspace dir {}", current.display()))?; for entry in entries { @@ -180,7 +181,8 @@ impl AppStore { let path = entry.path(); // Skip the history directory. if path.is_dir() { - let name = path.file_name() + let name = path + .file_name() .map(|n| n.to_string_lossy().to_string()) .unwrap_or_default(); // Skip build artifacts, history, hidden dirs, and package dirs diff --git a/crates/openproof-tui/src/custom_terminal.rs b/crates/openproof-tui/src/custom_terminal.rs index fe993c0..7a22006 100644 --- a/crates/openproof-tui/src/custom_terminal.rs +++ b/crates/openproof-tui/src/custom_terminal.rs @@ -96,7 +96,9 @@ impl Drop for CustomTerminal { impl CustomTerminal { pub fn with_options(mut backend: B) -> io::Result { let screen_size = backend.size()?; - let cursor_pos = backend.get_cursor_position().unwrap_or(Position { x: 0, y: 0 }); + let cursor_pos = backend + .get_cursor_position() + .unwrap_or(Position { x: 0, y: 0 }); Ok(Self { backend, buffers: [Buffer::empty(Rect::ZERO), Buffer::empty(Rect::ZERO)], @@ -206,12 +208,7 @@ impl CustomTerminal { self.last_known_screen_size = screen_size; // Recompute viewport to fill the terminal from the current y position let height = screen_size.height.saturating_sub(self.viewport_area.y); - let new_area = Rect::new( - 0, - self.viewport_area.y, - screen_size.width, - height, - ); + let new_area = Rect::new(0, self.viewport_area.y, screen_size.width, height); self.set_viewport_area(new_area); } Ok(()) @@ -280,10 +277,7 @@ impl CustomTerminal { /// Push lines into terminal scrollback by scrolling the viewport area up. /// This is what makes the native scrollbar work -- content moves from the /// viewport into the terminal's scrollback buffer. - pub fn scroll_region_up( - &mut self, - rows_to_scroll: u16, - ) -> io::Result<()> { + pub fn scroll_region_up(&mut self, rows_to_scroll: u16) -> io::Result<()> { if rows_to_scroll == 0 || self.viewport_area.is_empty() { return Ok(()); } @@ -348,7 +342,10 @@ where modifier = cell.modifier; } if cell.fg != fg || cell.bg != bg { - queue!(writer, SetColors(Colors::new(cell.fg.into(), cell.bg.into())))?; + queue!( + writer, + SetColors(Colors::new(cell.fg.into(), cell.bg.into())) + )?; fg = cell.fg; bg = cell.bg; } diff --git a/crates/openproof-tui/src/insert_history.rs b/crates/openproof-tui/src/insert_history.rs index a4ab091..f3005a9 100644 --- a/crates/openproof-tui/src/insert_history.rs +++ b/crates/openproof-tui/src/insert_history.rs @@ -25,10 +25,7 @@ use crate::custom_terminal::CustomTerminal; /// terminal scrollback), then write the new content in the space created /// above the viewport. The viewport position doesn't change relative to the /// bottom of the screen. -pub fn insert_history_lines( - terminal: &mut CustomTerminal, - lines: Vec, -) -> io::Result<()> +pub fn insert_history_lines(terminal: &mut CustomTerminal, lines: Vec) -> io::Result<()> where B: Backend + Write, { @@ -121,13 +118,25 @@ fn write_line_spans(writer: &mut impl Write, line: &Line) -> io::Result<()> { let bg = span.style.bg.map(Into::into).unwrap_or(CColor::Reset); queue!(writer, SetColors(Colors::new(fg, bg)))?; - if span.style.add_modifier.contains(ratatui::style::Modifier::BOLD) { + if span + .style + .add_modifier + .contains(ratatui::style::Modifier::BOLD) + { queue!(writer, SetAttribute(crossterm::style::Attribute::Bold))?; } - if span.style.add_modifier.contains(ratatui::style::Modifier::DIM) { + if span + .style + .add_modifier + .contains(ratatui::style::Modifier::DIM) + { queue!(writer, SetAttribute(crossterm::style::Attribute::Dim))?; } - if span.style.add_modifier.contains(ratatui::style::Modifier::ITALIC) { + if span + .style + .add_modifier + .contains(ratatui::style::Modifier::ITALIC) + { queue!(writer, SetAttribute(crossterm::style::Attribute::Italic))?; } diff --git a/crates/openproof-tui/src/lib.rs b/crates/openproof-tui/src/lib.rs index e738024..22bb5ee 100644 --- a/crates/openproof-tui/src/lib.rs +++ b/crates/openproof-tui/src/lib.rs @@ -128,7 +128,10 @@ pub fn render_entry(entry: &openproof_protocol::TranscriptEntry) -> Vec> ", Style::default().fg(Color::Cyan).add_modifier(Modifier::DIM)), + Span::styled( + ">> ", + Style::default().fg(Color::Cyan).add_modifier(Modifier::DIM), + ), Span::styled(tool_name.to_string(), Style::default().fg(Color::Cyan)), Span::styled( format!("({args_summary})"), @@ -142,10 +145,17 @@ pub fn render_entry(entry: &openproof_protocol::TranscriptEntry) -> Vec = entry.content.lines().take(10).collect(); let truncated = output_lines.len() < entry.content.lines().count(); lines.push(Line::from(vec![ - Span::styled("<< ", Style::default().fg(Color::Green).add_modifier(Modifier::DIM)), + Span::styled( + "<< ", + Style::default() + .fg(Color::Green) + .add_modifier(Modifier::DIM), + ), Span::styled( format!("{tool_name}: "), - Style::default().fg(Color::Green).add_modifier(Modifier::DIM), + Style::default() + .fg(Color::Green) + .add_modifier(Modifier::DIM), ), ])); for ol in &output_lines { @@ -165,7 +175,9 @@ pub fn render_entry(entry: &openproof_protocol::TranscriptEntry) -> Vec Vec Vec {thought_line}"), - Style::default().fg(Color::DarkGray).add_modifier(Modifier::ITALIC), + Style::default() + .fg(Color::DarkGray) + .add_modifier(Modifier::ITALIC), ))); } } @@ -213,7 +229,8 @@ pub fn draw(frame: &mut custom_terminal::Frame<'_>, state: &mut AppState) { let area = frame.area(); let prefix_len = 2; // "> " - let input_height = compute_input_height(&state.composer, prefix_len, area.width, &state.paste_blocks); + let input_height = + compute_input_height(&state.composer, prefix_len, area.width, &state.paste_blocks); let chunks = Layout::default() .direction(Direction::Vertical) @@ -343,21 +360,29 @@ fn draw_chat_area(f: &mut custom_terminal::Frame<'_>, state: &mut AppState, area } openproof_protocol::MessageRole::Assistant => { let cleaned = strip_markers(&entry.content); - lines.extend(markdown::render_markdown( - &cleaned, - Style::default(), - )); + lines.extend(markdown::render_markdown(&cleaned, Style::default())); } openproof_protocol::MessageRole::ToolCall => { let tool_name = entry.title.as_deref().unwrap_or("tool"); let args_summary = if entry.content.len() > 100 { - format!("{}...", entry.content.chars().take(100).collect::()) + format!( + "{}...", + entry.content.chars().take(100).collect::() + ) } else { entry.content.clone() }; lines.push(Line::from(vec![ - Span::styled(">> ", Style::default().fg(Color::Cyan).add_modifier(Modifier::DIM)), - Span::styled(tool_name.to_string(), Style::default().fg(Color::Cyan)), + Span::styled( + ">> ", + Style::default() + .fg(Color::Cyan) + .add_modifier(Modifier::DIM), + ), + Span::styled( + tool_name.to_string(), + Style::default().fg(Color::Cyan), + ), Span::styled( format!("({args_summary})"), Style::default().fg(Color::DarkGray), @@ -366,20 +391,32 @@ fn draw_chat_area(f: &mut custom_terminal::Frame<'_>, state: &mut AppState, area } openproof_protocol::MessageRole::ToolResult => { let tool_name = entry.title.as_deref().unwrap_or("tool"); - let output_lines: Vec<&str> = entry.content.lines().take(10).collect(); + let output_lines: Vec<&str> = + entry.content.lines().take(10).collect(); let truncated = output_lines.len() < entry.content.lines().count(); lines.push(Line::from(vec![ - Span::styled("<< ", Style::default().fg(Color::Green).add_modifier(Modifier::DIM)), + Span::styled( + "<< ", + Style::default() + .fg(Color::Green) + .add_modifier(Modifier::DIM), + ), Span::styled( format!("{tool_name}: "), - Style::default().fg(Color::Green).add_modifier(Modifier::DIM), + Style::default() + .fg(Color::Green) + .add_modifier(Modifier::DIM), ), ])); for ol in &output_lines { let trimmed = ol.trim(); - let style = if trimmed.starts_with('+') && !trimmed.starts_with("+++") { + let style = if trimmed.starts_with('+') + && !trimmed.starts_with("+++") + { Style::default().fg(Color::Green) - } else if trimmed.starts_with('-') && !trimmed.starts_with("---") { + } else if trimmed.starts_with('-') + && !trimmed.starts_with("---") + { Style::default().fg(Color::Red) } else if trimmed.starts_with("@@") { Style::default().fg(Color::Cyan).add_modifier(Modifier::DIM) @@ -391,7 +428,9 @@ fn draw_chat_area(f: &mut custom_terminal::Frame<'_>, state: &mut AppState, area if truncated { lines.push(Line::from(Span::styled( " ... (output truncated)".to_string(), - Style::default().fg(Color::DarkGray).add_modifier(Modifier::DIM), + Style::default() + .fg(Color::DarkGray) + .add_modifier(Modifier::DIM), ))); } } @@ -425,7 +464,10 @@ fn draw_chat_area(f: &mut custom_terminal::Frame<'_>, state: &mut AppState, area .add_modifier(Modifier::BOLD), ))); if matches!( - state.current_session().and_then(|s| s.transcript.last()).map(|e| e.role), + state + .current_session() + .and_then(|s| s.transcript.last()) + .map(|e| e.role), Some(openproof_protocol::MessageRole::Assistant) ) { // Already have an assistant header from prior streaming @@ -449,17 +491,10 @@ fn draw_chat_area(f: &mut custom_terminal::Frame<'_>, state: &mut AppState, area let elapsed_str = if elapsed_ms < 60_000 { format!("{}s", elapsed_ms / 1000) } else { - format!( - "{}m {}s", - elapsed_ms / 60_000, - (elapsed_ms % 60_000) / 1000 - ) + format!("{}m {}s", elapsed_ms / 60_000, (elapsed_ms % 60_000) / 1000) }; all_lines.push(Line::from(vec![ - Span::styled( - format!(" {spinner} "), - Style::default().fg(Color::Yellow), - ), + Span::styled(format!(" {spinner} "), Style::default().fg(Color::Yellow)), Span::styled("Thinking... ", Style::default().fg(Color::DarkGray)), Span::styled( format!("({elapsed_str})"), @@ -524,11 +559,7 @@ fn draw_input_area(f: &mut custom_terminal::Frame<'_>, state: &AppState, area: R .add_modifier(Modifier::BOLD), ); - let raw_lines = build_input_lines( - &state.composer, - state.composer_cursor, - &state.paste_blocks, - ); + let raw_lines = build_input_lines(&state.composer, state.composer_cursor, &state.paste_blocks); // Prepend the "> " prefix to the first line. let mut lines: Vec> = Vec::with_capacity(raw_lines.len()); @@ -574,18 +605,25 @@ fn draw_input_area(f: &mut custom_terminal::Frame<'_>, state: &AppState, area: R // --------------------------------------------------------------------------- fn draw_status_bar(f: &mut custom_terminal::Frame<'_>, state: &AppState, area: Rect) { - let is_autonomous = state.current_session() + let is_autonomous = state + .current_session() .map(|s| s.proof.is_autonomous_running) .unwrap_or(false); - let auto_iter = state.current_session() + let auto_iter = state + .current_session() .map(|s| s.proof.autonomous_iteration_count) .unwrap_or(0); let text = if state.turn_in_flight || state.verification_in_flight { - let elapsed = state.activity_started_at + let elapsed = state + .activity_started_at .map(|t| t.elapsed().as_secs()) .unwrap_or(0); - let elapsed_str = if elapsed > 0 { format!(" ({elapsed}s)") } else { String::new() }; + let elapsed_str = if elapsed > 0 { + format!(" ({elapsed}s)") + } else { + String::new() + }; let label = if !state.activity_label.is_empty() { state.activity_label.clone() } else if state.verification_in_flight { @@ -606,10 +644,15 @@ fn draw_status_bar(f: &mut custom_terminal::Frame<'_>, state: &AppState, area: R let activity = format!("{auto_prefix}{label}{elapsed_str}{iter_info}"); Span::styled(activity, Style::default().fg(Color::Yellow)) } else if is_autonomous { - let full = state.current_session() + let full = state + .current_session() .map(|s| s.proof.full_autonomous) .unwrap_or(false); - let mode_label = if full { "full autonomous" } else { "autonomous" }; + let mode_label = if full { + "full autonomous" + } else { + "autonomous" + }; Span::styled( format!(" {mode_label} (iter {auto_iter}) | idle between steps (shift+tab to cycle)"), Style::default().fg(Color::Cyan), @@ -620,8 +663,7 @@ fn draw_status_bar(f: &mut custom_terminal::Frame<'_>, state: &AppState, area: R Style::default().fg(Color::DarkGray), ) }; - let para = - Paragraph::new(Line::from(text)).style(Style::default().bg(Color::Rgb(30, 30, 30))); + let para = Paragraph::new(Line::from(text)).style(Style::default().bg(Color::Rgb(30, 30, 30))); f.render_widget(para, area); } @@ -692,16 +734,24 @@ fn draw_completion_popup(f: &mut custom_terminal::Frame<'_>, state: &AppState, c // Overlays // --------------------------------------------------------------------------- -fn draw_overlay(f: &mut custom_terminal::Frame<'_>, state: &AppState, overlay: &Overlay, area: Rect) { +fn draw_overlay( + f: &mut custom_terminal::Frame<'_>, + state: &AppState, + overlay: &Overlay, + area: Rect, +) { match overlay { Overlay::SessionPicker { selected } => draw_session_picker(f, state, *selected, area), - Overlay::FocusPicker { items, selected } => { - draw_focus_picker(f, items, *selected, area) - } + Overlay::FocusPicker { items, selected } => draw_focus_picker(f, items, *selected, area), } } -fn draw_session_picker(f: &mut custom_terminal::Frame<'_>, state: &AppState, selected: usize, area: Rect) { +fn draw_session_picker( + f: &mut custom_terminal::Frame<'_>, + state: &AppState, + selected: usize, + area: Rect, +) { let popup = centered_rect(75, 60, area); f.render_widget(Clear, popup); @@ -730,7 +780,10 @@ fn draw_session_picker(f: &mut custom_terminal::Frame<'_>, state: &AppState, sel height: 1, }; let header = Paragraph::new(Line::from(Span::styled( - format!(" {:30} {:>5} {:>5} {}", "Title", "Msgs", "Nodes", "Updated"), + format!( + " {:30} {:>5} {:>5} {}", + "Title", "Msgs", "Nodes", "Updated" + ), Style::default() .fg(Color::DarkGray) .add_modifier(Modifier::BOLD), @@ -763,7 +816,11 @@ fn draw_session_picker(f: &mut custom_terminal::Frame<'_>, state: &AppState, sel } else { Style::default().fg(Color::White) }; - let active = if i == state.selected_session { "*" } else { " " }; + let active = if i == state.selected_session { + "*" + } else { + " " + }; let ts: String = s.updated_at.chars().take(10).collect(); let title: String = s.title.chars().take(28).collect(); let text = format!( @@ -912,11 +969,7 @@ fn paste_label(block_idx: usize, paste_blocks: &[String]) -> String { /// Build `Line` objects for the composer, handling newlines, paste block /// markers, and cursor rendering. Each `\n` becomes a line break. -fn build_input_lines( - text: &str, - cursor: usize, - paste_blocks: &[String], -) -> Vec> { +fn build_input_lines(text: &str, cursor: usize, paste_blocks: &[String]) -> Vec> { let cursor_style = Style::default().fg(Color::Black).bg(Color::White); if text.is_empty() { @@ -956,10 +1009,7 @@ fn build_input_lines( // Cursor on the paste marker: highlight first char of label. let mut label_chars = label.chars(); let first = label_chars.next().unwrap_or(' '); - current_spans.push(Span::styled( - first.to_string(), - cursor_style, - )); + current_spans.push(Span::styled(first.to_string(), cursor_style)); let rest: String = label_chars.collect(); if !rest.is_empty() { current_spans.push(Span::styled(rest, paste_label_style())); @@ -968,17 +1018,15 @@ fn build_input_lines( current_spans.push(Span::styled(label, paste_label_style())); } block_idx += 1; - } else { - if at_cursor { - // Flush buffer, then emit cursor char. - if !buf.is_empty() { - current_spans.push(Span::raw(buf.clone())); - buf.clear(); - } - current_spans.push(Span::styled(ch.to_string(), cursor_style)); - } else { - buf.push(ch); + } else if at_cursor { + // Flush buffer, then emit cursor char. + if !buf.is_empty() { + current_spans.push(Span::raw(buf.clone())); + buf.clear(); } + current_spans.push(Span::styled(ch.to_string(), cursor_style)); + } else { + buf.push(ch); } } @@ -998,7 +1046,12 @@ fn build_input_lines( /// Compute the height needed for the input area, accounting for text wrapping, /// newlines, and paste block display labels. -fn compute_input_height(text: &str, prefix_len: usize, area_width: u16, paste_blocks: &[String]) -> u16 { +fn compute_input_height( + text: &str, + prefix_len: usize, + area_width: u16, + paste_blocks: &[String], +) -> u16 { let usable = area_width as usize; if usable == 0 { return 3; diff --git a/crates/openproof-tui/src/markdown.rs b/crates/openproof-tui/src/markdown.rs index 0859510..5954f38 100644 --- a/crates/openproof-tui/src/markdown.rs +++ b/crates/openproof-tui/src/markdown.rs @@ -296,7 +296,10 @@ mod tests { fn header_level_1() { let lines = render_markdown("# My Header", Style::default()); assert_eq!(lines[0].spans[0].style.fg, Some(Color::Cyan)); - assert!(lines[0].spans[0].style.add_modifier.contains(Modifier::BOLD)); + assert!(lines[0].spans[0] + .style + .add_modifier + .contains(Modifier::BOLD)); } #[test] @@ -310,7 +313,10 @@ mod tests { fn link_shows_text() { let lines = render_markdown("See [docs](https://example.com)", Style::default()); let spans = &lines[0].spans; - let link_span = spans.iter().find(|s| s.style.fg == Some(Color::Cyan)).unwrap(); + let link_span = spans + .iter() + .find(|s| s.style.fg == Some(Color::Cyan)) + .unwrap(); assert_eq!(span_text(link_span), "docs"); } @@ -318,7 +324,10 @@ mod tests { fn inline_code_has_yellow() { let lines = render_markdown("Use `cargo build` here", Style::default()); let spans = &lines[0].spans; - let code_span = spans.iter().find(|s| s.style.fg == Some(Color::Yellow)).unwrap(); + let code_span = spans + .iter() + .find(|s| s.style.fg == Some(Color::Yellow)) + .unwrap(); assert_eq!(span_text(code_span), "cargo build"); }