From 9d42a44a647259a3347a2e86ca1aeb2e533fa28c Mon Sep 17 00:00:00 2001 From: markm39 Date: Fri, 27 Mar 2026 22:44:01 -0500 Subject: [PATCH] feat(dashboard): add session management and fix loading performance Add delete, rename, and bulk delete operations to the dashboard sidebar. Sessions can now be managed via a "Manage" toggle that reveals checkboxes, inline rename, and delete controls. Fix slow dashboard loading by replacing full JSON blob deserialization with SQLite json_array_length() queries for the session list polling endpoint. Store layer: - list_session_summaries() uses SQL json functions to avoid deserializing transcript/proof/cloud blobs - delete_session() cleans up sessions, verification_runs, attempt_logs, sync_queue rows, and workspace directories - delete_sessions() bulk deletes in a single transaction - rename_session() updates title and timestamp Dashboard server: - Split lib.rs (516 lines) into lib.rs + routes.rs + manage.rs + tex.rs - New endpoints: DELETE /api/session, PATCH /api/session, POST /api/sessions/bulk-delete, GET /api/session-summaries - status() and sessions() handlers now use lightweight summaries Dashboard frontend: - Extract graph components to graph.js (was pushing app.js over 500 lines) - New SessionSidebar component in sessions.js with manage mode - Sidebar polls /api/session-summaries (lightweight) every 2s - Status polling (lean health, auth) reduced to every 10s --- Cargo.lock | 1 + crates/openproof-dashboard/Cargo.toml | 1 + crates/openproof-dashboard/src/lib.rs | 473 ++--------------- crates/openproof-dashboard/src/manage.rs | 70 +++ crates/openproof-dashboard/src/routes.rs | 223 ++++++++ crates/openproof-dashboard/src/tex.rs | 170 ++++++ crates/openproof-dashboard/static/app.js | 501 +++--------------- crates/openproof-dashboard/static/graph.js | 328 ++++++++++++ crates/openproof-dashboard/static/sessions.js | 177 +++++++ crates/openproof-dashboard/static/styles.css | 99 +++- crates/openproof-store/src/sessions.rs | 112 +++- 11 files changed, 1299 insertions(+), 856 deletions(-) create mode 100644 crates/openproof-dashboard/src/manage.rs create mode 100644 crates/openproof-dashboard/src/routes.rs create mode 100644 crates/openproof-dashboard/src/tex.rs create mode 100644 crates/openproof-dashboard/static/graph.js create mode 100644 crates/openproof-dashboard/static/sessions.js diff --git a/Cargo.lock b/Cargo.lock index 3d5312e..6abda43 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1294,6 +1294,7 @@ dependencies = [ "openproof-protocol", "openproof-store", "serde", + "serde_json", "tokio", ] diff --git a/crates/openproof-dashboard/Cargo.toml b/crates/openproof-dashboard/Cargo.toml index 6c387ca..94f41f5 100644 --- a/crates/openproof-dashboard/Cargo.toml +++ b/crates/openproof-dashboard/Cargo.toml @@ -8,6 +8,7 @@ license.workspace = true anyhow.workspace = true axum.workspace = true serde.workspace = true +serde_json.workspace = true tokio.workspace = true openproof-protocol = { path = "../openproof-protocol" } openproof-store = { path = "../openproof-store" } diff --git a/crates/openproof-dashboard/src/lib.rs b/crates/openproof-dashboard/src/lib.rs index 10f503a..0e96aff 100644 --- a/crates/openproof-dashboard/src/lib.rs +++ b/crates/openproof-dashboard/src/lib.rs @@ -1,28 +1,28 @@ +//! Web dashboard for OpenProof session inspection and management. + +mod manage; +mod routes; +mod tex; + use anyhow::Result; use axum::{ - extract::{Query, State}, - http::{header::CONTENT_TYPE, StatusCode}, - response::{Html, IntoResponse}, - routing::get, - Json, Router, -}; -use openproof_lean::detect_lean_health; -use openproof_model::load_auth_summary; -use openproof_protocol::{ - DashboardSessionSummary, DashboardStatusResponse, HealthReport, MessageRole, SessionSnapshot, + routing::{get, post}, + Router, }; use openproof_store::AppStore; -use std::{net::SocketAddr, process::Command, sync::Arc}; +use std::{net::SocketAddr, sync::Arc}; use tokio::{net::TcpListener, sync::oneshot, task::JoinHandle}; const INDEX_HTML: &str = include_str!("../static/index.html"); const APP_JS: &str = include_str!("../static/app.js"); const STYLES_CSS: &str = include_str!("../static/styles.css"); +const SESSIONS_JS: &str = include_str!("../static/sessions.js"); +const GRAPH_JS: &str = include_str!("../static/graph.js"); #[derive(Clone)] -struct DashboardState { - store: AppStore, - lean_project_dir: std::path::PathBuf, +pub(crate) struct DashboardState { + pub store: AppStore, + pub lean_project_dir: std::path::PathBuf, } pub struct DashboardServer { @@ -52,17 +52,29 @@ pub async fn start_dashboard_server( }); let router = Router::new() - .route("/", get(index)) - .route("/app.js", get(app_js)) - .route("/styles.css", get(styles_css)) - .route("/api/status", get(status)) - .route("/api/health", get(health)) - .route("/api/sessions", get(sessions)) - .route("/api/session", get(session)) - .route("/api/raw-state", get(status)) - .route("/api/paper/tex", get(paper_tex)) - .route("/api/paper/pdf", get(paper_pdf)) - .route("/api/workspace", get(workspace_files)) + .route("/", get(routes::index)) + .route("/app.js", get(routes::app_js)) + .route("/styles.css", get(routes::styles_css)) + .route("/sessions.js", get(routes::sessions_js)) + .route("/graph.js", get(routes::graph_js)) + .route("/api/status", get(routes::status)) + .route("/api/health", get(routes::health)) + .route("/api/sessions", get(routes::sessions)) + .route("/api/session-summaries", get(routes::session_summaries)) + .route( + "/api/session", + get(routes::session) + .delete(manage::delete_session) + .patch(manage::rename_session), + ) + .route( + "/api/sessions/bulk-delete", + post(manage::bulk_delete_sessions), + ) + .route("/api/raw-state", get(routes::status)) + .route("/api/paper/tex", get(routes::paper_tex)) + .route("/api/paper/pdf", get(routes::paper_pdf)) + .route("/api/workspace", get(routes::workspace_files)) .with_state(state); let primary_port = preferred_port.unwrap_or(4821); @@ -90,426 +102,21 @@ pub async fn start_dashboard_server( pub fn open_browser(url: &str) { let platform = std::env::consts::OS; let mut command = if platform == "macos" { - let mut cmd = Command::new("open"); + let mut cmd = std::process::Command::new("open"); cmd.arg(url); cmd } else if platform == "windows" { - let mut cmd = Command::new("cmd"); + let mut cmd = std::process::Command::new("cmd"); cmd.args(["/c", "start", "", url]); cmd } else { - let mut cmd = Command::new("xdg-open"); + let mut cmd = std::process::Command::new("xdg-open"); cmd.arg(url); cmd }; let _ = command.spawn(); } -async fn index() -> Html<&'static str> { - Html(INDEX_HTML) -} - -async fn app_js() -> impl IntoResponse { - ( - [(CONTENT_TYPE, "application/javascript; charset=utf-8")], - APP_JS, - ) -} - -async fn styles_css() -> impl IntoResponse { - ([(CONTENT_TYPE, "text/css; charset=utf-8")], STYLES_CSS) -} - -async fn status( - State(state): State>, -) -> Result, (StatusCode, String)> { - let sessions = state.store.list_sessions().map_err(internal_error)?; - let auth = load_auth_summary().unwrap_or_default(); - let lean = detect_lean_health(&state.lean_project_dir).unwrap_or_default(); - let payload = DashboardStatusResponse { - local_db_path: state.store.db_path().display().to_string(), - auth, - lean, - session_count: sessions.len(), - active_session_id: sessions.first().map(|session| session.id.clone()), - sessions: sessions.iter().map(build_session_summary).collect(), - }; - Ok(Json(payload)) -} - -async fn health( - State(state): State>, -) -> Result, (StatusCode, String)> { - let latest_session = state.store.latest_session().map_err(internal_error)?; - let auth = load_auth_summary().unwrap_or_default(); - let lean = detect_lean_health(&state.lean_project_dir).unwrap_or_default(); - let payload = HealthReport { - ok: lean.ok, - local_db_path: state.store.db_path().display().to_string(), - session_count: state.store.session_count().map_err(internal_error)?, - latest_session_id: latest_session.map(|session| session.id), - auth, - lean, - }; - Ok(Json(payload)) -} - -async fn sessions( - State(state): State>, -) -> Result>, (StatusCode, String)> { - let sessions = state - .store - .list_sessions() - .map_err(internal_error)? - .iter() - .map(build_session_summary) - .collect::>(); - Ok(Json(sessions)) -} - -#[derive(Debug, serde::Deserialize)] -struct SessionQuery { - id: Option, -} - -async fn session( - State(state): State>, - Query(query): Query, -) -> Result { - let session = match query.id.as_deref() { - Some(id) => state.store.get_session(id).map_err(internal_error)?, - None => state.store.latest_session().map_err(internal_error)?, - }; - match session { - Some(session) => Ok(Json(session).into_response()), - None => Ok(StatusCode::NOT_FOUND.into_response()), - } -} - -async fn paper_tex( - State(state): State>, - Query(query): Query, -) -> Result { - let session = match query.id.as_deref() { - Some(id) => state.store.get_session(id).map_err(internal_error)?, - None => state.store.latest_session().map_err(internal_error)?, - }; - let Some(session) = session else { - return Ok((StatusCode::NOT_FOUND, "No session").into_response()); - }; - // Read Paper.tex directly from workspace (source of truth) - let ws_dir = state.store.workspace_dir(&session.id); - let paper_file = std::fs::read_to_string(ws_dir.join("Paper.tex")).unwrap_or_default(); - let tex = if !paper_file.trim().is_empty() { - paper_file - } else { - generate_tex(&session) - }; - Ok(([(CONTENT_TYPE, "text/plain; charset=utf-8")], tex).into_response()) -} - -async fn paper_pdf( - State(state): State>, - Query(query): Query, -) -> Result { - let session = match query.id.as_deref() { - Some(id) => state.store.get_session(id).map_err(internal_error)?, - None => state.store.latest_session().map_err(internal_error)?, - }; - let Some(session) = session else { - return Ok((StatusCode::NOT_FOUND, "No session").into_response()); - }; - let tex = generate_tex(&session); - - // Compile in a temp directory. - let tmp = std::env::temp_dir().join("openproof-paper"); - let _ = std::fs::create_dir_all(&tmp); - let tex_path = tmp.join("paper.tex"); - std::fs::write(&tex_path, &tex).map_err(|e| internal_error(e.into()))?; - - let output = Command::new("lualatex") - .args(["-interaction=nonstopmode", "-halt-on-error", "paper.tex"]) - .current_dir(&tmp) - .output() - .map_err(|e| internal_error(anyhow::anyhow!("lualatex failed to start: {e}")))?; - - let pdf_path = tmp.join("paper.pdf"); - if !pdf_path.exists() { - let stderr = String::from_utf8_lossy(&output.stdout); - return Ok(( - StatusCode::INTERNAL_SERVER_ERROR, - format!("lualatex failed:\n{stderr}"), - ) - .into_response()); - } - - let pdf_bytes = std::fs::read(&pdf_path).map_err(|e| internal_error(e.into()))?; - Ok(([(CONTENT_TYPE, "application/pdf")], pdf_bytes).into_response()) -} - -async fn workspace_files( - State(state): State>, - Query(query): Query, -) -> Result { - let session = match query.id.as_deref() { - Some(id) => state.store.get_session(id).map_err(internal_error)?, - None => state.store.latest_session().map_err(internal_error)?, - }; - let Some(session) = session else { - return Ok("[]".to_string().into_response()); - }; - let ws_dir = state.store.workspace_dir(&session.id); - let mut result = String::from("["); - let mut first = true; - if let Ok(entries) = state.store.list_workspace_files(&session.id) { - 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(','); - } - first = false; - // Manual JSON to avoid serde_json dependency - let escaped = content - .replace('\\', "\\\\") - .replace('"', "\\\"") - .replace('\n', "\\n") - .replace('\r', "\\r") - .replace('\t', "\\t"); - result.push_str(&format!( - "{{\"path\":\"{path}\",\"content\":\"{escaped}\"}}" - )); - } - } - } - result.push(']'); - Ok(([(CONTENT_TYPE, "application/json")], result).into_response()) -} - -fn generate_tex(session: &SessionSnapshot) -> String { - let proof = &session.proof; - let title = &session.title; - - // If the model has written a LaTeX paper body, use it directly. - if !proof.paper_tex.trim().is_empty() { - // If paper_tex is already a complete document, return it as-is - if proof.paper_tex.contains("\\documentclass") { - return proof.paper_tex.clone(); - } - let mut doc = String::new(); - doc.push_str("\\documentclass[11pt]{article}\n"); - doc.push_str("\\usepackage[margin=1in]{geometry}\n"); - doc.push_str("\\usepackage{fontspec}\n"); - doc.push_str("\\usepackage{amsmath,amssymb,amsthm}\n"); - doc.push_str("\\usepackage{listings}\n"); - doc.push_str("\\usepackage{xcolor}\n"); - doc.push_str("\\lstset{basicstyle=\\ttfamily\\small,breaklines=true,frame=single,backgroundcolor=\\color{gray!10},literate=\n"); - doc.push_str(" {ℕ}{{\\ensuremath{\\mathbb{N}}}}1\n"); - doc.push_str(" {ℝ}{{\\ensuremath{\\mathbb{R}}}}1\n"); - doc.push_str(" {ℤ}{{\\ensuremath{\\mathbb{Z}}}}1\n"); - doc.push_str(" {→}{{\\ensuremath{\\to}}}1\n"); - doc.push_str(" {←}{{\\ensuremath{\\leftarrow}}}1\n"); - doc.push_str(" {∀}{{\\ensuremath{\\forall}}}1\n"); - doc.push_str(" {∃}{{\\ensuremath{\\exists}}}1\n"); - doc.push_str(" {∧}{{\\ensuremath{\\land}}}1\n"); - doc.push_str(" {∨}{{\\ensuremath{\\lor}}}1\n"); - doc.push_str(" {≤}{{\\ensuremath{\\leq}}}1\n"); - doc.push_str(" {≥}{{\\ensuremath{\\geq}}}1\n"); - doc.push_str(" {≠}{{\\ensuremath{\\neq}}}1\n"); - doc.push_str(" {∈}{{\\ensuremath{\\in}}}1\n"); - doc.push_str(" {⟨}{{\\ensuremath{\\langle}}}1\n"); - doc.push_str(" {⟩}{{\\ensuremath{\\rangle}}}1\n"); - doc.push_str(" {λ}{{\\ensuremath{\\lambda}}}1\n"); - doc.push_str(" {∑}{{\\ensuremath{\\sum}}}1\n"); - doc.push_str(" {∞}{{\\ensuremath{\\infty}}}1\n"); - doc.push_str("}\n"); - 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(&format!("\n\\title{{{}}}\n", tex_escape(title))); - doc.push_str("\\author{OpenProof}\n"); - 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 - .replace("[language=Lean]", "") - .replace("[language=lean]", "") - .replace("[language=lean4]", "") - .replace("[language=Lean4]", ""); - doc.push_str(&sanitized); - doc.push_str("\n\n\\end{document}\n"); - return doc; - } - - // Fallback: mechanical generation from proof state. - let mut doc = String::new(); - doc.push_str("\\documentclass[11pt]{article}\n"); - doc.push_str("\\usepackage[margin=1in]{geometry}\n"); - doc.push_str("\\usepackage{amsmath,amssymb,amsthm}\n"); - doc.push_str("\\usepackage{listings}\n"); - doc.push_str("\\usepackage{xcolor}\n"); - doc.push_str("\\lstset{basicstyle=\\ttfamily\\small,breaklines=true,frame=single,backgroundcolor=\\color{gray!10}}\n"); - 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('\n'); - doc.push_str(&format!("\\title{{{}}}\n", tex_escape(title))); - doc.push_str("\\author{OpenProof}\n"); - doc.push_str("\\date{\\today}\n"); - doc.push_str("\n\\begin{document}\n\\maketitle\n\n"); - - // Problem statement - if let Some(problem) = &proof.problem { - if !problem.trim().is_empty() { - doc.push_str("\\section*{Problem}\n"); - doc.push_str(&tex_escape(problem)); - doc.push_str("\n\n"); - } - } - - // Formal target - if let Some(target) = &proof.formal_target { - if !target.trim().is_empty() { - doc.push_str("\\section*{Formal Target}\n"); - doc.push_str("\\begin{lstlisting}[language={}]\n"); - doc.push_str(target); - doc.push_str("\n\\end{lstlisting}\n\n"); - } - } - - // Proof nodes - if !proof.nodes.is_empty() { - doc.push_str("\\section{Proof Structure}\n\n"); - for node in &proof.nodes { - let env = match node.kind { - openproof_protocol::ProofNodeKind::Theorem => "theorem", - openproof_protocol::ProofNodeKind::Lemma => "lemma", - _ => "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}]}" - } - _ => "", - }; - doc.push_str(&format!( - "\\begin{{{env}}}[{}]{status_marker}\n", - tex_escape(&node.label) - )); - if !node.statement.is_empty() { - doc.push_str(&tex_escape(&node.statement)); - doc.push('\n'); - } - doc.push_str(&format!("\\end{{{env}}}\n\n")); - - if !node.content.trim().is_empty() { - doc.push_str("\\begin{lstlisting}[language={}]\n"); - doc.push_str(&node.content); - doc.push_str("\n\\end{lstlisting}\n\n"); - } - } - } - - // Paper notes - if !proof.paper_notes.is_empty() { - doc.push_str("\\section{Notes}\n\n"); - doc.push_str("\\begin{itemize}\n"); - for note in &proof.paper_notes { - doc.push_str(&format!("\\item {}\n", tex_escape(note))); - } - doc.push_str("\\end{itemize}\n\n"); - } - - // Strategy summary - if let Some(strategy) = &proof.strategy_summary { - if !strategy.trim().is_empty() { - doc.push_str("\\section{Strategy}\n\n"); - doc.push_str(&tex_escape(strategy)); - doc.push_str("\n\n"); - } - } - - doc.push_str("\\end{document}\n"); - doc -} - -fn tex_escape(s: &str) -> String { - s.replace('\\', "\\textbackslash{}") - .replace('{', "\\{") - .replace('}', "\\}") - .replace('&', "\\&") - .replace('%', "\\%") - .replace('$', "\\$") - .replace('#', "\\#") - .replace('_', "\\_") - .replace('^', "\\^{}") - .replace('~', "\\~{}") -} - -fn build_session_summary(session: &SessionSnapshot) -> DashboardSessionSummary { - let last_entry = session.transcript.last(); - let active_node_label = session - .proof - .active_node_id - .as_deref() - .and_then(|id| session.proof.nodes.iter().find(|node| node.id == id)) - .map(|node| node.label.clone()); - DashboardSessionSummary { - id: session.id.clone(), - title: session.title.clone(), - updated_at: session.updated_at.clone(), - workspace_label: session.workspace_label.clone(), - transcript_entries: session.transcript.len(), - proof_nodes: session.proof.nodes.len(), - active_node_label, - proof_phase: Some(session.proof.phase.clone()), - last_role: last_entry.map(|entry| match entry.role { - MessageRole::User => "user".to_string(), - MessageRole::Assistant => "assistant".to_string(), - MessageRole::System => "system".to_string(), - MessageRole::Notice => "notice".to_string(), - MessageRole::ToolCall => "tool_call".to_string(), - MessageRole::ToolResult => "tool_result".to_string(), - MessageRole::Diff => "diff".to_string(), - MessageRole::Thought => "thought".to_string(), - }), - last_excerpt: last_entry.map(|entry| match entry.role { - MessageRole::ToolCall => { - let name = entry.title.as_deref().unwrap_or("tool"); - format!(">> {name}()") - } - MessageRole::ToolResult => { - let name = entry.title.as_deref().unwrap_or("tool"); - truncate(&format!("<< {name}: {}", entry.content), 180) - } - _ => truncate(&entry.content, 180), - }), - } -} - -fn truncate(input: &str, limit: usize) -> String { - let trimmed = input.trim(); - if trimmed.chars().count() <= limit { - return trimmed.to_string(); - } - trimmed - .chars() - .take(limit.saturating_sub(1)) - .collect::() - + "…" -} - -fn internal_error(error: anyhow::Error) -> (StatusCode, String) { - (StatusCode::INTERNAL_SERVER_ERROR, error.to_string()) -} - pub fn dashboard_url(port: u16) -> String { SocketAddr::from(([127, 0, 0, 1], port)).to_string() } diff --git a/crates/openproof-dashboard/src/manage.rs b/crates/openproof-dashboard/src/manage.rs new file mode 100644 index 0000000..1408991 --- /dev/null +++ b/crates/openproof-dashboard/src/manage.rs @@ -0,0 +1,70 @@ +//! Session management endpoints: delete, rename, bulk delete. + +use axum::{ + extract::{Query, State}, + http::StatusCode, + Json, +}; +use std::sync::Arc; + +use crate::routes::{internal_error, SessionQuery}; +use crate::DashboardState; + +#[derive(Debug, serde::Deserialize)] +pub(crate) struct RenameRequest { + pub id: String, + pub title: String, +} + +#[derive(Debug, serde::Deserialize)] +pub(crate) struct BulkDeleteRequest { + pub ids: Vec, +} + +pub(crate) async fn delete_session( + State(state): State>, + Query(query): Query, +) -> Result, (StatusCode, String)> { + let Some(id) = query.id.as_deref() else { + return Err((StatusCode::BAD_REQUEST, "missing id parameter".to_string())); + }; + let deleted = state.store.delete_session(id).map_err(internal_error)?; + if deleted { + Ok(Json(serde_json::json!({"deleted": true}))) + } else { + Err((StatusCode::NOT_FOUND, "session not found".to_string())) + } +} + +pub(crate) async fn rename_session( + State(state): State>, + Json(body): Json, +) -> Result, (StatusCode, String)> { + let title = body.title.trim(); + if title.is_empty() { + return Err((StatusCode::BAD_REQUEST, "title cannot be empty".to_string())); + } + let updated = state + .store + .rename_session(&body.id, title) + .map_err(internal_error)?; + if updated { + Ok(Json(serde_json::json!({"updated": true}))) + } else { + Err((StatusCode::NOT_FOUND, "session not found".to_string())) + } +} + +pub(crate) async fn bulk_delete_sessions( + State(state): State>, + Json(body): Json, +) -> Result, (StatusCode, String)> { + if body.ids.is_empty() { + return Err((StatusCode::BAD_REQUEST, "ids cannot be empty".to_string())); + } + let deleted = state + .store + .delete_sessions(&body.ids) + .map_err(internal_error)?; + Ok(Json(serde_json::json!({"deleted": deleted}))) +} diff --git a/crates/openproof-dashboard/src/routes.rs b/crates/openproof-dashboard/src/routes.rs new file mode 100644 index 0000000..5fef8ca --- /dev/null +++ b/crates/openproof-dashboard/src/routes.rs @@ -0,0 +1,223 @@ +//! Read-only HTTP handlers for the dashboard. + +use axum::{ + extract::{Query, State}, + http::{header::CONTENT_TYPE, StatusCode}, + response::{Html, IntoResponse}, + Json, +}; +use openproof_lean::detect_lean_health; +use openproof_model::load_auth_summary; +use openproof_protocol::{DashboardSessionSummary, DashboardStatusResponse, HealthReport}; +use std::{process::Command, sync::Arc}; + +use crate::tex::generate_tex; +use crate::{DashboardState, APP_JS, GRAPH_JS, INDEX_HTML, SESSIONS_JS, STYLES_CSS}; + +pub(crate) fn internal_error(error: anyhow::Error) -> (StatusCode, String) { + (StatusCode::INTERNAL_SERVER_ERROR, error.to_string()) +} + +pub(crate) async fn index() -> Html<&'static str> { + Html(INDEX_HTML) +} + +pub(crate) async fn app_js() -> impl IntoResponse { + ( + [(CONTENT_TYPE, "application/javascript; charset=utf-8")], + APP_JS, + ) +} + +pub(crate) async fn styles_css() -> impl IntoResponse { + ([(CONTENT_TYPE, "text/css; charset=utf-8")], STYLES_CSS) +} + +pub(crate) async fn sessions_js() -> impl IntoResponse { + ( + [(CONTENT_TYPE, "application/javascript; charset=utf-8")], + SESSIONS_JS, + ) +} + +pub(crate) async fn graph_js() -> impl IntoResponse { + ( + [(CONTENT_TYPE, "application/javascript; charset=utf-8")], + GRAPH_JS, + ) +} + +pub(crate) async fn status( + State(state): State>, +) -> Result, (StatusCode, String)> { + let summaries = state + .store + .list_session_summaries() + .map_err(internal_error)?; + let auth = load_auth_summary().unwrap_or_default(); + let lean = detect_lean_health(&state.lean_project_dir).unwrap_or_default(); + let payload = DashboardStatusResponse { + local_db_path: state.store.db_path().display().to_string(), + auth, + lean, + session_count: summaries.len(), + active_session_id: summaries.first().map(|s| s.id.clone()), + sessions: summaries, + }; + Ok(Json(payload)) +} + +pub(crate) async fn health( + State(state): State>, +) -> Result, (StatusCode, String)> { + let latest_session = state.store.latest_session().map_err(internal_error)?; + let auth = load_auth_summary().unwrap_or_default(); + let lean = detect_lean_health(&state.lean_project_dir).unwrap_or_default(); + let payload = HealthReport { + ok: lean.ok, + local_db_path: state.store.db_path().display().to_string(), + session_count: state.store.session_count().map_err(internal_error)?, + latest_session_id: latest_session.map(|session| session.id), + auth, + lean, + }; + Ok(Json(payload)) +} + +pub(crate) async fn sessions( + State(state): State>, +) -> Result>, (StatusCode, String)> { + let summaries = state + .store + .list_session_summaries() + .map_err(internal_error)?; + Ok(Json(summaries)) +} + +#[derive(Debug, serde::Deserialize)] +pub(crate) struct SessionQuery { + pub id: Option, +} + +pub(crate) async fn session( + State(state): State>, + Query(query): Query, +) -> Result { + let session = match query.id.as_deref() { + Some(id) => state.store.get_session(id).map_err(internal_error)?, + None => state.store.latest_session().map_err(internal_error)?, + }; + match session { + Some(session) => Ok(Json(session).into_response()), + None => Ok(StatusCode::NOT_FOUND.into_response()), + } +} + +pub(crate) async fn session_summaries( + State(state): State>, +) -> Result>, (StatusCode, String)> { + let summaries = state + .store + .list_session_summaries() + .map_err(internal_error)?; + Ok(Json(summaries)) +} + +pub(crate) async fn paper_tex( + State(state): State>, + Query(query): Query, +) -> Result { + let session = match query.id.as_deref() { + Some(id) => state.store.get_session(id).map_err(internal_error)?, + None => state.store.latest_session().map_err(internal_error)?, + }; + let Some(session) = session else { + return Ok((StatusCode::NOT_FOUND, "No session").into_response()); + }; + // Read Paper.tex directly from workspace (source of truth) + let ws_dir = state.store.workspace_dir(&session.id); + let paper_file = std::fs::read_to_string(ws_dir.join("Paper.tex")).unwrap_or_default(); + let tex = if !paper_file.trim().is_empty() { + paper_file + } else { + generate_tex(&session) + }; + Ok(([(CONTENT_TYPE, "text/plain; charset=utf-8")], tex).into_response()) +} + +pub(crate) async fn paper_pdf( + State(state): State>, + Query(query): Query, +) -> Result { + let session = match query.id.as_deref() { + Some(id) => state.store.get_session(id).map_err(internal_error)?, + None => state.store.latest_session().map_err(internal_error)?, + }; + let Some(session) = session else { + return Ok((StatusCode::NOT_FOUND, "No session").into_response()); + }; + let tex = generate_tex(&session); + + // Compile in a temp directory. + let tmp = std::env::temp_dir().join("openproof-paper"); + let _ = std::fs::create_dir_all(&tmp); + let tex_path = tmp.join("paper.tex"); + std::fs::write(&tex_path, &tex).map_err(|e| internal_error(e.into()))?; + + let output = Command::new("lualatex") + .args(["-interaction=nonstopmode", "-halt-on-error", "paper.tex"]) + .current_dir(&tmp) + .output() + .map_err(|e| internal_error(anyhow::anyhow!("lualatex failed to start: {e}")))?; + + let pdf_path = tmp.join("paper.pdf"); + if !pdf_path.exists() { + let stderr = String::from_utf8_lossy(&output.stdout); + return Ok(( + StatusCode::INTERNAL_SERVER_ERROR, + format!("lualatex failed:\n{stderr}"), + ) + .into_response()); + } + + let pdf_bytes = std::fs::read(&pdf_path).map_err(|e| internal_error(e.into()))?; + Ok(([(CONTENT_TYPE, "application/pdf")], pdf_bytes).into_response()) +} + +pub(crate) async fn workspace_files( + State(state): State>, + Query(query): Query, +) -> Result { + let session = match query.id.as_deref() { + Some(id) => state.store.get_session(id).map_err(internal_error)?, + None => state.store.latest_session().map_err(internal_error)?, + }; + let Some(session) = session else { + return Ok("[]".to_string().into_response()); + }; + let ws_dir = state.store.workspace_dir(&session.id); + let mut result = String::from("["); + let mut first = true; + if let Ok(entries) = state.store.list_workspace_files(&session.id) { + 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(','); + } + first = false; + let escaped = content + .replace('\\', "\\\\") + .replace('"', "\\\"") + .replace('\n', "\\n") + .replace('\r', "\\r") + .replace('\t', "\\t"); + result.push_str(&format!( + "{{\"path\":\"{path}\",\"content\":\"{escaped}\"}}" + )); + } + } + } + result.push(']'); + Ok(([(CONTENT_TYPE, "application/json")], result).into_response()) +} diff --git a/crates/openproof-dashboard/src/tex.rs b/crates/openproof-dashboard/src/tex.rs new file mode 100644 index 0000000..3b8f9c5 --- /dev/null +++ b/crates/openproof-dashboard/src/tex.rs @@ -0,0 +1,170 @@ +//! LaTeX generation from proof session state. + +use openproof_protocol::SessionSnapshot; + +pub(crate) fn generate_tex(session: &SessionSnapshot) -> String { + let proof = &session.proof; + let title = &session.title; + + // If the model has written a LaTeX paper body, use it directly. + if !proof.paper_tex.trim().is_empty() { + // If paper_tex is already a complete document, return it as-is + if proof.paper_tex.contains("\\documentclass") { + return proof.paper_tex.clone(); + } + let mut doc = String::new(); + doc.push_str("\\documentclass[11pt]{article}\n"); + doc.push_str("\\usepackage[margin=1in]{geometry}\n"); + doc.push_str("\\usepackage{fontspec}\n"); + doc.push_str("\\usepackage{amsmath,amssymb,amsthm}\n"); + doc.push_str("\\usepackage{listings}\n"); + doc.push_str("\\usepackage{xcolor}\n"); + doc.push_str("\\lstset{basicstyle=\\ttfamily\\small,breaklines=true,frame=single,backgroundcolor=\\color{gray!10},literate=\n"); + doc.push_str(" {ℕ}{{\\ensuremath{\\mathbb{N}}}}1\n"); + doc.push_str(" {ℝ}{{\\ensuremath{\\mathbb{R}}}}1\n"); + doc.push_str(" {ℤ}{{\\ensuremath{\\mathbb{Z}}}}1\n"); + doc.push_str(" {→}{{\\ensuremath{\\to}}}1\n"); + doc.push_str(" {←}{{\\ensuremath{\\leftarrow}}}1\n"); + doc.push_str(" {∀}{{\\ensuremath{\\forall}}}1\n"); + doc.push_str(" {∃}{{\\ensuremath{\\exists}}}1\n"); + doc.push_str(" {∧}{{\\ensuremath{\\land}}}1\n"); + doc.push_str(" {∨}{{\\ensuremath{\\lor}}}1\n"); + doc.push_str(" {≤}{{\\ensuremath{\\leq}}}1\n"); + doc.push_str(" {≥}{{\\ensuremath{\\geq}}}1\n"); + doc.push_str(" {≠}{{\\ensuremath{\\neq}}}1\n"); + doc.push_str(" {∈}{{\\ensuremath{\\in}}}1\n"); + doc.push_str(" {⟨}{{\\ensuremath{\\langle}}}1\n"); + doc.push_str(" {⟩}{{\\ensuremath{\\rangle}}}1\n"); + doc.push_str(" {λ}{{\\ensuremath{\\lambda}}}1\n"); + doc.push_str(" {∑}{{\\ensuremath{\\sum}}}1\n"); + doc.push_str(" {∞}{{\\ensuremath{\\infty}}}1\n"); + doc.push_str("}\n"); + 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(&format!("\n\\title{{{}}}\n", tex_escape(title))); + doc.push_str("\\author{OpenProof}\n"); + 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 + .replace("[language=Lean]", "") + .replace("[language=lean]", "") + .replace("[language=lean4]", "") + .replace("[language=Lean4]", ""); + doc.push_str(&sanitized); + doc.push_str("\n\n\\end{document}\n"); + return doc; + } + + // Fallback: mechanical generation from proof state. + let mut doc = String::new(); + doc.push_str("\\documentclass[11pt]{article}\n"); + doc.push_str("\\usepackage[margin=1in]{geometry}\n"); + doc.push_str("\\usepackage{amsmath,amssymb,amsthm}\n"); + doc.push_str("\\usepackage{listings}\n"); + doc.push_str("\\usepackage{xcolor}\n"); + doc.push_str("\\lstset{basicstyle=\\ttfamily\\small,breaklines=true,frame=single,backgroundcolor=\\color{gray!10}}\n"); + 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('\n'); + doc.push_str(&format!("\\title{{{}}}\n", tex_escape(title))); + doc.push_str("\\author{OpenProof}\n"); + doc.push_str("\\date{\\today}\n"); + doc.push_str("\n\\begin{document}\n\\maketitle\n\n"); + + // Problem statement + if let Some(problem) = &proof.problem { + if !problem.trim().is_empty() { + doc.push_str("\\section*{Problem}\n"); + doc.push_str(&tex_escape(problem)); + doc.push_str("\n\n"); + } + } + + // Formal target + if let Some(target) = &proof.formal_target { + if !target.trim().is_empty() { + doc.push_str("\\section*{Formal Target}\n"); + doc.push_str("\\begin{lstlisting}[language={}]\n"); + doc.push_str(target); + doc.push_str("\n\\end{lstlisting}\n\n"); + } + } + + // Proof nodes + if !proof.nodes.is_empty() { + doc.push_str("\\section{Proof Structure}\n\n"); + for node in &proof.nodes { + let env = match node.kind { + openproof_protocol::ProofNodeKind::Theorem => "theorem", + openproof_protocol::ProofNodeKind::Lemma => "lemma", + _ => "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}]}" + } + _ => "", + }; + doc.push_str(&format!( + "\\begin{{{env}}}[{}]{status_marker}\n", + tex_escape(&node.label) + )); + if !node.statement.is_empty() { + doc.push_str(&tex_escape(&node.statement)); + doc.push('\n'); + } + doc.push_str(&format!("\\end{{{env}}}\n\n")); + + if !node.content.trim().is_empty() { + doc.push_str("\\begin{lstlisting}[language={}]\n"); + doc.push_str(&node.content); + doc.push_str("\n\\end{lstlisting}\n\n"); + } + } + } + + // Paper notes + if !proof.paper_notes.is_empty() { + doc.push_str("\\section{Notes}\n\n"); + doc.push_str("\\begin{itemize}\n"); + for note in &proof.paper_notes { + doc.push_str(&format!("\\item {}\n", tex_escape(note))); + } + doc.push_str("\\end{itemize}\n\n"); + } + + // Strategy summary + if let Some(strategy) = &proof.strategy_summary { + if !strategy.trim().is_empty() { + doc.push_str("\\section{Strategy}\n\n"); + doc.push_str(&tex_escape(strategy)); + doc.push_str("\n\n"); + } + } + + doc.push_str("\\end{document}\n"); + doc +} + +pub(crate) fn tex_escape(s: &str) -> String { + s.replace('\\', "\\textbackslash{}") + .replace('{', "\\{") + .replace('}', "\\}") + .replace('&', "\\&") + .replace('%', "\\%") + .replace('$', "\\$") + .replace('#', "\\#") + .replace('_', "\\_") + .replace('^', "\\^{}") + .replace('~', "\\~{}") +} diff --git a/crates/openproof-dashboard/static/app.js b/crates/openproof-dashboard/static/app.js index 7ec48b0..e68958f 100644 --- a/crates/openproof-dashboard/static/app.js +++ b/crates/openproof-dashboard/static/app.js @@ -1,10 +1,12 @@ -import React, { useEffect, useMemo, useState, useCallback } from "https://esm.sh/react@18.3.1"; +import React, { useEffect, useState, useCallback } from "https://esm.sh/react@18.3.1"; import { createRoot } from "https://esm.sh/react-dom@18.3.1/client"; import htm from "https://esm.sh/htm@3.1.1"; -import { ReactFlow, Background, Controls, MiniMap, Handle, Position } from "https://esm.sh/@xyflow/react@12.6.0?deps=react@18.3.1,react-dom@18.3.1"; +import { GraphTab } from "/graph.js"; +import { SessionSidebar } from "/sessions.js"; const h = htm.bind(React.createElement); const POLL_MS = 2000; +const STATUS_POLL_MS = 10000; // ── Helpers ───────────────────────────────────────────────────────────── @@ -30,32 +32,50 @@ function App() { const [session, setSession] = useState(null); const [tab, setTab] = useState("overview"); const [status, setStatus] = useState(null); + const [refreshKey, setRefreshKey] = useState(0); - // Poll sessions list + const triggerRefresh = useCallback(() => setRefreshKey((k) => k + 1), []); + + // Poll lightweight session summaries for the sidebar useEffect(() => { let c = false; async function poll() { try { - const r = await fetch("/api/status"); + const r = await fetch("/api/session-summaries"); const d = await r.json(); if (c) return; - setStatus(d); - setSessions(d.sessions || []); - setSelectedId((cur) => cur || d.activeSessionId || d.sessions?.[0]?.id || null); + setSessions(d || []); + setSelectedId((cur) => cur || d?.[0]?.id || null); } catch {} } poll(); const t = setInterval(poll, POLL_MS); return () => { c = true; clearInterval(t); }; + }, [refreshKey]); + + // Poll status (lean health, auth) at a lower frequency + useEffect(() => { + let c = false; + async function poll() { + try { + const r = await fetch("/api/status"); + const d = await r.json(); + if (!c) setStatus(d); + } catch {} + } + poll(); + const t = setInterval(poll, STATUS_POLL_MS); + return () => { c = true; clearInterval(t); }; }, []); - // Poll selected session + // Poll selected session detail useEffect(() => { let c = false; if (!selectedId) { setSession(null); return () => { c = true; }; } async function poll() { try { const r = await fetch(`/api/session?id=${encodeURIComponent(selectedId)}`); + if (r.status === 404) { if (!c) setSession(null); return; } const d = await r.json(); if (!c) setSession(d); } catch {} @@ -85,17 +105,11 @@ function App() {
-
-
Sessions
- ${sessions.map((s) => h` - - `)} -
+ <${SessionSidebar} + sessions=${sessions} + selectedId=${selectedId} + onSelect=${setSelectedId} + onChanged=${triggerRefresh} />
@@ -178,401 +192,7 @@ function OverviewTab({ session }) { `; } -// ── Graph Tab (React Flow) ────────────────────────────────────────────── - -const statusColor = (s) => { - const st = String(s || "").toLowerCase(); - if (st === "verified" || st === "done") return "#22c55e"; - if (st === "proving" || st === "running") return "#eab308"; - if (st === "failed" || st === "error" || st === "blocked") return "#ef4444"; - return "#525252"; -}; - -const roleColor = (r) => { - const role = String(r || "").toLowerCase(); - if (role === "prover") return "#3b82f6"; - if (role === "repairer") return "#f59e0b"; - if (role === "planner") return "#8b5cf6"; - if (role === "retriever") return "#06b6d4"; - if (role === "critic") return "#ec4899"; - return "#6b7280"; -}; - -const kindIcon = (k) => { - const kind = String(k || "").toLowerCase(); - if (kind === "theorem") return "\u{1D4AF}"; - if (kind === "lemma") return "\u{2113}"; - if (kind === "def" || kind === "artifact") return "\u{1D49F}"; - if (kind === "axiom") return "\u{1D49C}"; - return "\u25CB"; -}; - -function ProofNodeComponent({ data }) { - const borderColor = statusColor(data.status); - return h` -
- <${Handle} type="target" position=${Position.Top} style=${{ background: "#555" }} /> -
- ${kindIcon(data.kind)} - ${data.label} -
-
- ${data.kind || "node"} \u00b7 ${data.status} -
- ${data.statement ? h` -
- ${data.statement} -
- ` : null} - <${Handle} type="source" position=${Position.Bottom} style=${{ background: "#555" }} /> -
- `; -} - -function BranchNodeComponent({ data }) { - const color = roleColor(data.role); - const hasSnippet = !!(data.lean_snippet || data.leanSnippet || "").trim(); - return h` -
- <${Handle} type="target" position=${Position.Top} style=${{ background: color }} /> -
- ${data.role}${data.hidden ? " (hidden)" : ""} - ${hasSnippet ? h`\u25CF` : null} -
-
- ${String(data.status || "idle")} \u00b7 score ${(data.score || 0).toFixed(0)} \u00b7 ${data.attempt_count || data.attemptCount || 0} tries -
- ${data.summary ? h` -
- ${data.summary} -
- ` : null} -
- `; -} - -function GoalNodeComponent({ data }) { - const colors = { open: "#f59e0b", in_progress: "#3b82f6", closed: "#22c55e", failed: "#ef4444" }; - const color = colors[data.status] || "#737373"; - const failCount = (data.failed_tactics || data.failedTactics || []).length; - return h` -
- <${Handle} type="target" position=${Position.Top} style=${{ background: color }} /> -
- - ${data.status === "closed" ? "\u2713" : data.status === "failed" ? "\u2717" : "\u25CB"} goal - - ${failCount > 0 ? h` - - ${failCount} failed - - ` : null} - ${data.attempts > 0 ? h` - ${data.attempts} tried - ` : null} -
-
- ${(data.goal_text || data.goalText || "").substring(0, 60)} -
- ${data.tactic_applied || data.tacticApplied ? h` -
- via: ${data.tactic_applied || data.tacticApplied} -
- ` : null} - <${Handle} type="source" position=${Position.Bottom} style=${{ background: color }} /> -
- `; -} - -const nodeTypes = { - proofNode: ProofNodeComponent, - branchNode: BranchNodeComponent, - goalNode: GoalNodeComponent, -}; - -function GraphTab({ session }) { - const proof = session?.proof; - const proofNodes = proof?.nodes || []; - const allBranches = proof?.branches || []; - const [showBranches, setShowBranches] = useState(false); - const branches = showBranches ? allBranches : []; - - if (proofNodes.length === 0 && allBranches.length === 0) { - return h`
No proof nodes to visualize
`; - } - - // Build React Flow nodes and edges - const { flowNodes, flowEdges } = useMemo(() => { - const nodes = []; - const edges = []; - - // Layout: if nodes have parent_id, use tree layout. - // Otherwise use a 2-column grid for flat declarations. - const hasTree = proofNodes.some(n => n.parent_id || n.parentId); - - if (hasTree) { - // Tree layout by depth - const byDepth = {}; - for (const n of proofNodes) { - const d = n.depth || 0; - if (!byDepth[d]) byDepth[d] = []; - byDepth[d].push(n); - } - for (const n of proofNodes) { - const d = n.depth || 0; - const siblings = byDepth[d] || []; - const idx = siblings.indexOf(n); - const totalWidth = siblings.length * 220; - const startX = -(totalWidth / 2) + 110; - nodes.push({ - id: n.id, type: "proofNode", - position: { x: startX + idx * 220, y: d * 120 }, - draggable: true, - data: { ...n, _nodeColor: statusColor(n.status) }, - }); - } - } else { - // Grid layout for flat declarations (2 columns) - const cols = 2; - for (let i = 0; i < proofNodes.length; i++) { - const n = proofNodes[i]; - const col = i % cols; - const row = Math.floor(i / cols); - nodes.push({ - id: n.id, type: "proofNode", - position: { x: col * 280, y: row * 100 }, - draggable: true, - data: { ...n, _nodeColor: statusColor(n.status) }, - }); - } - } - - // Edges: parent edges, dependency edges, and flow edges - let prevId = null; - for (const n of proofNodes) { - const parentId = n.parent_id || n.parentId; - if (parentId) { - edges.push({ - id: "tree-" + n.id, source: parentId, target: n.id, - style: { stroke: "#3b82f6", strokeWidth: 2 }, - animated: n.status === "proving", - }); - } else if (prevId && !hasTree) { - // Flow edge for flat layouts (declaration order) - edges.push({ - id: "flow-" + n.id, source: prevId, target: n.id, - style: { stroke: "#333", strokeWidth: 1 }, - type: "smoothstep", - }); - } - prevId = n.id; - - // Dependency edges - for (const depId of (n.depends_on || n.dependsOn || [])) { - edges.push({ - id: "dep-" + n.id + "-" + depId, source: depId, - target: n.id, - style: { stroke: "#6b7280", strokeWidth: 1, strokeDasharray: "4 3" }, - }); - } - } - - // Position branches below the tree - const maxDepth = Math.max(0, ...proofNodes.map((n) => n.depth || 0)); - const branchY = (maxDepth + 1) * 100 + 40; - const branchCols = {}; - - for (const b of branches) { - const focusId = b.focus_node_id || b.focusNodeId || proofNodes[0]?.id; - if (!branchCols[focusId]) branchCols[focusId] = 0; - const col = branchCols[focusId]++; - - const parentNode = nodes.find((n) => n.id === focusId); - const baseX = parentNode ? parentNode.position.x : col * 160; - - const bId = "branch-" + b.id; - nodes.push({ - id: bId, - type: "branchNode", - position: { x: baseX + col * 160, y: branchY }, - draggable: true, - data: { ...b, _nodeColor: roleColor(b.role) }, - }); - - if (focusId) { - edges.push({ - id: "agent-" + b.id, - source: focusId, - target: bId, - style: { stroke: roleColor(b.role), strokeWidth: 1, strokeDasharray: "4 3", opacity: 0.5 }, - }); - } - } - - // Add proof goal nodes (from Pantograph proof tree) - const proofGoals = proof?.proof_goals || proof?.proofGoals || []; - const goalY = (maxDepth + 1) * 100 + (branches.length > 0 ? 180 : 40); - for (let i = 0; i < proofGoals.length; i++) { - const g = proofGoals[i]; - const gId = "goal-" + g.id; - nodes.push({ - id: gId, - type: "goalNode", - position: { x: i * 200 - (proofGoals.length * 100), y: goalY + (g.parent_goal_id || g.parentGoalId ? 80 : 0) }, - draggable: true, - data: g, - }); - // Edge from parent goal - const parentGoalId = g.parent_goal_id || g.parentGoalId; - if (parentGoalId) { - edges.push({ - id: "goaltree-" + g.id, - source: "goal-" + parentGoalId, - target: gId, - style: { stroke: "#3b82f6", strokeWidth: 1, strokeDasharray: "2 2" }, - label: g.tactic_applied || g.tacticApplied || "", - labelStyle: { fill: "#22c55e", fontSize: 8 }, - }); - } - // Edge from proof node to first-level goals - if (!parentGoalId && proofNodes.length > 0) { - const activeNodeId = proof?.active_node_id || proof?.activeNodeId || proofNodes[0]?.id; - edges.push({ - id: "nodegoal-" + g.id, - source: activeNodeId, - target: gId, - style: { stroke: "#f59e0b", strokeWidth: 1, strokeDasharray: "3 3", opacity: 0.6 }, - }); - } - } - - return { flowNodes: nodes, flowEdges: edges }; - }, [proofNodes, branches, proof]); - - // Use controlled mode: pass nodes/edges directly to ReactFlow. - // No useNodesState/useEdgesState -- avoids the state-fighting bug - // that causes nodes to flash then disappear on poll updates. - - const verification = proof?.last_verification; - const attemptNum = proof?.attempt_number || proof?.attemptNumber || 0; - - return h` -
-
- Phase: ${proof?.phase || "idle"} - \u00a0\u00b7\u00a0 Nodes: ${proofNodes.length} - \u00a0\u00b7\u00a0 Goals: ${(proof?.proof_goals || proof?.proofGoals || []).length} - \u00a0\u00b7\u00a0 Attempts: ${attemptNum} - - ${verification ? h` - \u00a0\u00b7\u00a0 - - ${verification.ok ? "Lean verified" : "Lean failed"} - - - ` : null} -
-
- <${ReactFlow} - nodes=${flowNodes} - edges=${flowEdges} - nodeTypes=${nodeTypes} - fitView - fitViewOptions=${{ padding: 0.3 }} - minZoom=${0.2} - maxZoom=${2} - defaultViewport=${{ x: 0, y: 0, zoom: 0.8 }} - proOptions=${{ hideAttribution: true }} - style=${{ background: "#0a0a0a" }} - > - <${Background} color="#222" gap=${20} /> - <${Controls} position="bottom-right" /> - <${MiniMap} - nodeColor=${(n) => n.data?._nodeColor || "#525252"} - maskColor="rgba(0,0,0,0.7)" - style=${{ background: "#111" }} - /> - -
-
- `; -} - -// ── Paper Tab ─────────────────────────────────────────────────────────── - -// Lean syntax highlighting (keywords, types, comments, strings) -const LEAN_KEYWORDS = new Set([ - "theorem", "lemma", "def", "abbrev", "instance", "class", "structure", - "where", "by", "have", "let", "show", "suffices", "calc", "match", "with", - "if", "then", "else", "do", "return", "for", "in", "open", "import", - "namespace", "end", "section", "variable", "example", "noncomputable", - "sorry", "exact", "apply", "intro", "intros", "rw", "simp", "omega", - "ring", "norm_num", "linarith", "nlinarith", "aesop", "trivial", - "constructor", "rcases", "obtain", "refine", "cases", "induction", - "contradiction", "exfalso", "push_neg", "classical", "decide", -]); -const LEAN_TYPES = new Set([ - "Prop", "Type", "Sort", "Nat", "Int", "Bool", "String", "List", "Option", - "True", "False", "And", "Or", "Not", "Iff", "Exists", "Finset", "Set", -]); - -function highlightLean(line) { - // Comment - if (line.trimStart().startsWith("--") || line.trimStart().startsWith("/-")) { - return h`${line}`; - } - // sorry gets red - if (line.includes("sorry")) { - const parts = line.split("sorry"); - const result = []; - for (let i = 0; i < parts.length; i++) { - if (i > 0) result.push(h`sorry`); - result.push(highlightTokens(parts[i])); - } - return h`${result}`; - } - return highlightTokens(line); -} - -function highlightTokens(text) { - return text.replace(/\b(\w+)\b/g, (match) => { - if (LEAN_KEYWORDS.has(match)) return `\x01kw\x02${match}\x01/kw\x02`; - if (LEAN_TYPES.has(match)) return `\x01ty\x02${match}\x01/ty\x02`; - return match; - }).split(/(\x01kw\x02[^\x01]*\x01\/kw\x02|\x01ty\x02[^\x01]*\x01\/ty\x02)/).map((part, i) => { - if (part.startsWith("\x01kw\x02")) return h`${part.slice(4, -5)}`; - if (part.startsWith("\x01ty\x02")) return h`${part.slice(4, -5)}`; - return part; - }); -} +// ── Activity Tab ──────────────────────────────────────────────────────── function ActivityTab({ session }) { const proof = session?.proof; @@ -627,6 +247,53 @@ function ActivityTab({ session }) { `; } +// ── Lean Syntax Highlighting ──────────────────────────────────────────── + +const LEAN_KEYWORDS = new Set([ + "theorem", "lemma", "def", "abbrev", "instance", "class", "structure", + "where", "by", "have", "let", "show", "suffices", "calc", "match", "with", + "if", "then", "else", "do", "return", "for", "in", "open", "import", + "namespace", "end", "section", "variable", "example", "noncomputable", + "sorry", "exact", "apply", "intro", "intros", "rw", "simp", "omega", + "ring", "norm_num", "linarith", "nlinarith", "aesop", "trivial", + "constructor", "rcases", "obtain", "refine", "cases", "induction", + "contradiction", "exfalso", "push_neg", "classical", "decide", +]); +const LEAN_TYPES = new Set([ + "Prop", "Type", "Sort", "Nat", "Int", "Bool", "String", "List", "Option", + "True", "False", "And", "Or", "Not", "Iff", "Exists", "Finset", "Set", +]); + +function highlightLean(line) { + if (line.trimStart().startsWith("--") || line.trimStart().startsWith("/-")) { + return h`${line}`; + } + if (line.includes("sorry")) { + const parts = line.split("sorry"); + const result = []; + for (let i = 0; i < parts.length; i++) { + if (i > 0) result.push(h`sorry`); + result.push(highlightTokens(parts[i])); + } + return h`${result}`; + } + return highlightTokens(line); +} + +function highlightTokens(text) { + return text.replace(/\b(\w+)\b/g, (match) => { + if (LEAN_KEYWORDS.has(match)) return `\x01kw\x02${match}\x01/kw\x02`; + if (LEAN_TYPES.has(match)) return `\x01ty\x02${match}\x01/ty\x02`; + return match; + }).split(/(\x01kw\x02[^\x01]*\x01\/kw\x02|\x01ty\x02[^\x01]*\x01\/ty\x02)/).map((part, i) => { + if (part.startsWith("\x01kw\x02")) return h`${part.slice(4, -5)}`; + if (part.startsWith("\x01ty\x02")) return h`${part.slice(4, -5)}`; + return part; + }); +} + +// ── Code Tab ──────────────────────────────────────────────────────────── + function CodeTab({ sessionId }) { const filesRef = React.useRef([]); const [filePaths, setFilePaths] = useState([]); @@ -643,13 +310,11 @@ function CodeTab({ sessionId }) { if (c) return; const f = d.files || d || []; filesRef.current = f; - // Only update file list if paths changed (avoids re-render on content-only changes) const newPaths = f.map(x => x.path).join(","); const oldPaths = filePaths.join(","); if (newPaths !== oldPaths) { setFilePaths(f.map(x => x.path)); } - // Update content for selected file without resetting scroll const sel = selected || (f.length > 0 ? f[0].path : null); if (!selected && f.length > 0) setSelected(f[0].path); const cur = f.find(x => x.path === sel); @@ -713,8 +378,10 @@ function CodeTab({ sessionId }) { `; } +// ── Paper Tab ─────────────────────────────────────────────────────────── + function PaperTab({ sessionId }) { - const [view, setView] = useState("pdf"); // "pdf" or "tex" + const [view, setView] = useState("pdf"); const [tex, setTex] = useState(""); const [pdfUrl, setPdfUrl] = useState(null); const [error, setError] = useState(""); diff --git a/crates/openproof-dashboard/static/graph.js b/crates/openproof-dashboard/static/graph.js new file mode 100644 index 0000000..0e6911f --- /dev/null +++ b/crates/openproof-dashboard/static/graph.js @@ -0,0 +1,328 @@ +import React, { useMemo, useState } from "https://esm.sh/react@18.3.1"; +import htm from "https://esm.sh/htm@3.1.1"; +import { ReactFlow, Background, Controls, MiniMap, Handle, Position } from "https://esm.sh/@xyflow/react@12.6.0?deps=react@18.3.1,react-dom@18.3.1"; + +const h = htm.bind(React.createElement); + +// ── Color helpers ────────────────────────────────────────────────────── + +const statusColor = (s) => { + const st = String(s || "").toLowerCase(); + if (st === "verified" || st === "done") return "#22c55e"; + if (st === "proving" || st === "running") return "#eab308"; + if (st === "failed" || st === "error" || st === "blocked") return "#ef4444"; + return "#525252"; +}; + +const roleColor = (r) => { + const role = String(r || "").toLowerCase(); + if (role === "prover") return "#3b82f6"; + if (role === "repairer") return "#f59e0b"; + if (role === "planner") return "#8b5cf6"; + if (role === "retriever") return "#06b6d4"; + if (role === "critic") return "#ec4899"; + return "#6b7280"; +}; + +const kindIcon = (k) => { + const kind = String(k || "").toLowerCase(); + if (kind === "theorem") return "\u{1D4AF}"; + if (kind === "lemma") return "\u{2113}"; + if (kind === "def" || kind === "artifact") return "\u{1D49F}"; + if (kind === "axiom") return "\u{1D49C}"; + return "\u25CB"; +}; + +// ── Node components ──────────────────────────────────────────────────── + +function ProofNodeComponent({ data }) { + const borderColor = statusColor(data.status); + return h` +
+ <${Handle} type="target" position=${Position.Top} style=${{ background: "#555" }} /> +
+ ${kindIcon(data.kind)} + ${data.label} +
+
+ ${data.kind || "node"} \u00b7 ${data.status} +
+ ${data.statement ? h` +
+ ${data.statement} +
+ ` : null} + <${Handle} type="source" position=${Position.Bottom} style=${{ background: "#555" }} /> +
+ `; +} + +function BranchNodeComponent({ data }) { + const color = roleColor(data.role); + const hasSnippet = !!(data.lean_snippet || data.leanSnippet || "").trim(); + return h` +
+ <${Handle} type="target" position=${Position.Top} style=${{ background: color }} /> +
+ ${data.role}${data.hidden ? " (hidden)" : ""} + ${hasSnippet ? h`\u25CF` : null} +
+
+ ${String(data.status || "idle")} \u00b7 score ${(data.score || 0).toFixed(0)} \u00b7 ${data.attempt_count || data.attemptCount || 0} tries +
+ ${data.summary ? h` +
+ ${data.summary} +
+ ` : null} +
+ `; +} + +function GoalNodeComponent({ data }) { + const colors = { open: "#f59e0b", in_progress: "#3b82f6", closed: "#22c55e", failed: "#ef4444" }; + const color = colors[data.status] || "#737373"; + const failCount = (data.failed_tactics || data.failedTactics || []).length; + return h` +
+ <${Handle} type="target" position=${Position.Top} style=${{ background: color }} /> +
+ + ${data.status === "closed" ? "\u2713" : data.status === "failed" ? "\u2717" : "\u25CB"} goal + + ${failCount > 0 ? h` + + ${failCount} failed + + ` : null} + ${data.attempts > 0 ? h` + ${data.attempts} tried + ` : null} +
+
+ ${(data.goal_text || data.goalText || "").substring(0, 60)} +
+ ${data.tactic_applied || data.tacticApplied ? h` +
+ via: ${data.tactic_applied || data.tacticApplied} +
+ ` : null} + <${Handle} type="source" position=${Position.Bottom} style=${{ background: color }} /> +
+ `; +} + +const nodeTypes = { + proofNode: ProofNodeComponent, + branchNode: BranchNodeComponent, + goalNode: GoalNodeComponent, +}; + +// ── GraphTab ─────────────────────────────────────────────────────────── + +export function GraphTab({ session }) { + const proof = session?.proof; + const proofNodes = proof?.nodes || []; + const allBranches = proof?.branches || []; + const [showBranches, setShowBranches] = useState(false); + const branches = showBranches ? allBranches : []; + + if (proofNodes.length === 0 && allBranches.length === 0) { + return h`
No proof nodes to visualize
`; + } + + const { flowNodes, flowEdges } = useMemo(() => { + const nodes = []; + const edges = []; + const hasTree = proofNodes.some(n => n.parent_id || n.parentId); + + if (hasTree) { + const byDepth = {}; + for (const n of proofNodes) { + const d = n.depth || 0; + if (!byDepth[d]) byDepth[d] = []; + byDepth[d].push(n); + } + for (const n of proofNodes) { + const d = n.depth || 0; + const siblings = byDepth[d] || []; + const idx = siblings.indexOf(n); + const totalWidth = siblings.length * 220; + const startX = -(totalWidth / 2) + 110; + nodes.push({ + id: n.id, type: "proofNode", + position: { x: startX + idx * 220, y: d * 120 }, + draggable: true, + data: { ...n, _nodeColor: statusColor(n.status) }, + }); + } + } else { + const cols = 2; + for (let i = 0; i < proofNodes.length; i++) { + const n = proofNodes[i]; + const col = i % cols; + const row = Math.floor(i / cols); + nodes.push({ + id: n.id, type: "proofNode", + position: { x: col * 280, y: row * 100 }, + draggable: true, + data: { ...n, _nodeColor: statusColor(n.status) }, + }); + } + } + + let prevId = null; + for (const n of proofNodes) { + const parentId = n.parent_id || n.parentId; + if (parentId) { + edges.push({ + id: "tree-" + n.id, source: parentId, target: n.id, + style: { stroke: "#3b82f6", strokeWidth: 2 }, + animated: n.status === "proving", + }); + } else if (prevId && !hasTree) { + edges.push({ + id: "flow-" + n.id, source: prevId, target: n.id, + style: { stroke: "#333", strokeWidth: 1 }, + type: "smoothstep", + }); + } + prevId = n.id; + + for (const depId of (n.depends_on || n.dependsOn || [])) { + edges.push({ + id: "dep-" + n.id + "-" + depId, source: depId, + target: n.id, + style: { stroke: "#6b7280", strokeWidth: 1, strokeDasharray: "4 3" }, + }); + } + } + + const maxDepth = Math.max(0, ...proofNodes.map((n) => n.depth || 0)); + const branchY = (maxDepth + 1) * 100 + 40; + const branchCols = {}; + + for (const b of branches) { + const focusId = b.focus_node_id || b.focusNodeId || proofNodes[0]?.id; + if (!branchCols[focusId]) branchCols[focusId] = 0; + const col = branchCols[focusId]++; + const parentNode = nodes.find((n) => n.id === focusId); + const baseX = parentNode ? parentNode.position.x : col * 160; + const bId = "branch-" + b.id; + nodes.push({ + id: bId, type: "branchNode", + position: { x: baseX + col * 160, y: branchY }, + draggable: true, + data: { ...b, _nodeColor: roleColor(b.role) }, + }); + if (focusId) { + edges.push({ + id: "agent-" + b.id, source: focusId, target: bId, + style: { stroke: roleColor(b.role), strokeWidth: 1, strokeDasharray: "4 3", opacity: 0.5 }, + }); + } + } + + const proofGoals = proof?.proof_goals || proof?.proofGoals || []; + const goalY = (maxDepth + 1) * 100 + (branches.length > 0 ? 180 : 40); + for (let i = 0; i < proofGoals.length; i++) { + const g = proofGoals[i]; + const gId = "goal-" + g.id; + nodes.push({ + id: gId, type: "goalNode", + position: { x: i * 200 - (proofGoals.length * 100), y: goalY + (g.parent_goal_id || g.parentGoalId ? 80 : 0) }, + draggable: true, data: g, + }); + const parentGoalId = g.parent_goal_id || g.parentGoalId; + if (parentGoalId) { + edges.push({ + id: "goaltree-" + g.id, source: "goal-" + parentGoalId, target: gId, + style: { stroke: "#3b82f6", strokeWidth: 1, strokeDasharray: "2 2" }, + label: g.tactic_applied || g.tacticApplied || "", + labelStyle: { fill: "#22c55e", fontSize: 8 }, + }); + } + if (!parentGoalId && proofNodes.length > 0) { + const activeNodeId = proof?.active_node_id || proof?.activeNodeId || proofNodes[0]?.id; + edges.push({ + id: "nodegoal-" + g.id, source: activeNodeId, target: gId, + style: { stroke: "#f59e0b", strokeWidth: 1, strokeDasharray: "3 3", opacity: 0.6 }, + }); + } + } + + return { flowNodes: nodes, flowEdges: edges }; + }, [proofNodes, branches, proof]); + + const verification = proof?.last_verification; + const attemptNum = proof?.attempt_number || proof?.attemptNumber || 0; + + return h` +
+
+ Phase: ${proof?.phase || "idle"} + \u00a0\u00b7\u00a0 Nodes: ${proofNodes.length} + \u00a0\u00b7\u00a0 Goals: ${(proof?.proof_goals || proof?.proofGoals || []).length} + \u00a0\u00b7\u00a0 Attempts: ${attemptNum} + + ${verification ? h` + \u00a0\u00b7\u00a0 + + ${verification.ok ? "Lean verified" : "Lean failed"} + + + ` : null} +
+
+ <${ReactFlow} + nodes=${flowNodes} + edges=${flowEdges} + nodeTypes=${nodeTypes} + fitView + fitViewOptions=${{ padding: 0.3 }} + minZoom=${0.2} + maxZoom=${2} + defaultViewport=${{ x: 0, y: 0, zoom: 0.8 }} + proOptions=${{ hideAttribution: true }} + style=${{ background: "#0a0a0a" }} + > + <${Background} color="#222" gap=${20} /> + <${Controls} position="bottom-right" /> + <${MiniMap} + nodeColor=${(n) => n.data?._nodeColor || "#525252"} + maskColor="rgba(0,0,0,0.7)" + style=${{ background: "#111" }} + /> + +
+
+ `; +} diff --git a/crates/openproof-dashboard/static/sessions.js b/crates/openproof-dashboard/static/sessions.js new file mode 100644 index 0000000..1c6e2f9 --- /dev/null +++ b/crates/openproof-dashboard/static/sessions.js @@ -0,0 +1,177 @@ +import React, { useState, useCallback } from "https://esm.sh/react@18.3.1"; +import htm from "https://esm.sh/htm@3.1.1"; + +const h = htm.bind(React.createElement); + +export function SessionSidebar({ sessions, selectedId, onSelect, onChanged }) { + const [managing, setManaging] = useState(false); + const [checked, setChecked] = useState(new Set()); + const [editingId, setEditingId] = useState(null); + const [editTitle, setEditTitle] = useState(""); + const [confirmDelete, setConfirmDelete] = useState(null); // null | {type, ids} + + const toggleCheck = useCallback((id) => { + setChecked((prev) => { + const next = new Set(prev); + if (next.has(id)) next.delete(id); + else next.add(id); + return next; + }); + }, []); + + const toggleAll = useCallback(() => { + setChecked((prev) => { + if (prev.size === sessions.length) return new Set(); + return new Set(sessions.map((s) => s.id)); + }); + }, [sessions]); + + const startRename = useCallback((id, title) => { + setEditingId(id); + setEditTitle(title); + }, []); + + const commitRename = useCallback(async () => { + if (!editingId || !editTitle.trim()) return; + try { + await fetch("/api/session", { + method: "PATCH", + headers: { "Content-Type": "application/json" }, + body: JSON.stringify({ id: editingId, title: editTitle.trim() }), + }); + onChanged(); + } catch {} + setEditingId(null); + setEditTitle(""); + }, [editingId, editTitle, onChanged]); + + const cancelRename = useCallback(() => { + setEditingId(null); + setEditTitle(""); + }, []); + + const requestDelete = useCallback((ids) => { + setConfirmDelete({ ids }); + }, []); + + const executeDelete = useCallback(async () => { + if (!confirmDelete) return; + const { ids } = confirmDelete; + try { + if (ids.length === 1) { + await fetch(`/api/session?id=${encodeURIComponent(ids[0])}`, { method: "DELETE" }); + } else { + await fetch("/api/sessions/bulk-delete", { + method: "POST", + headers: { "Content-Type": "application/json" }, + body: JSON.stringify({ ids }), + }); + } + // If we deleted the selected session, clear selection + if (ids.includes(selectedId)) { + const remaining = sessions.filter((s) => !ids.includes(s.id)); + onSelect(remaining[0]?.id || null); + } + setChecked((prev) => { + const next = new Set(prev); + for (const id of ids) next.delete(id); + return next; + }); + onChanged(); + } catch {} + setConfirmDelete(null); + }, [confirmDelete, sessions, selectedId, onSelect, onChanged]); + + const checkedCount = checked.size; + + return h` +
+
+ Sessions + +
+ + ${managing && sessions.length > 0 ? h` +
+ + ${checkedCount > 0 ? h` + + ` : null} + ${checkedCount > 0 ? h` + ${checkedCount} selected + ` : null} +
+ ` : null} + + ${confirmDelete ? h` +
+
Delete ${confirmDelete.ids.length} session${confirmDelete.ids.length > 1 ? "s" : ""}?
+
This cannot be undone.
+
+ + +
+
+ ` : null} + +
+ ${sessions.map((s) => h` +
+ ${managing ? h` + toggleCheck(s.id)} /> + ` : null} +
editingId !== s.id && onSelect(s.id)}> + ${editingId === s.id ? h` + setEditTitle(e.target.value)} + onKeyDown=${(e) => { + if (e.key === "Enter") commitRename(); + if (e.key === "Escape") cancelRename(); + }} + onClick=${(e) => e.stopPropagation()} + ref=${(el) => el && el.focus()} /> + ` : h` + ${s.title} + `} + ${s.transcriptEntries || 0} entries \u00b7 ${s.proofNodes || 0} nodes +
+ ${managing && editingId !== s.id ? h` +
+ + +
+ ` : null} + ${editingId === s.id ? h` +
+ + +
+ ` : null} +
+ `)} +
+
+ `; +} diff --git a/crates/openproof-dashboard/static/styles.css b/crates/openproof-dashboard/static/styles.css index 29a6628..1dd1bba 100644 --- a/crates/openproof-dashboard/static/styles.css +++ b/crates/openproof-dashboard/static/styles.css @@ -254,12 +254,19 @@ body { /* Session picker (sidebar) */ .layout { display: flex; height: calc(100% - 40px - 34px); } .sidebar { - width: 220px; + width: 260px; border-right: 1px solid var(--border); background: var(--surface); - overflow: auto; + display: flex; + flex-direction: column; flex-shrink: 0; } +.sidebar-header { + display: flex; + align-items: center; + border-bottom: 1px solid var(--border); + padding-right: 8px; +} .sidebar-title { padding: 8px 12px; font-size: 11px; @@ -269,11 +276,16 @@ body { color: var(--muted); border-bottom: 1px solid var(--border); } +.session-list { + flex: 1; + overflow: auto; +} .session-item { - display: block; + display: flex; + align-items: center; width: 100%; text-align: left; - padding: 8px 12px; + padding: 0; border: none; background: none; color: var(--text); @@ -283,8 +295,85 @@ body { } .session-item:hover { background: var(--surface-2); } .session-item-active { background: var(--surface-2); border-left: 2px solid var(--accent); } -.session-item strong { display: block; font-size: 12px; margin-bottom: 2px; } +.session-item-body { + flex: 1; + min-width: 0; + padding: 8px 12px; + cursor: pointer; +} +.session-item strong { display: block; font-size: 12px; margin-bottom: 2px; overflow: hidden; text-overflow: ellipsis; white-space: nowrap; } .session-item small { color: var(--muted); font-size: 11px; } +.session-item-actions { + display: flex; + gap: 2px; + padding-right: 6px; + flex-shrink: 0; +} + +/* Session management controls */ +.session-check { margin: 0 0 0 10px; flex-shrink: 0; cursor: pointer; accent-color: var(--accent); } +.session-toolbar { + display: flex; + align-items: center; + gap: 8px; + padding: 6px 12px; + border-bottom: 1px solid var(--border); + background: var(--surface-2); + font-size: 11px; +} +.session-check-label { display: flex; align-items: center; gap: 4px; cursor: pointer; color: var(--muted); font-size: 11px; } +.session-check-label input { accent-color: var(--accent); cursor: pointer; } +.session-toolbar-count { color: var(--muted); margin-left: auto; } +.session-edit-input { + width: 100%; + padding: 3px 6px; + font-size: 12px; + font-family: var(--sans); + background: var(--bg); + color: var(--text); + border: 1px solid var(--accent); + border-radius: 3px; + outline: none; +} + +/* Buttons */ +.btn-small { + padding: 3px 8px; + font-size: 10px; + font-weight: 500; + border: 1px solid var(--border); + border-radius: 3px; + background: var(--surface-2); + color: var(--text); + cursor: pointer; +} +.btn-small:hover { background: var(--border); } +.btn-manage { font-size: 10px; } +.btn-danger { background: #450a0a; border-color: #7f1d1d; color: var(--red); } +.btn-danger:hover { background: #7f1d1d; } +.btn-icon { + background: none; + border: none; + color: var(--muted); + cursor: pointer; + font-size: 12px; + padding: 2px 4px; + border-radius: 3px; +} +.btn-icon:hover { background: var(--surface-2); color: var(--text); } +.btn-icon-danger:hover { color: var(--red); } + +/* Delete confirmation */ +.delete-confirm { + padding: 10px 12px; + border-bottom: 1px solid var(--border); + background: #1a0a0a; + font-size: 12px; + color: var(--text); +} +.delete-confirm-sub { color: var(--muted); font-size: 11px; margin-top: 2px; } +.delete-confirm-actions { display: flex; gap: 6px; margin-top: 8px; } + .main-area { flex: 1; min-width: 0; display: flex; flex-direction: column; } /* Empty state */ diff --git a/crates/openproof-store/src/sessions.rs b/crates/openproof-store/src/sessions.rs index 555d5e9..38be8c3 100644 --- a/crates/openproof-store/src/sessions.rs +++ b/crates/openproof-store/src/sessions.rs @@ -1,6 +1,8 @@ use anyhow::{Context, Result}; use chrono::Utc; -use openproof_protocol::{CloudPolicy, ProofSessionState, SessionSnapshot, TranscriptEntry}; +use openproof_protocol::{ + CloudPolicy, DashboardSessionSummary, ProofSessionState, SessionSnapshot, TranscriptEntry, +}; use rusqlite::{params, Connection}; use serde_json::Value; use std::fs; @@ -78,6 +80,114 @@ impl AppStore { self.upsert_session(&conn, session) } + /// Lightweight session listing that avoids deserializing JSON blobs. + /// Uses SQLite json functions to compute counts at the database level. + pub fn list_session_summaries(&self) -> Result> { + let conn = self.connect()?; + let mut stmt = conn.prepare( + r#" + SELECT id, title, updated_at, workspace_label, + json_array_length(transcript_json) AS transcript_entries, + json_array_length(json_extract(proof_json, '$.nodes')) AS proof_nodes + FROM sessions + ORDER BY updated_at DESC + "#, + )?; + let rows = stmt.query_map([], |row| { + Ok(DashboardSessionSummary { + id: row.get(0)?, + title: row.get(1)?, + updated_at: row.get(2)?, + workspace_label: row.get(3)?, + transcript_entries: row.get::<_, i64>(4).unwrap_or(0).max(0) as usize, + proof_nodes: row.get::<_, i64>(5).unwrap_or(0).max(0) as usize, + active_node_label: None, + proof_phase: None, + last_role: None, + last_excerpt: None, + }) + })?; + let mut summaries = Vec::new(); + for row in rows { + summaries.push(row?); + } + Ok(summaries) + } + + pub fn delete_session(&self, session_id: &str) -> Result { + let conn = self.connect()?; + let deleted = conn.execute("DELETE FROM sessions WHERE id = ?", params![session_id])?; + if deleted > 0 { + let _ = conn.execute( + "DELETE FROM verification_runs WHERE session_id = ?", + params![session_id], + ); + let _ = conn.execute( + "DELETE FROM attempt_logs WHERE session_id = ?", + params![session_id], + ); + let _ = conn.execute( + "DELETE FROM sync_queue WHERE session_id = ?", + params![session_id], + ); + let ws_dir = self.workspace_dir(session_id); + if ws_dir.exists() { + let _ = fs::remove_dir_all(&ws_dir); + } + Ok(true) + } else { + Ok(false) + } + } + + pub fn delete_sessions(&self, session_ids: &[String]) -> Result { + if session_ids.is_empty() { + return Ok(0); + } + let conn = self.connect()?; + let tx = conn.unchecked_transaction()?; + let placeholders: Vec<&str> = session_ids.iter().map(|_| "?").collect(); + let in_clause = placeholders.join(","); + let params: Vec<&dyn rusqlite::ToSql> = session_ids + .iter() + .map(|id| id as &dyn rusqlite::ToSql) + .collect(); + let deleted = tx.execute( + &format!("DELETE FROM sessions WHERE id IN ({in_clause})"), + params.as_slice(), + )?; + let _ = tx.execute( + &format!("DELETE FROM verification_runs WHERE session_id IN ({in_clause})"), + params.as_slice(), + ); + let _ = tx.execute( + &format!("DELETE FROM attempt_logs WHERE session_id IN ({in_clause})"), + params.as_slice(), + ); + let _ = tx.execute( + &format!("DELETE FROM sync_queue WHERE session_id IN ({in_clause})"), + params.as_slice(), + ); + tx.commit()?; + for id in session_ids { + let ws_dir = self.workspace_dir(id); + if ws_dir.exists() { + let _ = fs::remove_dir_all(&ws_dir); + } + } + Ok(deleted) + } + + pub fn rename_session(&self, session_id: &str, new_title: &str) -> Result { + let conn = self.connect()?; + let now = Utc::now().to_rfc3339(); + let updated = conn.execute( + "UPDATE sessions SET title = ?, updated_at = ? WHERE id = ?", + params![new_title, now, session_id], + )?; + Ok(updated > 0) + } + pub fn import_legacy_sessions(&self) -> Result { let mut summary = openproof_protocol::LegacyImportSummary::default(); if !self.paths.legacy_sessions_dir.exists() {