my-project-public

repository

loading code, commits, and activity

repositories

loading repo index

#1	use anyhow::Result;
#2	use std::path::Path;
#3
#4	// Embed template files
#5	const LAKEFILE: &str = include_str!("../templates/lakefile.lean");
#6	const LEAN_TOOLCHAIN: &str = include_str!("../templates/lean-toolchain");
#7	const MAIN_LEAN: &str = include_str!("../templates/Main.lean");
#8	const GITIGNORE: &str = include_str!("../templates/.gitignore");
#9	const README: &str = include_str!("../templates/README.lean.md");
#10
#11	// Embed lean_support files
#12	const SUPPORT_LAKEFILE: &str = include_str!("../lean_support/lakefile.lean");
#13	const SUPPORT_TOOLCHAIN: &str = include_str!("../lean_support/lean-toolchain");
#14	const SUPPORT_ROOT: &str = include_str!("../lean_support/QEDGen.lean");
#15	const SUPPORT_ACCOUNT: &str = include_str!("../lean_support/QEDGen/Solana/Account.lean");
#16	const SUPPORT_AUTHORITY: &str = include_str!("../lean_support/QEDGen/Solana/Authority.lean");
#17	const SUPPORT_STATE: &str = include_str!("../lean_support/QEDGen/Solana/State.lean");
#18	const SUPPORT_TOKEN: &str = include_str!("../lean_support/QEDGen/Solana/Token.lean");
#19	const SUPPORT_CPI: &str = include_str!("../lean_support/QEDGen/Solana/Cpi.lean");
#20	const SUPPORT_VALID: &str = include_str!("../lean_support/QEDGen/Solana/Valid.lean");
#21	const SUPPORT_SOLANA: &str = include_str!("../lean_support/QEDGen/Solana.lean");
#22
#23	pub fn setup_lean_project(output_dir: &Path) -> Result<()> {
#24	// Write template files
#25	std::fs::write(output_dir.join("lakefile.lean"), LAKEFILE)?;
#26	std::fs::write(output_dir.join("lean-toolchain"), LEAN_TOOLCHAIN)?;
#27	std::fs::write(output_dir.join("Main.lean"), MAIN_LEAN)?;
#28	std::fs::write(output_dir.join(".gitignore"), GITIGNORE)?;
#29	std::fs::write(output_dir.join("README.md"), README)?;
#30
#31	// Write lean_support directory
#32	write_lean_support(output_dir)?;
#33
#34	Ok(())
#35	}
#36
#37	/// Update only the lean_support/ files without touching lakefile.lean or
#38	/// lean-toolchain. This preserves the .lake/ build cache while ensuring
#39	/// axiom definitions are current.
#40	pub fn update_lean_support(output_dir: &Path) -> Result<()> {
#41	write_lean_support(output_dir)
#42	}
#43
#44	fn write_lean_support(output_dir: &Path) -> Result<()> {
#45	let support_dir = output_dir.join("lean_support");
#46	std::fs::create_dir_all(&support_dir)?;
#47	std::fs::write(support_dir.join("lakefile.lean"), SUPPORT_LAKEFILE)?;
#48	std::fs::write(support_dir.join("lean-toolchain"), SUPPORT_TOOLCHAIN)?;
#49	std::fs::write(support_dir.join("QEDGen.lean"), SUPPORT_ROOT)?;
#50
#51	// Write QEDGen/Solana.lean (namespace file)
#52	let qedgen_dir = support_dir.join("QEDGen");
#53	std::fs::create_dir_all(&qedgen_dir)?;
#54	std::fs::write(qedgen_dir.join("Solana.lean"), SUPPORT_SOLANA)?;
#55
#56	// Write QEDGen/Solana modules
#57	let solana_dir = support_dir.join("QEDGen/Solana");
#58	std::fs::create_dir_all(&solana_dir)?;
#59	std::fs::write(solana_dir.join("Account.lean"), SUPPORT_ACCOUNT)?;
#60	std::fs::write(solana_dir.join("Authority.lean"), SUPPORT_AUTHORITY)?;
#61	std::fs::write(solana_dir.join("State.lean"), SUPPORT_STATE)?;
#62	std::fs::write(solana_dir.join("Token.lean"), SUPPORT_TOKEN)?;
#63	std::fs::write(solana_dir.join("Cpi.lean"), SUPPORT_CPI)?;
#64	std::fs::write(solana_dir.join("Valid.lean"), SUPPORT_VALID)?;
#65
#66	Ok(())
#67	}
#68

z6Mkq5mY3JWtxoxUobWcfNHm7AkRubgSWEZTkBVqZXJviFZ5/my-project-public