)]}'
{
  "commit": "57883ba504fd655ac6b87c4896f6549d813a49ff",
  "tree": "56aa575ab6e0a648738319b28d1b1d80423d98bc",
  "parents": [
    "c632a0a0e434a951cdcf61bb4da3344abadd5587"
  ],
  "author": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Sun Sep 06 21:07:50 2026 +0000"
  },
  "committer": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Thu Sep 10 12:06:28 2026 +0000"
  },
  "message": "feat: bundle the `lean4lean` external checker with release toolchains\n\nThis PR ships the `lean4lean` external checker in release toolchains, alongside `leanchecker`, so an independent kernel implementation is available out of the box.\n\nA `lean4lean` build target fetches and builds it, pinned by `LEAN4LEAN_REV`. Like `leanchecker-paranoid` the target is not part of `ALL`, here because it fetches; release CI builds it explicitly. It drops the binary into the build tree, so the existing `bin/` install rule ships it.\n\nIt is built with the toolchain `lean4lean` itself pins, not with the toolchain being released, because it consumes the export format rather than `.olean`s: `bin/leanexport` writes an export file and `lean4lean --import` reads it, so none of the githash locking `CHECK_OLEAN_VERSION` applies to olean reads is involved, and the binary needs no rebuild per release. The build links `-linitialize_minimal` rather than initializing all of `Lean`, which takes the binary from 117 MB to 36 MB; that is sound only because the checker never elaborates Lean source, so it is applied here rather than asked of `lean4lean`, which must stay buildable against toolchains without `libinitialize_minimal.a`.\n\nBuilding is not evidence of working, though. `lean4lean` models Lean\u0027s primitive definitions, so a revision predating a change to them still builds against its own toolchain but rejects code using those primitives. `tests/pkg/lean4lean` therefore exports `Init.Data.List.Basic` and checks it through `--import`, which replays into an empty environment and so re-adds every primitive; it skips when the binary was not built, so it costs ordinary test runs nothing. `tests/elab/lean4lean_primitives.lean` pins the definitional shapes an external checker matches on, so a change to them fails in the PR that makes it rather than at release time.\n\nThe build step runs on release builds only and deliberately hard-fails, so a checker that cannot check this Lean blocks the release rather than being shipped broken. Nightlies and ordinary CI are unaffected.\n\nCo-Authored-By: Claude Opus 5 \u003cnoreply@anthropic.com\u003e\nClaude-Session: https://claude.ai/code/session_01JPPJuXrRxwXgsWEAqM62dd\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "1ef2985f85f1bf449c5aac87364e4970016e1743",
      "old_mode": 33188,
      "old_path": ".github/workflows/build-template.yml",
      "new_id": "67af328b46f1d18097c58e173c2f94e15a42a3ee",
      "new_mode": 33188,
      "new_path": ".github/workflows/build-template.yml"
    },
    {
      "type": "modify",
      "old_id": "37427171b06efa9b2d05065de853f2bf93d63df0",
      "old_mode": 33188,
      "old_path": "LICENSES",
      "new_id": "f0f6f9a61b50a13971978b54fdd469c4690fe20e",
      "new_mode": 33188,
      "new_path": "LICENSES"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "015b87773bcb9d77c2c21d3e05ccf0c3b68aa786",
      "new_mode": 33261,
      "new_path": "script/lean4lean-minimal-init.sh"
    },
    {
      "type": "modify",
      "old_id": "1c642adcd07bcdea281d12b54171aeb16fb88bce",
      "old_mode": 33188,
      "old_path": "src/CMakeLists.txt",
      "new_id": "13507a38aa5c6acc1e13cdd4c1244b0168e5538c",
      "new_mode": 33188,
      "new_path": "src/CMakeLists.txt"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "b19fccfc2c3e151da294dbf1ca9770fce013e383",
      "new_mode": 33188,
      "new_path": "tests/pkg/lean4lean/run_test.sh"
    }
  ]
}