Changelog

leanprover/lean4 · · 10 commits

Lean adds richer lint hints and tactic replay speedups

New hints for unused bindings and simp args, plus a major incremental-elaboration fix that avoids rerunning tactics on trailing whitespace changes.

Kha wkrozowski hargoniX Vtec234

Replay tactics when only trailing whitespace changes (Kha8554442)

Lean now avoids rerunning tactics when you edit only whitespace immediately after them, preserving progress while typing the next step. The change threads stripped trailing whitespace through the snapshot tree and reapplies it on access, with broad updates across elaboration and language snapshot code.

Unused variables linter now suggests underscore-prefixing (wkrozowski6b303d9)

The unusedVariables linter now emits a hint that suggests prefixing the binding with _, making the warning more actionable. This improves the UX of a common lint by showing the exact fix directly in the message.

Unused simp args hint now renders a cleaner edit (wkrozowski81074d1)

The UnusedSimpArgs linter now produces a hint with .none diff granularity, so the suggested edit is displayed more clearly. The tests were updated to reflect the new [apply]-style hint rendering.

Other misc changes

  • Added Insert instances for NameMap and NameSet (Vtec234c1d6de5)
  • Fixed namespacing in DeprecatedModule (wkrozowskid14ff0b)
  • Disabled binary stripping in release CMake config (hargoniX306bbbc)
  • Re-enabled header snapshots in CI (Kha6405ec1)
  • Tweaked CI to skip stack-overflowing tests under fsanitize (Khae90c70f)
  • Adjusted PR release tag pushes to negotiate common objects first (Khafedd162)
  • Disabled Lake cache when PREV_STAGE is used (Kha86b7320)