You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.