lean4-htt/FORK_STRATEGY.md

lean4-htt: Fork Strategy

This is a fork of 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 — the cubical-transport HoTT engine that depends on this fork.
• Cubical Agda — the precedent for adding cubical primitives to a host proof assistant.
• topolei — the prior project that used Rust FFI for the computational kernel; informs the architectural pattern for foundational extensions.