feat(cli): add tactic-search --file for batch data generation

crates/openproof-cli/src/autonomous.rs

@@ -1294,6 +1294,46 @@ pub async fn run_tactic_search_once(session_id: String) -> Result<()> {
     Ok(())
 }
 
+/// Run tactic search on a standalone Lean file (no session needed).
+/// Creates a temporary workspace and session, runs search, exports verified data.
+pub async fn run_tactic_search_file(file_path: String) -> Result<()> {
+    let content = fs::read_to_string(&file_path).with_context(|| format!("reading {file_path}"))?;
+
+    let sorry_count = openproof_lean::find_sorry_positions(&content).len();
+    anyhow::ensure!(sorry_count > 0, "No sorrys found in {file_path}");
+
+    let store = AppStore::open(StorePaths::detect()?)?;
+
+    // Create a minimal session via the store's own API
+    let session_id = format!("expert_file_{}", chrono::Utc::now().timestamp_millis());
+
+    // Write the lean file to a workspace directory the store can find
+    let workspace_dir = store.workspace_dir(&session_id);
+    fs::create_dir_all(&workspace_dir)?;
+    fs::write(workspace_dir.join("Main.lean"), &content)?;
+
+    // Build a session snapshot with just enough for tactic search
+    let mut node = openproof_protocol::ProofNode::default();
+    node.id = "root".to_string();
+    node.content = content.clone();
+    node.status = openproof_protocol::ProofNodeStatus::Pending;
+    let mut proof = openproof_protocol::ProofSessionState::default();
+    proof.nodes.push(node);
+    proof.active_node_id = Some("root".to_string());
+
+    let session = openproof_protocol::SessionSnapshot {
+        id: session_id.clone(),
+        title: file_path.clone(),
+        proof,
+        ..Default::default()
+    };
+    store.save_session(&session)?;
+
+    eprintln!("[tactic-search] File: {file_path}, {sorry_count} sorry(s), session: {session_id}");
+
+    run_tactic_search_once(session_id).await
+}
+
 fn tactic_proposer_backend(config: Option<&crate::setup::SetupResult>) -> TacticProposerBackend {
     if let Ok(value) = std::env::var("OPENPROOF_TACTIC_PROPOSER") {
         let normalized = value.trim().to_ascii_lowercase();

crates/openproof-cli/src/main.rs

@@ -29,7 +29,8 @@ enum Command {
         prompt: String,
     },
     TacticSearch {
-        resume: String,
+        resume: Option<String>,
+        file: Option<String>,
     },
     Run {
         problem: String,
@@ -61,7 +62,15 @@ 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::TacticSearch { resume } => autonomous::run_tactic_search_once(resume).await,
+        Command::TacticSearch { resume, file } => {
+            if let Some(file_path) = file {
+                autonomous::run_tactic_search_file(file_path).await
+            } else if let Some(session_id) = resume {
+                autonomous::run_tactic_search_once(session_id).await
+            } else {
+                bail!("tactic-search requires --resume <session_id> or --file <path.lean>")
+            }
+        }
         Command::Run {
             problem,
             label,
@@ -223,22 +232,27 @@ fn parse_args(args: Vec<String>) -> Result<CliOptions> {
 
     if args.first().map(String::as_str) == Some("tactic-search") {
         let mut resume = None;
+        let mut file = None;
         let mut index = 1;
         while index < args.len() {
             match args[index].as_str() {
                 "--resume" => {
                     index += 1;
                     resume = args.get(index).cloned();
                 }
+                "--file" => {
+                    index += 1;
+                    file = args.get(index).cloned();
+                }
                 unexpected => bail!("unknown tactic-search argument: {unexpected}"),
             }
             index += 1;
         }
-        let Some(resume) = resume else {
-            bail!("openproof tactic-search requires --resume <session_id>");
-        };
+        if resume.is_none() && file.is_none() {
+            bail!("openproof tactic-search requires --resume <session_id> or --file <path.lean>");
+        }
         return Ok(CliOptions {
-            command: Command::TacticSearch { resume },
+            command: Command::TacticSearch { resume, file },
             launch_cwd,
         });
     }