v0.1.17

Version-range cfg flags for per-toolchain gating

lean-rs-sys's build script now emits a monotone lower-bound cfg family alongside the existing exact-version
lean_v_<token> flag: lean_at_least_<major>_<minor> is set for every supported-window minor at or below the resolved
toolchain (release candidates count as their target minor, so 4.31.0-rc1 ⇒ lean_at_least_4_31). Downstream code can
gate a symbol introduced in a given release with #[cfg(lean_at_least_4_31)] and the older path with
#[cfg(not(lean_at_least_4_31))], rather than OR-ing exact-version tokens. The script also emits rustc-check-cfg for
every version token and minor boundary the window spans, so gating on a non-active version stays lint-clean under
-D warnings; only boundaries within the window [floor ..= head] are registered.

Re-export the supported-window query API from lean-toolchain

lean-toolchain now re-exports SUPPORTED_TOOLCHAINS, SupportedToolchain, supported_for, and supported_by_digest
from lean-rs-sys, alongside the existing LEAN_VERSION / LEAN_HEADER_DIGEST / required_symbols() surface. This
lets a consumer answer "is this pin inside the supported window?" and "does this lean.h digest match a known
toolchain?" through the non-FFI facade, without a direct lean-rs-sys dependency (which carries link directives).

Guarded the bundled interop shim copy against drift

lean-rs-host's bundled lean-rs-interop-shims is now a verbatim copy of the canonical package under
crates/lean-rs/shims/lean-rs-interop-shims. The host copy had silently drifted — it was missing
LeanRsInterop.Worker.Stream (the worker row-streaming helpers), which had been added to the canonical copy alone. The
host copy is meant to be the full generic package, not a host-trimmed subset (it already carried Callback.String,
which the host policy shims also do not import), so the missing module was negligent drift, not design. Worker.Stream
is added to the host copy, and a new interop_shims_parity test asserts the two copies are byte-identical so they
cannot diverge again. The duplication itself is structural — a published crate's Cargo.toml include cannot reach
into another crate's directory, so each crate vendors its own self-contained copy.

Removed the obsolete lake/ shim package mirror

Deleted lake/lean-rs-host-shims and lake/lean-rs-interop-shims. These were the standalone Lake packages from the
original hybrid layout (v0.1.0), back when downstream consumers required the host shims over git. Once the shim
packages were bundled into the lean-rs and lean-rs-host crates — shipped via each crate's Cargo.toml include and
built on demand by the Rust loader — the lake/ copies became an unreferenced mirror that had drifted stale (they never
received the string-callback C path). Nothing in the build, tests, fixtures, or current docs referenced them. The
authoritative copies remain under crates/lean-rs/shims/lean-rs-interop-shims,
crates/lean-rs-host/shims/lean-rs-interop-shims, and crates/lean-rs-host/shims/lean-rs-host-shims.

Lean 4.31.0-rc1 added to the supported window

leanprover/lean4:v4.31.0-rc1 is now a supported and CI-tested toolchain (new lean.h digest; layout and
REQUIRED_SYMBOLS probes both clean, no missing symbols), and is promoted to the CI/release/sanitizer head. The
supported window is now 4.26.0 through 4.31.0-rc1.

Adopting rc1 also fixed a latent bug in the host "attempt proof" shim, surfaced by Lean 4.31's stricter tactic-block
indentation enforcement. When a candidate tactic was spliced into an existing proof, the bare by keyword atom could be
selected as the insertion position and the candidate indented from an unrelated line, emitting it at column 0 — accepted
leniently by Lean ≤ 4.30 but rejected as a parse error by Lean ≥ 4.31. The shim now models a selected proof position as
a type that, by construction, is a real tactic at a positive source column, and derives the candidate's indentation from
that tactic's own column, so insertion aligns with a sibling tactic the parser already accepted. This makes the host's
bounded proof-attempt path behave identically across the supported window.

Structured worker declaration search

lean-rs-worker-protocol replaces the 0.1.16 declaration-search request/row shape with a structured bounded search
surface: name contains/suffix matching, kind filters, required-constant filters, conclusion-head filters, namespace or
module scope biasing, deterministic scores/ranks, compact declaration flags, and fanout/timing facts. Search remains
metadata-only from the caller's perspective and does not render declaration type text; use the existing single-name
declaration-type query for explicit bounded rendering.