Palomar.ix

Palomar.ix is the Lean 4.33 compatibility home for the current Palomar Registry snapshot.

The upstream projects remain pinned to their immutable registry commits and retain their original toolchain metadata. This repository projects isolated Lean 4.33 workspaces, applies checked compatibility overlays, asks a pinned ix compiler to compile each verified solution closure, and assembles the anonymous pieces into one catalog.

Layout

• Palomar/: typed registry snapshot, workspace generator, overlay manifest, and build driver.
• Workspace/: generated per-entry Lake workspaces. Package stores and lockfiles are local build state and are ignored.
• Patches/v4.33/: source migrations from each immutable upstream revision to the shared Lean/Mathlib 4.33 compatibility spine.

Only overlays listed in Palomar/Compatibility.lean are considered validated. A *.wip.patch records recoverable port work but is never applied by the corpus driver.

Development

The flake supplies Lean 4.33, the exact ix compiler, and the process tools used by the corpus builder. No sibling ix checkout is needed:

nix develop
lake build palomar
lake exe palomar gen --check
lake exe palomar spec
lake exe palomar build --only PalomarVertexGap22

The packaged driver is also available as nix run . -- <command>; for example, nix run . -- spec. nix flake check builds the driver and runs its focused tests plus the generated-workspace freshness check.

Outside Nix, install the toolchain in lean-toolchain, put a compatible ix binary on PATH (or set IX_EXE=/absolute/path/to/ix), and use the same Lake commands. Palomar's Lake package has no ix source dependency.

The compatibility target is exactly leanprover/lean4:v4.33.0, with Mathlib revision db584cd6d46c92f209a44c0f1c829460d327499d. The flake pins ix revision 148b4fc537c365793cc78e244d6cff023acbc7f9.