v4.33.0.1

• Refactor adoption into read-only action planning, component accounting, and report
  rendering. Share donor/source selection with execution and retain execution-time
  validation. Separate logical replacement, retained source/package/artifact content,
  and payload transfer. Deduplicate source objects by source identity; never add
  publication samples to measured totals. Remove the misleading aggregate published
  artifact-size headline. Report signed logical change when complete; physical disk
  recovery and peak allocation remain unknown. Add typed uncertainty and versioned
  additive JSON estimates; deprecate aggregate sample and physical-recovery scalars.

• Measure inventory completeness and local post-operation observations. Reuse one
  missing-frame validator for sparse OCI planning/pulling, deduplicate exact ranges,
  and expose remaining payload separately from config metadata read during planning.

• Correct attach/detach transaction cleanup: failed backup deletion after commit
  reports cleanup failure without attempting rollback from a partially removed backup.

• Add OCI metadata-backed artifact size references to adoption planning, with
  explicitly approximate same-repository revision fallbacks. Keep these separate
  from exact reuse/storage decisions. Summarize unknown costs and substituted
  versions in normal output; expose per-project provenance with --verbose and
  JSON. Metadata lookup never installs compilers or downloads artifact packs.

• Parallelize adoption project inspection and hashing of unique local dependency
  directories. Automatically size the planning pool from available CPUs and RAM,
  capped at eight workers; add adopt --jobs for explicit control. Deduplicate
  source hashes and repeated size inventories within each plan, preserve result
  order and worker progress, and retain fresh execution-time validation. Package
  preparation and attachment remain serialized.

• Make shared package and artifact identities cover the full normalized effective
  root graph, including dependencies introduced by overrides. This fixes an
  unsound reuse key; it does not demonstrate an incorrect Lean verdict. Bump
  shared-project identity to v4 and artifact compatibility to v3; older records
  cannot authorize artifact reuse. Unrelated graph changes now conservatively
  invalidate reuse too.

• During first adoption, retain compatible build outputs from the original local
  dependency checkout only when its recorded compiler and graph provenance match.
  Exclude linked state and path-sensitive traces; report rejected donors and the
  need to rebuild when provenance is unavailable. Source import remains separate
  from artifact migration, including for subdirectory packages.

• Revalidate every project during batch adoption instead of skipping projects
  merely because an attachment marker exists. Broken or stale links are repaired
  through normal adoption; modified local checkouts remain protected. Planning,
  adoption, and verify PROJECT share attachment validation. Project verification
  is local-only and reports subject_kind: project with null lock/environment IDs;
  it verifies attachment state, not a Lean proof verdict.

• Plan reuse with locally hashed Lean/Lake identities without installing tools.
  Report incomplete storage estimates, unknown download amounts, and unknown
  recovery instead of treating missing dependencies as zero-cost acquisitions.
  Storage figures describe materialized content, not physical disk allocation.

• Exercise Windows unit tests, macOS real-Lean integration, and clean anonymous
  Mathlib consumption of the PR checkout in CI. Add active HTTP cancellation
  and descendant-termination regressions; cancellation now checks between
  available HTTP chunks, and POSIX shutdown kills surviving descendants even
  when the direct child exits first.

• Make store lifecycle guarantees consistent across every execution path.
  Every cross-process lock now comes from one registry under <home>/.locks
  (LockPaths), so shared-project package locks and store cleanup finally
  contend; every published tree goes through one staged-publish transaction
  whose staging directory is owned by a lock while it is built, so doctor --repair only removes staging trees nobody is building; scratch cleanup
  holds the workspace lease across its rename; capsule and slim-toolchain
  replacement swaps the old tree out only once the new one is complete and
  restores it if the swap fails; a failed adopt restores the previous
  attachment record and config instead of deleting them; sparse projections
  validate the existing environment before writing into it.

• Carry cancellation and bounds end to end. All child processes (Lean, Lake,
  Git, elan, helpers) run through one internal seam with a shared timeout,
  cancel event, bounded output and observer buffering, process-tree shutdown
  and reader deadlines, and resource limits are applied without importing in
  the forked child. Sparse acquisition, capsule pulls and source fetches
  accept the cancel event; async wrappers preserve the caller's cancellation
  when a worker fails during cleanup; a failing matrix context always stops
  its running siblings.

• Validate at the boundary and keep identities stable. One portable
  relative-path policy (rejecting absolute, drive, UNC, backslash, NUL and
  .. forms) backs manifests, locks, capsules, archives and program
  inventories; locks validate packagesDir and package subdirectories at
  construction and freeze their manifest so lock_id cannot drift; provenance
  and program inventories are frozen the same way; specifications, generated
  root modules and locks all use one canonical package order; verify
  reports the path check it actually performs.

• Refresh storage status honestly: aliases, usage timestamps and object
  counts are re-read on every call while the expensive size accounting stays
  cached, and shared package builds invalidate that cache explicitly. The
  header-snapshot cache keys by the compiler binary's identity, not its
  spelling.

• Consolidate result construction: one conversion from process outcome to
  ExecutionResult, exclusive timing phases (a dependency build before a
  retried check now reports preliminary_check and build separately), a
  failed support module keeps every earlier support transcript, profile
  keeps the failing warmup, and a process killed by a signal reports the new
  crashed verdict rather than rejected.

• Progress observers are strictly observational: a failing callback is
  recorded on the emitter and never fails or rolls back an operation; the
  console renderer always shuts down; repeated counted operations with the
  same label print their checkpoints again; lean-run error messages name
  the flags the parser actually accepts.

• Extract shared primitives into internal modules (_archive, _platform,
  _sources, _project_identity, _git, _process, _transaction,
  _relpath, _results, _cancellation) so high-level modules no longer
  serve as each other's utility libraries.

• Shorten source-build environment staging names so deeply nested Mathlib
  artifacts remain below legacy MAX_PATH while leantar hydrates the cache
  on Windows. The previous PID plus full-UUID name put some artifacts at
  exactly 260 characters, where hydration failed with os error 3 and forced
  users toward a full Mathlib source build.

• Hydrate Mathlib's upstream build cache when new has no exact shared project
  or downloadable environment to seed from. The cold-start fallback previously
  opened the catalog environment without enabling the trusted URL-keyed
  accelerator, so it skipped lake exe cache get and compiled all of Mathlib
  from source.

v4.33.0

• Cover the remaining silent phases with progress. Elan bootstrap and
  elan toolchain install, and the lake init/lake update behind new, now
  stream their output as process.progress/process.output like every other
  subprocess. Long pure-Python loops report counted progress that renders as a
  bar: verification.inventory (hashing build artifacts in verify),
  bundle.tree_inventory (env export/import), source.snapshot_digest
  (source fingerprints, including path dependencies during adopt), and
  capsule.import_parse. The publish preflight fetch
  (publish.remote_probe_started) and the Lake configuration read behind
  project-wide check (project.config_translate_started) announce
  themselves. Any event carrying current/total and a label now renders as
  a counted bar without a dedicated console handler, and deep helpers reach
  the active runtime's emitter through lean_runtime.events.current().
• Re-running adopt over a tree no longer re-probes every already attached
  project (a Lake graph load each, up to two minutes for Mathlib); the plan
  already reports them as attached and verify re-checks links. Attachment
  now announces adopt.attach_started per project, rendered as
  Attaching projects [bar] i/n, and the pre-swap Lake graph probe streams its
  output like every other Lake invocation instead of running silently.

v4.30.0

• Attach shared dependencies on Windows without administrator rights. Creating
  a symbolic link needs SeCreateSymbolicLinkPrivilege (administrators or
  Developer Mode), so adopt and project attach failed with
  WinError 1314: A required privilege is not held by the client on a normal
  account, and the pre-attach probe never caught it. When symlink creation is
  denied, the package link is now created as a directory junction, which any
  user may create and which Lake and Git traverse identically. Every place
  that recognizes an attached package as a link (status, verify,
  unshare, adoption planning, rollback, source fingerprinting) now
  recognizes junctions too.
• Size local dependency checkouts during adopt without descending into
  attached links, using one directory scan per level instead of rglob.
• Show progress while subprocesses run. Lake's [n/m] build steps now stream
  from check, build, and artifact hydration as process.progress events
  (rate-limited to ten per second), rendered on a terminal as one in-place bar
  (lake [████░░░░] 3300/8318 · Building Mathlib.Foo) and in logs as 25%
  checkpoints; every other output line becomes a throttled process.output
  heartbeat shown in place on a terminal, so lake exe cache get is no longer
  silent. Third-party backends that do not accept the new optional on_output
  callback keep working unchanged.
• Announce counted phases that used to be silent: adopt.inspect_started and
  adopt.identity_started for each project during adoption planning, and
  project.detach.package_started for each package unshare materializes; all
  carry current/total and render as the same counted bar.
• Keep the terminal alive during any silent stretch: when no event has arrived
  for two seconds the console shows ⋯ <last activity> (Ns) in place; plain
  logs print Still working: … after ten seconds and then every thirty.
• Name new shared package directories pkg_<32 hex> instead of
  project_package_<64 hex>. The 80-character name pushed Mathlib's deepest
  build outputs past Windows' 260-character path limit, so an adopted Mathlib
  project could hydrate its cache but never finish build
  (failed to create file '…\Isometric.olean.server'). The digest is the same
  identity truncated to 128 bits; existing project_package_* directories stay
  valid and reusable. To move already adopted projects onto short paths,
  lean-runtime project unshare each of them, delete the legacy
  project-packages/project_package_* directories (nothing references them once
  every project is unshared; clean does not yet reclaim them), and
  lean-runtime adopt again.
• Windows correctness fixes surfaced by running the suite on Windows:
  compact source snapshots stage under a shorter directory name so Git's
  shallow-clone metadata stays below MAX_PATH ('$GIT_DIR' too big);
  lean-runtime run rewrites a container backend's POSIX staged path back to
  the user's file on Windows hosts; lock waiters learn the holding operation
  through a .owner sidecar (a byte-locked file cannot be read on Windows);
  declaration shards close their SQLite connection before publication so the
  rename succeeds; storage deduplicates hard links via os.stat() because
  DirEntry.stat() reports no inode on Windows; publish accepts a
  drive-letter origin path (C:\...) instead of treating C as a URL scheme;
  bundle import accepts CRLF working files whose LF-normalized blob is the
  recorded object (core.autocrlf); and storage cleanup clamps negative file
  ages from filesystem timestamp granularity.

v4.27.0

• Fingerprint a project by what Lake compiles, not by everything beside the
  lakefile. The workspace digest that keys header snapshots and provenance now
  hashes lakefile.toml/lakefile.lean, lean-toolchain, lake-manifest.json,
  and the .lean files under each declared target's module roots (the whole
  tree, minus .git and .lake, when the lakefile is not declarative).
  Previously every byte under the project root was read on each check and
  build, so a lakefile above a data directory, a virtual environment, or an
  unrelated monorepo made the first step of a check run for minutes with no
  output. Digests change value once because of this.
• Announce project fingerprinting as project.fingerprint_started and
  project.fingerprint_finished events (phase fingerprint, with
  elapsed_ms), so --verbose never goes silent between check.started and
  the first Lake invocation.

v4.26.0

• Stop status claiming a download is required for core-only files. A lock
  without packages runs straight on the toolchain and never materializes an
  environment in the store, so readiness and cost are now judged by the
  toolchain alone: status reports environment ready locally and
  Download none once the toolchain is installed, and status --probe
  prices it as zero instead of unknown. Previously the store directory that
  check never creates kept the row at not local · Download required.

v4.25.0

• Pin the Elan build that automatic bootstrap installs. Bootstrap now
  downloads the v4.2.3 release archive for the host platform directly from
  the Elan releases, verifies its SHA-256, and runs its elan-init, instead of
  running the installer script that always fetched releases/latest. Two
  machines on the same Lean Runtime version therefore get the same Elan.
• Retry elan toolchain install up to two more times when Elan reports a
  transient download failure (dropped connection, TLS handshake error,
  timeout), announcing each retry as a toolchain.install_retry event. Unknown
  toolchains and disk errors still fail immediately.
• State the model up front: lean-runtime --help, the docs index, and the
  command reference now open with the four nouns (context, environment, lock,
  verdict) and the rule that discovery proposes an environment while only Lean
  accepts it.
• Make status a dry run of check. A standalone file reports its context
  source and confidence (proposed for discovery, exact for a project, lock,
  or stored environment), the candidates in the order check would try them,
  whether each environment and toolchain is already local, and whether a
  download is needed; status --probe prices the first download.
• Report Lean's answer as a first-class verdict (accepted, rejected, or
  not_run) in execution results, --json output (data.verdict), and the
  --matrix table, and attribute every human-readable verdict to the exact
  environment it was produced in.
• Wrap status --json in a lean-runtime.status/v1 envelope like every other
  machine-readable command. Scripts that read the bare object must now read
  data.
• Apply one mutation rule everywhere: toolchain optimize --prune-original,
  env publish, toolchain publish, program publish, and
  declaration-index publish now describe the change and require --yes or an
  interactive confirmation, exiting with code 2 non-interactively otherwise.
• Separate the vocabulary of context (where the decision comes from) and
  environment (what was chosen) across help text and documentation;
  check --help and status --help now describe the model, --using takes
  an ENVIRONMENT, and the generated AGENTS.md opens with the same model
  plus the status dry run and the --yes rule.
• Improve Windows checks by reusing Elan from PATH, recognizing native
  .exe toolchain binaries, and running core-only discovery directly against
  its exact Lean toolchain when no platform environment artifact is needed.
• Treat files outside every declared lakefile.toml target as standalone even
  when they sit below a pinned project, add check --standalone as an explicit
  override, and explain ignored parent projects in status.

v4.24.0

• Key shared Lake package artifacts by the exact installed Lean and Lake
  executable digests. Existing /1 package artifacts are source-only donors;
  the first build of each project re-shares artifacts under the /2 key.
• Let an exact registered dependency graph donate source across toolchain
  versions, while stripping its build tree, and refresh existing project
  attachments when their computed workspace identity changes.
• Report obsolete /1 project artifacts in doctor, reclaim them through
  clean, and refuse publishing moving toolchain spellings such as master
  or undated nightly. Publication also fails early when its input is an
  acquired sparse capsule rather than a source build.

v4.23.0

v4.23.0

v4.22.0

v4.22.0

v4.21.0

v4.21.0