my-project-public

repository

loading code, commits, and activity

repositories

loading repo index

#1	use crate::api::BuildStatus;
#2	use anyhow::Result;
#3	use std::path::{Path, PathBuf};
#4	use std::process::Stdio;
#5	use tokio::process::Command;
#6
#7	pub struct ValidationResult {
#8	pub status: BuildStatus,
#9	pub log_path: Option<PathBuf>,
#10	}
#11
#12	pub async fn validate_completion(
#13	output_dir: &Path,
#14	completion_index: usize,
#15	validation_workspace: Option<&Path>,
#16	) -> Result<ValidationResult> {
#17	let log_dir = output_dir.join("validation");
#18	std::fs::create_dir_all(&log_dir)?;
#19	let log_path = log_dir.join(format!("completion_{}.log", completion_index));
#20
#21	let workspace = match validation_workspace {
#22	Some(ws) => ws.to_path_buf(),
#23	None => validation_workspace_dir()?,
#24	};
#25	std::fs::create_dir_all(&workspace)?;
#26	ensure_workspace_ready(&workspace).await?;
#27
#28	// Copy Best.lean to validation workspace
#29	std::fs::copy(output_dir.join("Best.lean"), workspace.join("Best.lean"))?;
#30
#31	// Run lake build
#32	let build_result = run_command(
#33	"lake",
#34	&["build", "Best"],
#35	&workspace,
#36	&[],
#37	)
#38	.await;
#39
#40	match build_result {
#41	Ok((stdout, stderr, code)) => {
#42	let combined = format!("{}\n{}", stdout, stderr);
#43	std::fs::write(&log_path, &combined)?;
#44	Ok(ValidationResult {
#45	status: if code == 0 {
#46	BuildStatus::Success
#47	} else {
#48	BuildStatus::Failed
#49	},
#50	log_path: Some(log_path),
#51	})
#52	}
#53	Err(e) => {
#54	std::fs::write(&log_path, format!("Error: {}", e))?;
#55	Ok(ValidationResult {
#56	status: BuildStatus::Skipped,
#57	log_path: Some(log_path),
#58	})
#59	}
#60	}
#61	}
#62
#63	/// Set up the global validation workspace. Called by `qedgen setup` and
#64	/// by the install script to pre-fetch the Mathlib cache.
#65	pub async fn setup_workspace(workspace: Option<&Path>) -> Result<()> {
#66	let ws = match workspace {
#67	Some(ws) => ws.to_path_buf(),
#68	None => validation_workspace_dir()?,
#69	};
#70
#71	std::fs::create_dir_all(&ws)?;
#72	eprintln!("Setting up validation workspace at {}...", ws.display());
#73
#74	crate::project::setup_lean_project(&ws)?;
#75	eprintln!(" Project scaffold created.");
#76
#77	eprintln!(" Running lake update...");
#78	let _update = run_command("lake", &["update"], &ws, &[]).await;
#79
#80	fetch_or_build_mathlib(&ws).await;
#81
#82	eprintln!("Workspace setup complete: {}", ws.display());
#83	Ok(())
#84	}
#85
#86	/// Ensure the validation workspace is ready for `lake build Best`.
#87	///
#88	/// On first call (no lakefile.lean exists): sets up the full project scaffold,
#89	/// runs `lake update` to resolve dependencies, and fetches the Mathlib cache.
#90	///
#91	/// On subsequent calls: only updates the lean_support/ files (which may change
#92	/// when axioms are updated), preserving .lake/ build cache.
#93	async fn ensure_workspace_ready(workspace: &Path) -> Result<()> {
#94	if !workspace.join("lakefile.lean").exists() {
#95	crate::project::setup_lean_project(workspace)?;
#96
#97	eprintln!(" Setting up validation workspace (first time)...");
#98	let _update = run_command("lake", &["update"], workspace, &[]).await;
#99
#100	fetch_or_build_mathlib(workspace).await;
#101	} else {
#102	crate::project::update_lean_support(workspace)?;
#103	}
#104
#105	Ok(())
#106	}
#107
#108	/// Fetch pre-built Mathlib oleans, falling back to building from source.
#109	async fn fetch_or_build_mathlib(workspace: &Path) {
#110	eprintln!(" Fetching Mathlib cache (this may take a few minutes)...");
#111	let cache_result = run_command("lake", &["exe", "cache", "get"], workspace, &[]).await;
#112
#113	match &cache_result {
#114	Ok((_, _, code)) if *code == 0 => {
#115	eprintln!(" Mathlib cache fetched successfully.");
#116	}
#117	_ => {
#118	eprintln!(" Mathlib cache fetch failed. Building from source...");
#119	let build_result = run_command("lake", &["build", "Mathlib.Tactic"], workspace, &[]).await;
#120	match &build_result {
#121	Ok((_, _, code)) if *code == 0 => {
#122	eprintln!(" Mathlib built from source successfully.");
#123	}
#124	_ => {
#125	eprintln!(" Warning: Mathlib build failed. First validation run will be slow.");
#126	}
#127	}
#128	}
#129	}
#130	}
#131
#132	async fn run_command(
#133	cmd: &str,
#134	args: &[&str],
#135	cwd: &Path,
#136	env: &[(&str, &str)],
#137	) -> Result<(String, String, i32)> {
#138	let mut command = Command::new(cmd);
#139	command.args(args).current_dir(cwd).stdout(Stdio::piped()).stderr(Stdio::piped());
#140
#141	for (key, value) in env {
#142	command.env(key, value);
#143	}
#144
#145	let output = command.output().await?;
#146	let stdout = String::from_utf8_lossy(&output.stdout).to_string();
#147	let stderr = String::from_utf8_lossy(&output.stderr).to_string();
#148	let code = output.status.code().unwrap_or(-1);
#149
#150	Ok((stdout, stderr, code))
#151	}
#152
#153	fn validation_workspace_dir() -> Result<PathBuf> {
#154	if let Ok(ws) = std::env::var("QEDGEN_VALIDATION_WORKSPACE") {
#155	return Ok(PathBuf::from(ws));
#156	}
#157
#158	if let Ok(xdg) = std::env::var("XDG_CACHE_HOME") {
#159	return Ok(PathBuf::from(xdg)
#160	.join("qedgen-solana-skills")
#161	.join("validation-workspace"));
#162	}
#163
#164	if cfg!(target_os = "macos") {
#165	let home = std::env::var("HOME")?;
#166	return Ok(PathBuf::from(home)
#167	.join("Library")
#168	.join("Caches")
#169	.join("qedgen-solana-skills")
#170	.join("validation-workspace"));
#171	}
#172
#173	let home = std::env::var("HOME")?;
#174	Ok(PathBuf::from(home)
#175	.join(".cache")
#176	.join("qedgen-solana-skills")
#177	.join("validation-workspace"))
#178	}
#179
#180

z6Mkq5mY3JWtxoxUobWcfNHm7AkRubgSWEZTkBVqZXJviFZ5/my-project-public