c2e3ecb3e3
Some checks are pending
Lean Action CI / build (push) Waiting to run
Implements the cells-spec vision: a computation space that preserves auditability, correctness, interactivity. Phase 1 (Lean kernel + naga-IR Rust backend) is closed; foundation hypothesis stack (Selection H1+H2, Subobject H3, Trace H5, Obs.Ctx C2, Cubical.Trace) landed. Highlights: - Cubical-HoTT syntax + value/eval/readback in Lean - naga-IR pipeline (no GLSL string crosses FFI; 17/17 probes pass) - Honesty audit: every non-transport (sealed cells, vertex shader, Y-flip, presentation conventions) is documented as such - Polymorphic Trace α as free monoid; Cubical.Trace gives CTerm → Trace CTerm by structural fold (homomorphism = definition) - Selection as Huet zipper; Subobject as Boolean algebra over WCell - All theorems proven; the proof IS the implementation See STATUS.md for the resume guide. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
34 lines
1.3 KiB
Rust
34 lines
1.3 KiB
Rust
//! Build script — compiles the C shim that exposes Lean's inline
|
|
//! runtime helpers as real extern symbols (see shim.c).
|
|
//!
|
|
//! Native targets only. Wasm builds skip the shim (Phase D concern).
|
|
|
|
fn main() {
|
|
// Skip shim compilation on wasm — we don't link against Lean's
|
|
// runtime there; the Lean-wasm composite artifact story is a
|
|
// Phase D deliverable.
|
|
let target = std::env::var("TARGET").unwrap_or_default();
|
|
if target.starts_with("wasm32") {
|
|
return;
|
|
}
|
|
|
|
// Locate lean.h via the elan toolchain or an explicit env var.
|
|
let lean_include = std::env::var("LEAN_INCLUDE").unwrap_or_else(|_| {
|
|
// Default: assume elan is in PATH and use `lean --print-prefix`.
|
|
let prefix = std::process::Command::new("lean")
|
|
.arg("--print-prefix")
|
|
.output()
|
|
.expect("failed to run `lean --print-prefix`; set LEAN_INCLUDE instead");
|
|
let prefix = String::from_utf8(prefix.stdout).unwrap();
|
|
format!("{}/include", prefix.trim())
|
|
});
|
|
|
|
cc::Build::new()
|
|
.file("shim.c")
|
|
.include(&lean_include)
|
|
.flag("-Wno-unused-parameter")
|
|
.compile("topolei_cubical_shim");
|
|
|
|
println!("cargo:rerun-if-changed=shim.c");
|
|
println!("cargo:rerun-if-env-changed=LEAN_INCLUDE");
|
|
}
|