diff --git a/FORK_STRATEGY.md b/FORK_STRATEGY.md new file mode 100644 index 0000000000..4abe8a61e2 --- /dev/null +++ b/FORK_STRATEGY.md @@ -0,0 +1,186 @@ +# lean4-htt: Fork Strategy + +This is a fork of [leanprover/lean4](https://github.com/leanprover/lean4) +maintained for HoTT-compatible kernel extensions. The fork exists to add +foundational primitives that upstream Lean does not provide: identity Path +types without UIP, transport with full computational behavior, higher +inductive types (HITs), and (eventually) cubical primitives. + +The fork is the meta-theoretic foundation for the polytropos project (a +cubical-transport HoTT engine). Polytropos's σ-calculus and substitution +machinery need HoTT-compatible meta-level reasoning that cannot be built +out of standard Lean inductive types alone without leaking UIP via +`Quot.sound` + `propext`. + +## Why kernel-level, not library-level + +Standard Lean library encodings of HoTT (e.g., via `Quot`) inherit UIP +from the kernel's quotient axiom. UIP is incompatible with univalence: +in a univalent universe, paths between types can be non-trivially +distinct, and UIP collapses this. The fork avoids this by adding Path +types as kernel primitives with their own reduction rules — no Quot +trapdoor, no inherited UIP. + +This is the same engineering decision Cubical Agda made when extending +Agda with cubical primitives. The work is bounded, the precedent exists, +the architectural pattern is known. + +## Sync strategy with upstream + +The fork tracks `leanprover/lean4` (`upstream` remote) and publishes to +`maxgit.wg/max/lean4-htt` (`origin` remote). + +### Sync cadence + +Merge from upstream regularly. The cadence is "frequently enough that +each merge is mechanical" rather than a fixed schedule. Typical triggers: +- New upstream release +- Significant upstream features (e.g., LLVM backend updates, compiler + improvements) that we want to inherit +- After any local modification, before extending further + +### Merge over rebase + +The fork uses merges (not rebases) when pulling upstream. Rationale: +- Preserves the divergence history visibly in git log +- Avoids force-pushing the fork's master branch +- Makes each upstream sync a single commit (the merge commit) that can + be examined or reverted + +### Conflict resolution discipline + +When upstream and the fork modify the same file: +- Resolve in favor of preserving the fork's HoTT additions +- Verify the merged result still passes both upstream's tests and the + fork's HoTT-specific tests +- Document non-trivial conflicts in the merge commit's body + +If upstream restructures something the fork depends on (e.g., changing +the `Expr` representation, refactoring `whnf`), the fork's patches need +re-application. Keep modifications localized so re-application is +mechanical. + +## Modification strategy + +### Locality principle + +Add HoTT primitives in NEW files where possible: +- `src/kernel/hott/path.cpp`, `src/kernel/hott/transp.cpp`, etc. +- `src/Init/HoTT/` for Lean-side exposure of the new primitives +- `hott/` directory at the repo root for fork-specific design docs, + rationale, and tests + +Only modify existing upstream files where the kernel architecture +requires it: +- `src/kernel/expr.h` (or equivalent): add new `Expr::Kind` variants +- `src/kernel/whnf.cpp` (or equivalent): add a single hook that + dispatches to the HoTT reducer +- `src/kernel/type_checker.cpp` (or equivalent): add a single hook for + HoTT inference rules + +Every modification to an upstream file is documented with a comment +naming what it does and why. The grep-friendly tag is `LEAN4-HTT:`. + +### Feature flag (compile-time gating) + +HoTT primitives are gated behind a compile-time flag (likely a CMake +option `LEAN_HOTT=ON`). When `OFF`, the fork builds as vanilla Lean. +When `ON`, the HoTT extensions activate. + +This reduces upstream-merge friction: most upstream changes don't touch +HoTT code paths, so they merge cleanly into the fork. It also gives a +testable "is the fork still upstream-equivalent in vanilla mode?" +property. + +### Patch-series organization + +HoTT additions are organized as a series of focused commits, each adding +one cohesive feature: +- Commit: add `Path` type former +- Commit: add `Refl` constructor +- Commit: add `J` eliminator + reduction +- Commit: add `transport` + reduction +- Commit: add HIT support +- etc. + +Each commit is self-contained where possible. If upstream restructures +something that breaks a commit's assumptions, that commit can be +identified and re-applied without disturbing the others. + +## Directory structure + +``` +lean4-htt/ +├── FORK_STRATEGY.md # this file +├── hott/ # fork-specific design + tests +│ ├── README.md # what's in this directory +│ ├── design/ # architectural decisions +│ └── tests/ # HoTT-specific test suites +├── src/ # upstream Lean source (modified per locality principle) +│ ├── kernel/ +│ │ ├── hott/ # new directory for HoTT kernel primitives +│ │ └── ... # upstream files; LEAN4-HTT: tags mark modifications +│ ├── Init/ +│ │ ├── HoTT/ # new directory for Lean-side HoTT API +│ │ └── ... # upstream files +│ └── ... # rest of upstream src +├── tests/ # upstream tests (run unchanged) +└── ... # rest of upstream files +``` + +## CI and verification + +Two test suites: +1. Upstream's full test suite, run in `LEAN_HOTT=OFF` mode. Must pass + with no regression. +2. The fork's HoTT-specific test suite under `hott/tests/`, run in + `LEAN_HOTT=ON` mode. Verifies the new primitives behave correctly. + +CI runs both on every commit to the fork's master. + +## Forbidden moves + +The fork's HoTT extensions must not: +- Introduce UIP at the kernel level (defeats the purpose of forking) +- Depend on `Quot.sound` for HoTT primitive reductions +- Use `Classical.choice` in HoTT primitive implementations +- Add ad-hoc axioms beyond the minimum needed for soundness + +If a HoTT primitive cannot be implemented constructively (no axioms, no +UIP-leaky principles), it doesn't go in the fork. This is the same +discipline polytropos enforces at the engine's object level. + +## Maintenance + +The fork's maintainer: +- Runs upstream sync per the cadence above +- Resolves conflicts preserving HoTT additions +- Updates `FORK_STRATEGY.md` when the strategy evolves +- Documents non-mechanical decisions in `hott/design/` + +The fork is at `maxgit.wg/max/lean4-htt`. + +## Phases + +This is Phase 0: fork infrastructure (this file, directory structure, +remotes, sync workflow). No kernel modifications yet. + +Subsequent phases add HoTT primitives: +- Phase 1: minimal `Path` + `Refl` + `J` (the foundational core) +- Phase 2: `transport` with full computational behavior +- Phase 3: HIT support +- Phase 4: cubical primitives (interval, faces, Glue) if needed for + polytropos's full spec + +Each phase is gated on the previous landing and passing both test +suites. + +## Related projects + +- [polytropos](https://maxgit.wg/max/polytropos) — the cubical-transport + HoTT engine that depends on this fork. +- [Cubical Agda](https://github.com/agda/cubical) — the precedent for + adding cubical primitives to a host proof assistant. +- [topolei](https://maxgit.wg/max/topolei) — the prior project that + used Rust FFI for the computational kernel; informs the architectural + pattern for foundational extensions. diff --git a/hott/README.md b/hott/README.md new file mode 100644 index 0000000000..0660db1691 --- /dev/null +++ b/hott/README.md @@ -0,0 +1,19 @@ +# hott/ — Fork-specific HoTT extensions + +This directory holds fork-specific content that's not part of the +upstream Lean tree: + +- `design/` — architectural decisions, rationale documents, design + notes for each phase of HoTT primitive additions. +- `tests/` — HoTT-specific test suites (compiled with `LEAN_HOTT=ON`). + +Upstream Lean code lives in `../src/` under its normal layout, with +modifications tagged `LEAN4-HTT:` per the locality principle in +`../FORK_STRATEGY.md`. + +New HoTT kernel primitives live in `../src/kernel/hott/`. +New HoTT Lean-side APIs live in `../src/Init/HoTT/`. + +This directory exists at the repo root because it's outside the upstream +tree — it documents and tests the fork's additions without intermixing +with upstream files. diff --git a/hott/design/.gitkeep b/hott/design/.gitkeep new file mode 100644 index 0000000000..e69de29bb2 diff --git a/hott/tests/.gitkeep b/hott/tests/.gitkeep new file mode 100644 index 0000000000..e69de29bb2