• simp [f] does not unfold partial applications of f anymore. See issue #2042. To fix proofs affected by this change, use unfold f or simp (config := { unfoldPartialApp := true }) [f].

• By default, simp will no longer try to use Decidable instances to rewrite terms. In particular, not all decidable goals will be closed by simp, and the decide tactic may be useful in such cases. The decide simp configuration option can be used to locally restore the old simp behavior, as in simp (config := {decide := true}); this includes using Decidable instances to verify side goals such as numeric inequalities.

• Many bug fixes:

  • Add left/right actions to term tree coercion elaborator and make `^`` a right action

  • Fix for #2775, don't catch max recursion depth errors

  • Reduction of Decidable instances very slow when using cases tactic

  • simp not rewriting in binder

  • simp unfolding let even with zeta := false option

  • simp (with beta/zeta disabled) and discrimination trees

  • unknown free variable introduced by rw ... at h

  • dsimp doesn't use rfl theorems which consist of an unapplied constant

  • dsimp does not close reflexive equality goals if they are wrapped in metadata

  • rw [h] uses h from the environment in preference to h from the local context

  • missing withAssignableSyntheticOpaque for assumption tactic

  • ignoring default value for field warning

• Cancel outstanding tasks on document edit in the language server.

• Remove unnecessary % operations in Fin.mod and Fin.div

• Avoid DecidableEq in Array.mem

• Ensure USize.size unifies with ?m + 1

• Improve compatibility with emacs eglot client

Lake:

• Sensible defaults for lake new MyProject math

• Changed postUpdate? configuration option to a post_update declaration. See the post_update syntax docstring for more information on the new syntax.

• A manifest is automatically created on workspace load if one does not exists..

• The := syntax for configuration declarations (i.e., package, lean_lib, and lean_exe) has been deprecated. For example, package foo := {...} is deprecated.

• support for overriding package URLs via LAKE_PKG_URL_MAP

• Moved the default build directory (e.g., build), default packages directory (e.g., lake-packages), and the compiled configuration (e.g., lakefile.olean) into a new dedicated directory for Lake outputs, .lake. The cloud release build archives are also stored here, fixing #2713.

• Update manifest format to version 7 (see lean4#2801 for details on the changes).

• Deprecate the manifestFile field of a package configuration.

• There is now a more rigorous check on lakefile.olean compatibility (see #2842 for more details).