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>
32 lines
809 B
TOML
32 lines
809 B
TOML
# This file is automatically @generated by Cargo.
|
|
# It is not intended for manual editing.
|
|
version = 3
|
|
|
|
[[package]]
|
|
name = "cc"
|
|
version = "1.2.60"
|
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
|
checksum = "43c5703da9466b66a946814e1adf53ea2c90f10063b86290cc9eb67ce3478a20"
|
|
dependencies = [
|
|
"find-msvc-tools",
|
|
"shlex",
|
|
]
|
|
|
|
[[package]]
|
|
name = "find-msvc-tools"
|
|
version = "0.1.9"
|
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
|
checksum = "5baebc0774151f905a1a2cc41989300b1e6fbb29aff0ceffa1064fdd3088d582"
|
|
|
|
[[package]]
|
|
name = "shlex"
|
|
version = "1.3.0"
|
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
|
checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
|
|
|
|
[[package]]
|
|
name = "topolei-cubical"
|
|
version = "0.1.0"
|
|
dependencies = [
|
|
"cc",
|
|
]
|