1use std::collections::HashMap;
9use std::panic::{self, AssertUnwindSafe};
10use std::path::Path;
11use std::time::{Duration, Instant};
12
13use serde_json::{json, Value};
14
15use crate::args_parser::WrapperOptions;
16use crate::args_parser_queries::active_query_modes;
17use crate::execution_store::{ExecutionRecord, ExecutionRecordOptions, ExecutionStore};
18use crate::formal_ai::{run_formal_ai_task, Outcome, TaskOptions};
19use crate::formal_ai_client::{CompletionClient, HttpClient};
20use crate::formal_ai_policy::{resolve_bounds_with, EXIT_CONFIG, EXIT_UNAVAILABLE, EXIT_USAGE};
21use crate::formal_ai_runtime::{describe_identity, start_runtime};
22use crate::isolation::{append_log_file, get_timestamp};
23use crate::launch_identity::{
24 apply_launch, claim_launch, direct_execution_env, write_launch_log, ClaimError, LaunchPlan,
25};
26use crate::output_blocks::{
27 create_finish_block, create_start_block, FinishBlockOptions, StartBlockOptions,
28};
29use crate::signal_handler::{get_signal_exit_code, set_deferred_signals, was_signal_received};
30
31pub const EVIDENCE_SCHEMA: &str = "start-formal-ai-evidence/1";
32const PREFIX: &str = "[formal-ai]";
33
34pub fn validate_options(options: &WrapperOptions) -> Result<(), String> {
37 if !options.use_formal_ai {
38 return Ok(());
39 }
40 let mut conflicts: Vec<&str> = Vec::new();
41 if options.isolated.is_some() {
42 conflicts.push("--isolated");
43 }
44 if options.user {
45 conflicts.push("--isolated-user");
46 }
47 if options.detached {
48 conflicts.push("--detached");
49 }
50 if options.use_command_stream {
51 conflicts.push("--use-command-stream");
52 }
53 conflicts.extend(active_query_modes(options));
54 if conflicts.is_empty() {
55 Ok(())
56 } else {
57 Err(format!(
58 "--use-formal-ai cannot be combined with {} (experimental mode, see docs/formal-ai.md)",
59 conflicts.join(", ")
60 ))
61 }
62}
63
64pub fn request_text(raw_command: &[String]) -> String {
67 raw_command.join(" ").trim().to_string()
68}
69
70pub fn prefix_lines(text: &str) -> String {
72 text.split('\n')
73 .map(|line| {
74 format!("{} {}", PREFIX, line)
75 .trim_end_matches(' ')
76 .to_string()
77 })
78 .collect::<Vec<_>>()
79 .join("\n")
80}
81
82fn note(text: &str) {
83 eprintln!("{}", prefix_lines(text));
84}
85
86pub struct CliOptions<'a> {
88 pub request: &'a str,
89 pub session_id: &'a str,
90 pub launch: &'a LaunchPlan,
91 pub store: Option<&'a ExecutionStore>,
92 pub verbose: bool,
93 pub cwd: &'a Path,
94 pub get_env: &'a dyn Fn(&str) -> Option<String>,
95}
96
97pub fn run_formal_ai_cli(options: &CliOptions<'_>) -> i32 {
99 let request = options.request;
100 let session_id = options.session_id;
101 let bounds = match resolve_bounds_with(options.get_env) {
102 Ok(bounds) => bounds,
103 Err(message) => {
104 note(&format!("Error: {}", message));
105 return EXIT_CONFIG;
106 }
107 };
108 if request.is_empty() {
109 note("Error: --use-formal-ai needs a request after --");
110 return EXIT_USAGE;
111 }
112 let length = request.encode_utf16().count() as u64;
114 if length > bounds.max_request_chars {
115 note(&format!(
116 "Error: the request has {} characters; START_FORMAL_AI_MAX_REQUEST_CHARS is {}",
117 length, bounds.max_request_chars
118 ));
119 return EXIT_USAGE;
120 }
121 set_deferred_signals(true);
124 let cancel_code = || was_signal_received().then(get_signal_exit_code);
125 let deadline = Instant::now() + Duration::from_millis(bounds.timeout_ms);
126 let mut runtime = match start_runtime(options.get_env, &bounds, &was_signal_received) {
127 Ok(runtime) => runtime,
128 Err(message) => {
129 note(&format!("Error: {}", message));
130 note("No command was run: --use-formal-ai never falls back to aliases, a shell or an LLM.");
131 return cancel_code().unwrap_or(EXIT_UNAVAILABLE);
132 }
133 };
134 let identity = describe_identity(&runtime.identity);
135 note(&format!("runtime: {}", identity));
136 note(&format!("effects: {}", bounds.effects));
137
138 let cwd_text = options.cwd.to_string_lossy().to_string();
139 let log_path = options.launch.log_path.clone();
140 let start_time = get_timestamp();
141 let started = Instant::now();
142 let mut record = options.store.map(|_| {
143 let mut extra = HashMap::new();
144 extra.insert(
145 "formalAi".to_string(),
146 json!({
147 "request": request,
148 "effects": bounds.effects,
149 "runtime": runtime.identity.to_json(),
150 }),
151 );
152 ExecutionRecord::with_options(ExecutionRecordOptions {
153 uuid: Some(session_id.to_string()),
154 command: request.to_string(),
155 log_path: Some(log_path.to_string_lossy().to_string()),
156 pid: Some(std::process::id()),
157 shell: Some("formal-ai".to_string()),
158 working_directory: Some(cwd_text.clone()),
159 options: Some(extra),
160 ..Default::default()
161 })
162 });
163 if let (Some(record), Some(store)) = (record.as_mut(), options.store) {
164 apply_launch(record, options.launch);
165 if let Err(error) = claim_launch(store, record, options.launch) {
166 match error {
167 ClaimError::Refused(message) => {
168 note(&format!("Error: {}", message));
169 return 1;
170 }
171 ClaimError::Store(message) => {
172 if options.verbose {
173 note(&format!(
174 "[ExecutionStore] Warning: Failed to save initial record: {}",
175 message
176 ));
177 }
178 }
179 }
180 }
181 }
182 let header = [
183 "=== Start Command Log ===".to_string(),
184 format!("Timestamp: {}", start_time),
185 format!("Session ID: {}", session_id),
186 "Mode: --use-formal-ai (experimental)".to_string(),
187 format!("Request: {}", request),
188 format!("Formal AI: {}", identity),
189 format!("Effects: {}", bounds.effects),
190 format!("Platform: {}", std::env::consts::OS),
191 format!("Working Directory: {}", cwd_text),
192 "=".repeat(50),
193 String::new(),
194 String::new(),
195 ]
196 .join("\n");
197 write_launch_log(&log_path, &header, options.launch, record.as_ref());
198
199 let command = format!("--use-formal-ai -- {}", request);
200 println!(
201 "{}",
202 create_start_block(&StartBlockOptions {
203 session_id,
204 timestamp: &start_time,
205 command: &command,
206 extra_lines: None,
207 style: None,
208 width: None,
209 defer_command: false,
210 })
211 );
212 println!();
213
214 let mut evidence = json!({
215 "schema": EVIDENCE_SCHEMA,
216 "sessionId": session_id,
217 "runtime": runtime.identity.to_json(),
218 });
219 let env = direct_execution_env(session_id, options.launch);
220 let task_note = |text: &str| {
221 note(text);
222 append_log_file(&log_path, &format!("{} {}\n", PREFIX, text));
223 };
224 let mut client = HttpClient::new(&runtime.base_url, bounds.max_retries, deadline);
225 let task = panic::catch_unwind(AssertUnwindSafe(|| {
226 run_formal_ai_task(
227 &TaskOptions {
228 request,
229 cwd: options.cwd,
230 env: &env,
231 bounds: &bounds,
232 deadline,
233 mirror: true,
234 note: &task_note,
235 cancel: &cancel_code,
236 },
237 &mut client,
238 &mut evidence,
239 )
240 }));
241 let outcome = match task {
242 Ok(outcome) => {
243 evidence["formalAiRequests"] = json!(client.requests());
244 outcome
245 }
246 Err(payload) => {
247 let message = payload
248 .downcast_ref::<String>()
249 .cloned()
250 .or_else(|| payload.downcast_ref::<&str>().map(|s| s.to_string()))
251 .unwrap_or_else(|| "internal error".to_string());
252 let outcome = Outcome::new(
253 "internal-error",
254 1,
255 message,
256 &["start failed; the task state is unknown"],
257 );
258 evidence["outcome"] = outcome.to_json();
259 outcome
260 }
261 };
262 runtime.stop();
263 note(&format!("{}: {}", outcome.status, outcome.message));
264 for obligation in &outcome.remaining {
265 note(&format!("remaining: {}", obligation));
266 }
267 let duration_ms = started.elapsed().as_secs_f64() * 1000.0;
268 evidence["durationMs"] = json!(duration_ms.round() as u64);
269 let end_time = get_timestamp();
270 let pretty = serde_json::to_string_pretty(&evidence).unwrap_or_else(|_| evidence.to_string());
271 append_log_file(
272 &log_path,
273 &format!(
274 "\n=== Formal AI Evidence ===\n{}\n\n{}\nFinished: {}\nExit Code: {}\n",
275 pretty,
276 "=".repeat(50),
277 end_time,
278 outcome.exit_code
279 ),
280 );
281 if let (Some(mut record), Some(store)) = (record, options.store) {
282 if let Some(Value::Object(formal_ai)) = record.options.get_mut("formalAi") {
283 formal_ai.insert("outcome".to_string(), json!(outcome.status));
284 }
285 record.complete(outcome.exit_code);
286 if let Err(error) = store.save(&record) {
287 if options.verbose {
288 note(&format!(
289 "[Tracking] Warning: Could not save execution record: {}",
290 error
291 ));
292 }
293 }
294 }
295 println!();
296 println!(
297 "{}",
298 create_finish_block(&FinishBlockOptions {
299 session_id,
300 timestamp: &end_time,
301 exit_code: outcome.exit_code,
302 log_path: &log_path.to_string_lossy(),
303 duration_ms: Some(duration_ms),
304 result_message: None,
305 extra_lines: None,
306 style: None,
307 width: None,
308 })
309 );
310 outcome.exit_code
311}
312
313#[cfg(test)]
314mod tests {
315 use super::*;
316
317 #[test]
318 fn request_text_joins_the_argv_after_the_separator() {
319 let argv: Vec<String> = ["print", "list", "of", "files", ""]
320 .iter()
321 .map(|s| s.to_string())
322 .collect();
323 assert_eq!(request_text(&argv), "print list of files");
324 assert_eq!(request_text(&[]), "");
325 }
326
327 #[test]
328 fn notes_are_prefixed_per_line_without_trailing_spaces() {
329 assert_eq!(
330 prefix_lines("a\n\nb "),
331 "[formal-ai] a\n[formal-ai]\n[formal-ai] b"
332 );
333 }
334
335 #[test]
336 fn validation_rejects_modes_that_change_where_tools_run() {
337 let mut options = WrapperOptions {
338 use_formal_ai: true,
339 ..WrapperOptions::default()
340 };
341 assert!(validate_options(&options).is_ok());
342 options.isolated = Some("docker".to_string());
343 options.detached = true;
344 assert_eq!(
345 validate_options(&options).unwrap_err(),
346 "--use-formal-ai cannot be combined with --isolated, --detached (experimental mode, see docs/formal-ai.md)"
347 );
348 options.use_formal_ai = false;
349 assert!(validate_options(&options).is_ok());
350 }
351}