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>
49 lines
1.7 KiB
TOML
49 lines
1.7 KiB
TOML
[package]
|
|
name = "topolei-cubical"
|
|
version = "0.1.0"
|
|
edition = "2021"
|
|
rust-version = "1.76"
|
|
description = "Rust backend for Lean 4 cubical-transport HoTT evaluator (topolei)"
|
|
license = "MIT"
|
|
publish = false
|
|
|
|
# Dual-target crate:
|
|
# - `staticlib` for native linking into Lean executables.
|
|
# - `cdylib` for wasm32-unknown-unknown (embeds into a Lean-wasm
|
|
# composite artifact).
|
|
#
|
|
# Both crate types share the same `src/lib.rs` and `no_std` source —
|
|
# the only difference is link kind. Build both:
|
|
# cargo build --release # native staticlib
|
|
# cargo build --release --target wasm32-unknown-unknown # wasm cdylib
|
|
[lib]
|
|
name = "topolei_cubical"
|
|
crate-type = ["staticlib", "cdylib"]
|
|
|
|
# ── No std ──────────────────────────────────────────────────────────────────
|
|
# wasm32-unknown-unknown has no std library; we operate purely on
|
|
# Lean-allocated `lean_object*` pointers via extern "C" calls into the
|
|
# Lean runtime. The evaluator is pure functional — no IO, no threads,
|
|
# no allocator. Native builds also go through `no_std` for ABI uniformity.
|
|
|
|
[dependencies]
|
|
|
|
[build-dependencies]
|
|
cc = "1.0"
|
|
|
|
[features]
|
|
default = []
|
|
# When enabled, FFI stubs `panic!` on calls — useful for detecting
|
|
# accidentally-wired @[implemented_by] during development. Default:
|
|
# stubs return marker neutrals and Lean code ignores the Rust impl.
|
|
strict-stubs = []
|
|
|
|
[profile.release]
|
|
opt-level = 3
|
|
lto = true
|
|
codegen-units = 1
|
|
panic = "abort" # no unwinding — matches wasm32 default
|
|
|
|
[profile.dev]
|
|
opt-level = 0
|
|
panic = "abort"
|