feat: bundle the `con-leche` external checker with release toolchains

This PR ships `con-leche`, an external checker whose acceptance is proved in Lean not to admit a proof of `False`, in release toolchains alongside `lean4lean` and `nanoda`, so a third independent kernel is available out of the box.

A `con-leche` build target fetches and builds it, pinned by commit as the repository carries no tags. Like `lean4lean` the target is not part of `ALL`, here because it fetches; release CI builds the two in one step, as both want `elan`. It drops the binary into the build tree, so the existing `bin/` install rule ships it. It needs no `-linitialize_minimal` patch: the checker has its own term representation and imports no `Lean` module, so nothing links `libLean.a` to begin with.

It is built with the toolchain `con-leche` itself pins, not with the toolchain being released, because it consumes `bin/leanexport`'s NDJSON rather than `.olean`s. What it accepts is a separate question from what it builds against: it matches the accelerated `Nat` operations against one pinned dump per toolchain it supports, and declines a stream declaring a spelling none of them describes, so the pin here has to move whenever a release changes those definitions. `tests/pkg/con-leche` therefore checks a whole `Init` export, which is where that drift shows; it skips when the binary was not built, so it costs ordinary test runs nothing.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NboqU3PVduLZzJU8kjeh9G
4 files changed