Changelog

leanprover/lean4 · · 4 commits

Shake explanations get precise dependency reasons

Lean improves `lake shake --explain`, fixes `--plugin` parsing on Windows, and updates CI plus stage0 artifacts.

lake shake --explain now names why deps stick (Kha1708293)

lake shake --explain now reports precise preservation reasons beyond direct references, including shake: keep, --keep-public, --add-only/--only/shake: keep-all, --keep-downstream, --add-public, --keep-prefix, import all, and folder-nested imports. That makes shake output much more actionable when diagnosing why a module remains in the dependency graph.

--plugin switches to file=fn to avoid Windows path clashes (tydeuf8b7f30)

Lean changes the plugin initialization syntax from file:fn to file=fn, which avoids ambiguity with Windows drive-letter colons. The help text, parser, and plugin test were updated together so the new form is the supported CLI contract.

Other misc changes

  • CI: fix jira-sync workflow (#13739) (Kha2acdaaf)
  • Update stage0 artifacts (6749463)