v4.14.0-rc2

fix: do not link statically against pthread/dl/rt (#5966)

v4.14.0-rc1

chore: set LEAN_VERSION_IS_RELEASE

v4.13.0

Full Changelog: v4.12.0...v4.13.0

Language features, tactics, and metaprograms

• structure command

  • #5511 allows structure parents to be type synonyms.
  • #5531 allows default values for structure fields to be noncomputable.

• rfl and apply_rfl tactics

  • #3714, #3718 improve the rfl tactic and give better error messages.
  • #3772 makes rfl no longer use kernel defeq for ground terms.
  • #5329 tags Iff.refl with @[refl] (@Parcly-Taxel)
  • #5359 ensures that the rfl tactic tries Iff.rfl (@Parcly-Taxel)

• unfold tactic

  • #4834 let unfold do zeta-delta reduction of local definitions, incorporating functionality of the Mathlib unfold_let tactic.

• omega tactic

  • #5382 fixes spurious error in #5315
  • #5523 supports Int.toNat

• simp tactic

  • #5479 lets simp apply rules with higher-order patterns.

• induction tactic

  • #5494 fixes induction’s "pre-tactic" block to always be indented, avoiding unintended uses of it.

• ac_nf tactic

  • #5524 adds ac_nf, a counterpart to ac_rfl, for normalizing expressions with respect to associativity and commutativity. Tests it with BitVec expressions.

• bv_decide

  • #5211 makes extractLsb' the primitive bv_decide understands, rather than extractLsb (@alexkeizer)
  • #5365 adds bv_decide diagnoses.
  • #5375 adds bv_decide normalization rules for ofBool (a.getLsbD i) and ofBool a[i] (@alexkeizer)
  • #5423 enhances the rewriting rules of bv_decide
  • #5433 presents the bv_decide counterexample at the API
  • #5484 handles BitVec.ofNat with Nat fvars in bv_decide
  • #5506, #5507 add bv_normalize rules.
  • #5568 generalize the bv_normalize pipeline to support more general preprocessing passes
  • #5573 gets bv_normalize up-to-date with the current BitVec rewrites
  • Cleanups: #5408, #5493, #5578

• Elaboration improvements

  • #5266 preserve order of overapplied arguments in elab_as_elim procedure.
  • #5510 generalizes elab_as_elim to allow arbitrary motive applications.
  • #5283, #5512 refine how named arguments suppress explicit arguments. Breaking change: some previously omitted explicit arguments may need explicit _ arguments now.
  • #5376 modifies projection instance binder info for instances, making parameters that are instance implicit in the type be implicit.
  • #5402 localizes universe metavariable errors to let bindings and fun binders if possible. Makes "cannot synthesize metavariable" errors take precedence over unsolved universe level errors.
  • #5419 must not reduce ite in the discriminant of match-expression when reducibility setting is .reducible
  • #5474 have autoparams report parameter/field on failure
  • #5530 makes automatic instance names about types with hygienic names be hygienic.

• Deriving handlers

  • #5432 makes Repr deriving instance handle explicit type parameters

• Functional induction

  • #5364 adds more equalities in context, more careful cleanup.

• Linters

  • #5335 fixes the unused variables linter complaining about match/tactic combinations
  • #5337 fixes the unused variables linter complaining about some wildcard patterns

• Other fixes

  • #4768 fixes a parse error when .. appears with a . on the next line

• Metaprogramming

  • #3090 handles level parameters in Meta.evalExpr (@eric-wieser)
  • #5401 instance for Inhabited (TacticM α) (@alexkeizer)
  • #5412 expose Kernel.check for debugging purposes
  • #5556 improves the "invalid projection" type inference error in inferType.
  • #5587 allows MVarId.assertHypotheses to set BinderInfo and LocalDeclKind.
  • #5588 adds MVarId.tryClearMany', a variant of MVarId.tryClearMany.

Language server, widgets, and IDE extensions

• #5205 decreases the latency of auto-completion in tactic blocks.
• #5237 fixes symbol occurrence highlighting in VS Code not highlighting occurrences when moving the text cursor into the identifier from the right.
• #5257 fixes several instances of incorrect auto-completions being reported.
• #5299 allows auto-completion to report completions for global identifiers when the elaborator fails to provide context-specific auto-completions.
• #5312 fixes the server breaking when changing whitespace after the module header.
• #5322 fixes several instances of auto-completion reporting non-existent namespaces.
• #5428 makes sure to always report some recent file range as progress when waiting for elaboration.

Pretty printing

• #4979 make pretty printer escape identifiers that are tokens.
• #5389 makes formatter use the current token table.
• #5513 use breakable instead of unbreakable whitespace when formatting tokens.

Library

• #5222 reduces allocations in Json.compress.

• #5231 upstreams Zero and NeZero

• #5292 refactors Lean.Elab.Deriving.FromToJson (@arthur-adjedj)

• #5415 implements Repr Empty (@TomasPuverle)

• #5421 implements To/FromJSON Empty (@TomasPuverle)

• Logic

  • #5263 allows simplifying dite_not/decide_not with only Decidable (¬p).
  • #5268 fixes binders on ite_eq_left_iff
  • #5284 turns off Inhabited (Sum α β) instances
  • #5355 adds simp lemmas for LawfulBEq
  • #5374 add Nonempty instances for products, allowing more partial functions to elaborate successfully
  • #5447 updates Pi instance names
  • #5454 makes some instance arguments implicit
  • #5456 adds heq_comm
  • #5529 moves @[simp] from exists_prop' to exists_prop

• Bool

  • #5228 fills gaps in Bool lemmas
  • #5332 adds notation ^^ for Bool.xor
  • #5351 removes _root_.and (and or/not/xor) and instead exports/uses Bool.and (etc.).

• BitVec

  • #5240 removes BitVec simps with complicated RHS
  • #5247 BitVec.getElem_zeroExtend
  • #5248 simp lemmas for BitVec, improving confluence
  • #5249 removes @[simp] from some BitVec lemmas
  • #5252 changes BitVec.intMin/Max from abbrev to def
  • [#5278](https://...

v4.13.0-rc4

fix: do not force snapshot tree too early (#5752)

This turns out to be the issue behind #5736, though really it is yet
another indicator of a general thread pool weakness.

(cherry picked from commit fc5e3cc66e3f317a03a17d9b19cc8d6476cf31cd)

v4.13.0-rc3

Reapply "refactor: reduce Reservoir build fetch attempts & warnings (…

v4.13.0-rc2

Revert "feat: lake: Reservoir build cache (#5486)"

This reverts commit ffb4c5becf89d57560dd6f48f7693b2fdb9de6f9.

revert_lake_changes

Revert "feat: lake: Reservoir build cache (#5486)"

This reverts commit ffb4c5becf89d57560dd6f48f7693b2fdb9de6f9.

v4.13.0-rc1

chore: update CMakeLists.txt

v4.12.0

v4.12.0

Language features, tactics, and metaprograms

• bv_decide tactic. This release introduces a new tactic for proving goals involving BitVec and Bool. It reduces the goal to a SAT instance that is refuted by an external solver, and the resulting LRAT proof is checked in Lean. This is used to synthesize a proof of the goal by reflection. As this process uses verified algorithms, proofs generated by this tactic use Lean.ofReduceBool, so this tactic includes the Lean compiler as part of the trusted code base. The external solver CaDiCaL is included with Lean and does not need to be installed separately to make use of bv_decide.

  For example, we can use bv_decide to verify that a bit twiddling formula leaves at most one bit set:

  def popcount (x : BitVec 64) : BitVec 64 :=
    let rec go (x pop : BitVec 64) : Nat → BitVec 64
      | 0 => pop
      | n + 1 => go (x >>> 2) (pop + (x &&& 1)) n
    go x 0 64
  
  example (x : BitVec 64) : popcount ((x &&& (x - 1)) ^^^ x) ≤ 1 := by
    simp only [popcount, popcount.go]
    bv_decide

  When the external solver fails to refute the SAT instance generated by bv_decide, it can report a counterexample:

  /--
  error: The prover found a counterexample, consider the following assignment:
  x = 0xffffffffffffffff#64
  -/
  #guard_msgs in
  example (x : BitVec 64) : x < x + 1 := by
    bv_decide

  See Lean.Elab.Tactic.BVDecide for a more detailed overview, and look in tests/lean/run/bv_* for examples.

  #5013, #5074, #5100, #5113, #5137, #5203, #5212, #5220.

• simp tactic

  • #4988 fixes a panic in the reducePow simproc.
  • #5071 exposes the index option to the dsimp tactic, introduced to simp in #4202.
  • #5159 fixes a panic at Fin.isValue simproc.
  • #5167 and #5175 rename the simpCtorEq simproc to reduceCtorEq and makes it optional. (See breaking changes.)
  • #5187 ensures reduceCtorEq is enabled in the norm_cast tactic.
  • #5073 modifies the simp debug trace messages to tag with "dpre" and "dpost" instead of "pre" and "post" when in definitional rewrite mode. #5054 explains the reduce steps for trace.Debug.Meta.Tactic.simp trace messages.

• ext tactic

  • #4996 reduces default maximum iteration depth from 1000000 to 100.

• induction tactic

  • #5117 fixes a bug where let bindings in minor premises wouldn't be counted correctly.

• omega tactic

  • #5157 fixes a panic.

• conv tactic

  • #5149 improves arg n to handle subsingleton instance arguments.

• #5044 upstreams the #time command.

• #5079 makes #check and #reduce typecheck the elaborated terms.

• Incrementality

  • #4974 fixes regression where we would not interrupt elaboration of previous document versions.
  • #5004 fixes a performance regression.
  • #5001 disables incremental body elaboration in presence of where clauses in declarations.
  • #5018 enables infotrees on the command line for ilean generation.
  • #5040 and #5056 improve performance of info trees.
  • #5090 disables incrementality in the case .. | .. tactic.
  • #5312 fixes a bug where changing whitespace after the module header could break subsequent commands.

• Definitions

  • #5016 and #5066 add clean_wf tactic to clean up tactic state in decreasing_by. This can be disabled with set_option debug.rawDecreasingByGoal false.
  • #5055 unifies equational theorems between structural and well-founded recursion.
  • #5041 allows mutually recursive functions to use different parameter names among the “fixed parameter prefix”
  • #4154 and #5109 add fine-grained equational lemmas for non-recursive functions. See breaking changes.
  • #5129 unifies equation lemmas for recursive and non-recursive definitions. The backward.eqns.deepRecursiveSplit option can be set to false to get the old behavior. See breaking changes.
  • #5141 adds f.eq_unfold lemmas. Now Lean produces the following zoo of rewrite rules:

    Option.map.eq_1      : Option.map f none = none
    Option.map.eq_2      : Option.map f (some x) = some (f x)
    Option.map.eq_def    : Option.map f p = match o with | none => none | (some x) => some (f x)
    Option.map.eq_unfold : Option.map = fun f p => match o with | none => none | (some x) => some (f x)
    

    The f.eq_unfold variant is especially useful to rewrite with rw under binders.
  • #5136 fixes bugs in recursion over predicates.

• Variable inclusion

  • #5206 documents that include currently only applies to theorems.

• Elaboration

  • #4926 fixes a bug where autoparam errors were associated to an incorrect source position.
  • #4833 fixes an issue where cdot anonymous functions (e.g. (· + ·)) would not handle ambiguous notation correctly. Numbers the parameters, making this example expand as fun x1 x2 => x1 + x2 rather than fun x x_1 => x + x_1.
  • #5037 improves strength of the tactic that proves array indexing is in bounds.
  • #5119 fixes a bug in the tactic that proves indexing is in bounds where it could loop in the presence of mvars.
  • #5072 makes the structure type clickable in "not a field of structure" errors for structure instance notation.
  • #4717 fixes a bug where mutual inductive commands could create terms that the kernel rejects.
  • #5142 fixes a bug where variable could fail when mixing binder updates and declarations.

• Other fixes or improvements

  • #5118 changes the definition of the syntheticHole parser so that hovering over _ in ?_ gives the docstring for synthetic holes.
  • #5173 uses the emoji variant selector for ✅️,❌️,💥️ in messages, improving fonts selection.
  • #5183 fixes a bug in rename_i where implementation detail hypotheses could be renamed.

Language server, widgets, and IDE extensions

• #4821 resolves two language server bugs that especially affect Windows users. (1) Editing the header could result in the watchdog not correctly restarting the file worker, which would lead to the file seemingly being processed forever. (2) On an especially slow Windows machine, we found that starting the language server would sometimes not succeed at all. This PR also resolves an issue where we would not correctly emit messages that we received while the file worker is being restarted to the corresponding file worker after the restart.
• #5006 updates the user widget manual.
• #5193 updates the quickstart guide with the new display name for the Lean 4 extension ("Lean 4").
• #5185 fixes a bug where over time "import out of date" messages would accumulate.
• #4900 improves ilean loading performance by about a factor of two. Optimizes the JSON parser and the conversion from JSON to Lean data structures; see PR description for details.
• Other fixes or improvements
  • #5031 localizes an instance in Lsp.Diagnostics.

Pretty printing

• #4976 introduces @[app_delab], a macro for creating delaborators for particular constants. The @[app_delab ident] syntax resolves ident to its constant name name and th...

v4.12.0-rc1

chore: use `Expr.numObjs` instead of `lean_expr_size_shared` (#5239)

Remark: declarations like `sizeWithSharing` must be in `IO` since they
are not functions.

The commit also uses the more efficient `ShareCommon.shareCommon'`.