5e9be0ffe2
Some checks are pending
Lean Action CI / build (push) Waiting to run
- LICENSE: proprietary, all rights reserved. Public availability of the repo grants no license; use requires written consent from mgorog@gmail.com. - README: "Reusing this engine" → "Consuming the engine (with permission)" with explicit pointer to LICENSE. - CI: workflow moved from .github/workflows/ to .forgejo/workflows/ so forgejo's runner picks it up. Workflow now also installs Rust, builds native/cubical/, and runs cubical-test (62/62 verification) rather than only running lake build (which would have failed at link time without libtopolei_cubical.a). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
73 lines
2.9 KiB
Markdown
73 lines
2.9 KiB
Markdown
# cubical-transport-hott-lean4
|
|
|
|
A Lean 4 implementation of cubical-transport homotopy type theory
|
|
(CCHM-flavor), with a fast Rust kernel exposed through C ABI.
|
|
|
|
The Lean side defines the syntax, semantics, and soundness theorems.
|
|
The Rust side discharges the per-step β-rules of the evaluator.
|
|
Lean axioms are routed through `@[implemented_by]` to Rust functions
|
|
that return Lean objects in the same shape Lean would have produced;
|
|
the soundness layer (`CubicalTransport/Soundness.lean`) certifies the
|
|
backend at the boundary, so the kernel speed of the Rust code
|
|
preserves the Lean-level proofs.
|
|
|
|
## What's here
|
|
|
|
- `CubicalTransport/` — 22 Lean modules for syntax, substitution,
|
|
dimensional structure, faces, typing, evaluation (eval / value /
|
|
readback), transport, Glue, composition, and the soundness theorems.
|
|
- `native/cubical/` — Rust kernel (`#![no_std]`, dual-target native
|
|
staticlib + cdylib, wasm32 cdylib).
|
|
- `CubicalTest.lean`, `CubicalBench.lean` — engine smoke + property
|
|
tests (62/62 passing) and microbenchmarks.
|
|
|
|
## Consuming the engine (with permission)
|
|
|
|
This Software is **proprietary**. See `LICENSE` — no use is granted
|
|
by virtue of the repository being public. The instructions below
|
|
are for the copyright holder and any party with prior written consent
|
|
from `mgorog@gmail.com`.
|
|
|
|
Add as a Lake dependency from another Lean 4 project:
|
|
|
|
```toml
|
|
[[require]]
|
|
name = "cubicalTransport"
|
|
path = "../cubical-transport-hott-lean4" # or git = "..."
|
|
```
|
|
|
|
Then `import CubicalTransport.Syntax`, `import CubicalTransport.Eval`,
|
|
etc. Link against `native/cubical/target/release/libtopolei_cubical.a`
|
|
in your own `moreLinkArgs` so the FFI symbols resolve.
|
|
|
|
## Build
|
|
|
|
```bash
|
|
(cd native/cubical && cargo build --release)
|
|
lake build
|
|
./.lake/build/bin/cubical-test # 62/62 tests pass
|
|
```
|
|
|
|
## Reference
|
|
|
|
- `docs/FFI_DESIGN.md` — C ABI contract between Lean and the Rust kernel.
|
|
- `docs/FFI_COMPLETENESS.md` — per-function axiom audit.
|
|
- `docs/KERNEL_BOUNDARY.md` — what this delivers in unmodified Lean 4 vs.
|
|
what would need upstream Lean kernel work.
|
|
- `docs/NUMERICAL.md` — numerical implementation principles.
|
|
- `docs/PHASE1_HISTORY.md` — original transport/composition formalisation
|
|
plan (archived; Phase 1 closed; preserved as methodology template
|
|
for future phases).
|
|
- `docs/ZIGZAG_PORT.md` — step-by-step Lean port plan for the n-category
|
|
combinatorial engine (Phase 2+ higher-cell backend). Lands here
|
|
in the engine. **Read the cascade caveat at the top before
|
|
editing**: changes in the ported zigzag layer cascade to the
|
|
sibling `topolei` repo.
|
|
- `native/cubical/README.md` — Rust crate build + dev guide.
|
|
- `native/cubical/WASM.md` — wasm32 ABI integration contract.
|
|
|
|
## Used by
|
|
|
|
- [`max/topolei`](../topolei) — the cells-spec workspace interface,
|
|
built on this engine. See its `docs/cells-spec.md` and
|
|
`docs/STATUS.md` for the application-side picture.
|