31d19f655e
Some checks are pending
Lean Action CI / build (push) Waiting to run
Restructure to engine-only contents. Application code (Topolei.*
namespace, canvas-rs / render Rust crates, Main / ProbeTest, naga IR
pipeline, Selection / Subobject / Trace / Obs.Ctx hypothesis stack,
cells-spec / HYPOTHESES / STATUS / NAGA_IR_PLAN docs) moves to the
sibling repo max/topolei.
What moved:
- `Topolei/Cubical/*.lean` (22 files) → `CubicalTransport/*.lean`
with namespace `Topolei.Cubical.*` renamed to `CubicalTransport.*`.
Fully-qualified test types `TopoleiCubical{FFI,Property}Test` →
`CubicalTransport{FFI,Property}Test` for consistency.
- New root file `CubicalTransport.lean` re-exporting all 22 modules.
- Lakefile: package `cubicalTransport`; lib `CubicalTransport`; only
`cubical-test` and `cubical-bench` exes (no GPU link path).
The split criterion: anything an AI shortcut could break that would
cascade-corrupt downstream proofs lives here. Anything that would
only break the application stays in the topolei interface repo.
cubical-test passes 62/62 (smoke + properties) on the renamed engine.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
23 lines
566 B
TOML
23 lines
566 B
TOML
name = "cubicalTransport"
|
|
version = "0.1.0"
|
|
defaultTargets = ["cubical-test"]
|
|
|
|
[[lean_lib]]
|
|
name = "CubicalTransport"
|
|
|
|
[[lean_exe]]
|
|
name = "cubical-test"
|
|
root = "CubicalTest"
|
|
# Phase C.3 smoke tests + Phase D.1 property tests on the
|
|
# Rust-backed cubical evaluator. No GPU dependencies.
|
|
moreLinkArgs = [
|
|
"./native/cubical/target/release/libtopolei_cubical.a",
|
|
]
|
|
|
|
[[lean_exe]]
|
|
name = "cubical-bench"
|
|
root = "CubicalBench"
|
|
# Phase D.2 performance benchmarks on the Rust-backed evaluator.
|
|
moreLinkArgs = [
|
|
"./native/cubical/target/release/libtopolei_cubical.a",
|
|
]
|