v4.16.0-rc1

v4.16.0

Language

• #3696 makes all message constructors handle pretty printer errors.

• #4460 runs all linters for a single command (together) on a separate
  thread from further elaboration, making a first step towards
  parallelizing the elaborator.

• #5757 makes it harder to create "fake" theorems about definitions that
  are stubbed-out with sorry by ensuring that each sorry is not
  definitionally equal to any other. For example, this now fails:

example : (sorry : Nat) = sorry := rfl -- fails

However, this still succeeds, since the sorry is a single
indeterminate Nat:

def f (n : Nat) : Nat := sorry
example : f 0 = f 1 := rfl -- succeeds

One can be more careful by putting parameters to the right of the colon:

def f : (n : Nat) → Nat := sorry
example : f 0 = f 1 := rfl -- fails

Most sources of synthetic sorries (recall: a sorry that originates from
the elaborator) are now unique, except for elaboration errors, since
making these unique tends to cause a confusing cascade of errors. In
general, however, such sorries are labeled. This enables "go to
definition" on sorry in the Infoview, which brings you to its origin.
The option set_option pp.sorrySource true causes the pretty printer to
show source position information on sorries.

• #6123 ensures that the configuration in Simp.Config is used when
  reducing terms and checking definitional equality in simp.

• #6204 lets _ be used in numeric literals as a separator. For
  example, 1_000_000, 0xff_ff or 0b_10_11_01_00. New lexical syntax:

numeral10 : [0-9]+ ("_"+ [0-9]+)*
numeral2  : "0" [bB] ("_"* [0-1]+)+
numeral8  : "0" [oO] ("_"* [0-7]+)+
numeral16 : "0" [xX] ("_"* hex_char+)+
float     : numeral10 "." numeral10? [eE[+-]numeral10]

• #6270 fixes a bug that could cause the injectivity tactic to fail in
  reducible mode, which could cause unfolding lemma generation to fail
  (used by tactics such as unfold). In particular,
  Lean.Meta.isConstructorApp'? was not aware that n + 1 is equivalent
  to Nat.succ n.

• #6273 modifies the "foo has been deprecated: use betterFoo instead"
  warning so that foo and betterFoo are hoverable.

• #6278 enables simp configuration options to be passed to norm_cast.

• #6286 ensure bv_decide uses definitional equality in its reflection
  procedure as much as possible. Previously it would build up explicit
  congruence proofs for the kernel to check. This reduces the size of
  proof terms passed to kernel speeds up checking of large reflection
  proofs.

• #6288 uses Lean.RArray in bv_decide's reflection proofs. Giving
  speedups on problems with lots of variables.

• #6295 sets up simprocs for all the remaining operations defined in
  Init.Data.Fin.Basic

• #6300 adds the debug.proofAsSorry option. When enabled, the proofs
  of theorems are ignored and replaced with sorry.

• #6330 removes unnecessary parameters from the funcion induction
  principles. This is a breaking change; broken code can typically be adjusted
  simply by passing fewer parameters.

• #6330 removes unnecessary parameters from the funcion induction
  principles. This is a breaking change; broken code can typically be adjusted
  simply by passing fewer parameters.

• #6362 adds the --error=kind option (shorthand: -Ekind) to the
  lean CLI. When set, messages of kind (e.g.,
  linter.unusedVariables) will be reported as errors. This setting does
  nothing in interactive contexts (e.g., the server).

• #6366 adds support for Float32 and fixes a bug in the runtime.

• #6375 fixes a bug in the simplifier. It was producing terms with loose
  bound variables when eliminating unused let_fun expressions.

• #6378 adds an explanation to the error message when cases and
  induction are applied to a term whose type is not an inductive type.
  For Prop, these tactics now suggest the by_cases tactic. Example:

tactic 'cases' failed, major premise type is not an inductive type
  Prop

• #6381 fixes a bug in withTrackingZetaDelta and
  withTrackingZetaDeltaSet. The MetaM caches need to be reset. See new
  test.

• #6385 fixes a bug in simp_all? that caused some local declarations
  to be omitted from the Try this: suggestions.

• #6386 ensures that revertAll clears auxiliary declarations when
  invoked directly by users.

• #6387 fixes a type error in the proof generated by the contradiction
  tactic.

• #6397 ensures that simp and dsimp do not unfold definitions that
  are not intended to be unfolded by the user. See issue #5755 for an
  example affected by this issue.

• #6398 ensures Meta.check check projections.

• #6412 adds reserved names for congruence theorems used in the
  simplifier and grind tactics. The idea is prevent the same congruence
  theorems to be generated over and over again.

• #6413 introduces the following features to the WIP grind tactic:

• Expr internalization.
• Congruence theorem cache.
• Procedure for adding new facts
• New tracing options
• New preprocessing steps: fold projections and eliminate dangling
  Expr.mdata

• #6414 fixes a bug in Lean.Meta.Closure that would introduce
  under-applied delayed assignment metavariables, which would keep them
  from ever getting instantiated. This bug affected match elaboration
  when the expected type contained postponed elaboration problems, for
  example tactic blocks.

• #6419 fixes multiple bugs in the WIP grind tactic. It also adds
  support for printing the grind internal state.

• #6428 adds a new preprocessing step to the grind tactic:
  universe-level normalization. The goal is to avoid missing equalities in
  the congruence closure module.

• #6430 adds the predicate Expr.fvarsSet a b, which returns true if
  and only if the free variables in a are a subset of the free variables
  in b.

• #6433 adds a custom type and instance canonicalizer for the (WIP)
  grind tactic. The grind tactic uses congruence closure but
  disregards types, type formers, instances, and proofs. Proofs are
  ignored due to proof irrelevance. Types, type formers, and instances are
  considered supporting elements and are not factored into congruence
  detection. Instead, grind only checks whether elements are
  structurally equal, which, in the context of the grind tactic, is
  equivalent to pointer equality. See new tests for examples where the
  canonicalizer is important.

• #6435 implements the congruence table for the (WIP) grind tactic. It
  also fixes several bugs, and adds a new preprocessing step.

• #6437 adds support for detecting congruent terms in the (WIP) grind
  tactic. It also introduces the grind.debug option, which, when set to
  true, checks many invariants after each equivalence class is merged.
  This option is intended solely for debugging purposes.

• #6438 ensures norm_cast doesn't fail to act in the presence of
  no_index annotations

• #6441 adds basic truth value propagation rules to the (WIP) grind
  tactic.

• #6442 fixes the checkParents sanity check in grind.

• #6443 adds support for propagating the truth value of equalities in
  the (WIP) grind tactic.

• #6447 refactors grind and adds support for invoking the simplifier
  using the GrindM monad.

• #6448 declares the command builtin_grind_propagator for registering
  equation propagator for grind. It also declares the auxiliary the
  attribute.

• #6449 completes the implementation of the command
  builtin_grind_propagator.

• #6452 adds support for generating (small) proofs for any two
  expressions that belong to the same equivalence class in the grind
  tactic state.

• #6453 improves bv_decide's performance in the presence of large
  literals.

• #6455 fixes a bug in the equality pro...

v4.15.0

Language

• #4595 implements Simp.Config.implicitDefEqsProofs. When true
  (default: true), simp will not create a proof term for a
  rewriting rule associated with an rfl-theorem. Rewriting rules are
  provided by users by annotating theorems with the attribute @[simp].
  If the proof of the theorem is just rfl (reflexivity), and
  implicitDefEqProofs := true, simp will not create a proof term
  which is an application of the annotated theorem.

• #5429 avoid negative environment lookup

• #5501 ensure instantiateMVarsProfiling adds a trace node

• #5856 adds a feature to the the mutual def elaborator where the
  instance command yields theorems instead of definitions when the class
  is a Prop.

• #5907 unset trailing for simpa? "try this" suggestion

• #5920 changes the rule for which projections become instances. Before,
  all parents along with all indirect ancestors that were represented as
  subobject fields would have their projections become instances. Now only
  projections for direct parents become instances.

• #5934 make all_goals admit goals on failure

• #5942 introduce synthetic atoms in bv_decide

• #5945 adds a new definition Message.kind which returns the top-level
  tag of a message. This is serialized as the new field kind in
  SerialMessaege so that i can be used by external consumers (e.g.,
  Lake) to identify messages via lean --json.

• #5968 arg conv tactic misreported number of arguments on error

• #5979 BitVec.twoPow in bv_decide

• #5991 simplifies the implementation of omega.

• #5992 fix style in bv_decide normalizer

• #5999 adds configuration options for
  decide/decide!/native_decide and refactors the tactics to be
  frontends to the same backend. Adds a +revert option that cleans up
  the local context and reverts all local variables the goal depends on,
  along with indirect propositional hypotheses. Makes native_decide fail
  at elaboration time on failure without sacrificing performance (the
  decision procedure is still evaluated just once). Now native_decide
  supports universe polymorphism.

• #6010 changes bv_decide's configuration from lots of set_option to
  an elaborated config like simp or omega. The notable exception is
  sat.solver which is still a set_option such that users can configure
  a custom SAT solver globally for an entire project or file. Additionally
  it introduces the ability to set maxSteps for the simp preprocessing
  run through the new config.

• #6012 improves the validation of new syntactic tokens. Previously, the
  validation code had inconsistencies: some atoms would be accepted only
  if they had a leading space as a pretty printer hint. Additionally,
  atoms with internal whitespace are no longer allowed.

• #6016 removes the decide! tactic in favor of decide +kernel
  (breaking change).

• #6019 removes @[specilize] from MkBinding.mkBinding, which is a
  function that cannot be specialized (as none of its arguments are
  functions). As a result, the specializable function Nat.foldRevM.loop
  doesn't get specialized, which leads to worse performing code.

• #6022 makes the change tactic and conv tactic use the same
  elaboration strategy. It works uniformly for both the target and local
  hypotheses. Now change can assign metavariables, for example:

example (x y z : Nat) : x + y = z := by
  change ?a = _
  let w := ?a
  -- now `w : Nat := x + y`

• #6024 fixes a bug where the monad lift coercion elaborator would
  partially unify expressions even if they were not monads. This could be
  taken advantage of to propagate information that could help elaboration
  make progress, for example the first change worked because the monad
  lift coercion elaborator was unifying @Eq _ _ with @Eq (Nat × Nat) p:

example (p : Nat × Nat) : p = p := by
  change _ = ⟨_, _⟩ -- used to work (yielding `p = (p.fst, p.snd)`), now it doesn't
  change ⟨_, _⟩ = _ -- never worked

As such, this is a breaking change; you may need to adjust expressions
to include additional implicit arguments.

• #6029 adds a normalization rule to bv_normalize (which is used by
  bv_decide) that converts x / 2^k into x >>> k under suitable
  conditions. This allows us to simplify the expensive division circuits
  that are used for bitblasting into much cheaper shifting circuits.
  Concretely, it allows for the following canonicalization:

• #6030 fixes simp only [· ∈ ·] after #5020.

• #6035 introduces the and flattening pre processing pass from Bitwuzla
  to bv_decide. It splits hypotheses of the form (a && b) = true into
  a = true and b = true which has synergy potential with the already
  existing embedded constraint substitution pass.

• #6037 fixes bv_decide's embedded constraint substitution to generate
  correct counter examples in the corner case where duplicate theorems are
  in the local context.

• #6045 add LEAN_ALWAYS_INLINE to some functions

• #6048 fixes simp? suggesting output with invalid indentation

• #6051 mark Meta.Context.config as private

• #6053 fixes the caching infrastructure for whnf and isDefEq,
  ensuring the cache accounts for all relevant configuration flags. It
  also cleans up the WHNF.lean module and improves the configuration of
  whnf.

• #6061 adds a simp_arith benchmark.

• #6062 optimize Nat.Linear.Expr.toPoly

• #6064 optimize Nat.Linear.Poly.norm

• #6068 improves the asymptotic performance of simp_arith when there are many variables to consider.

• #6077 adds options to bv_decide's configuration structure such that
  all non mandatory preprocessing passes can be disabled.

• #6082 changes how the canonicalizer handles forall and lambda,
  replacing bvars with temporary fvars. Fixes a bug reported by @hrmacbeth
  on
  zulip.

• #6093 use mkFreshUserName in ArgsPacker

• #6096 improves the #print command for structures to show all fields
  and which parents the fields were inherited from, hiding internal
  details such as which parents are represented as subobjects. This
  information is still present in the constructor if needed. The pretty
  printer for private constants is also improved, and it now handles
  private names from the current module like any other name; private names
  from other modules are made hygienic.

• #6098 modifies Lean.MVarId.replaceTargetDefEq and
  Lean.MVarId.replaceLocalDeclDefEq to use Expr.equal instead of
  Expr.eqv when determining whether the expression has changed. This is
  justified on the grounds that binder names and binder infos are
  user-visible and affect elaboration.

• #6105 fixes a stack overflow caused by a cyclic assignment in the
  metavariable context. The cycle is unintentionally introduced by the
  structure instance elaborator.

• #6108 turn off pp.mvars in apply? results

• #6109 fixes an issue in the injection tactic. This tactic may
  execute multiple sub-tactics. If any of them fail, we must backtrack the
  partial assignment. This issue was causing the error: "mvarId is
  already assigned" in issue #6066. The issue is not yet resolved, as the
  equation generator for the match expressions is failing in the example
  provided in this issue.

• #6112 makes stricter requirements for the @[deprecated] attribute,
  requiring either a replacement identifier as @[deprecated bar] or
  suggestion text @[deprecated "Past its use by date"], and also
  requires a since := "..." field.

• #6114 liberalizes atom rules by allowing '' to be a prefix of an
  atom, after #6012 only added an exception for '' alone, and also adds
  some unit tests for atom validation.

• #6116 fixes a bug where structural recursion di...

v4.15.0-rc1

What's Changed

• chore: begin development cycle for v4.15 by @kim-em in #5936
• chore: upstream lemmas about Fin.foldX by @kim-em in #5937
• chore: upstream List.ofFn and relate to Array.ofFn by @kim-em in #5938
• feat: List.mapFinIdx, lemmas, relate to Array version by @kim-em in #5941
• feat: introduce synthetic atoms in bv_decide by @hargoniX in #5942
• feat: add Int16/Int32/Int64 by @hargoniX in #5885
• feat: update toolchain on lake update by @tydeu in #5684
• fix: make all_goals admit goals on failure by @kmill in #5934
• chore: port release notes for v4.13.0 to master by @kim-em in #5947
• feat: List.pmap_eq_self by @vihdzp in #5927
• feat: add Option.or_some' by @vihdzp in #5926
• chore: remove @[simp] from BitVec.ofFin_sub and sub_ofFin by @kim-em in #5951
• feat: relate Array.takeWhile with List.takeWhile by @kim-em in #5950
• feat: relate Array.eraseIdx with List.eraseIdx by @kim-em in #5952
• chore: CI: check for GitHub Actions updates once per month by @Kha in #5954
• chore: CI: bump nwtgck/actions-netlify from 2.0 to 3.0 by @dependabot in #5956
• chore: CI: bump softprops/action-gh-release from 1 to 2 by @dependabot in #5955
• chore: CI: bump raven-actions/actionlint from 1 to 2 by @dependabot in #5957
• chore: CI: bump actions/stale from 8 to 9 by @dependabot in #5958
• chore: CI: give Linux Debug unlimited test stack size by @Kha in #5953
• chore: CI: bump lycheeverse/lychee-action from 1.9.0 to 2.0.2 by @dependabot in #5959
• chore: CI: bump actions/github-script from 6 to 7 by @dependabot in #5962
• chore: CI: bump dawidd6/action-download-artifact from 2 to 6 by @dependabot in #5964
• chore: CI: bump dcarbone/install-jq-action from 1.0.1 to 2.1.0 by @dependabot in #5965
• feat: define ISize and basic operations on it by @hargoniX in #5961
• fix: do not link statically against pthread/dl/rt by @TwoFX in #5966
• chore: fix all_goals test, simulate the max rec depth error by @kmill in #5967
• chore: deprecate Array.split in favour of identical Array.partition by @kim-em in #5970
• fix: arg conv tactic misreported number of arguments on error by @kmill in #5968
• feat: relate Array.isPrefixOf with List.isPrefixOf by @kim-em in #5971
• chore: consolidate decide_True and decide_true_eq_true by @kim-em in #5949
• feat: relate Array.zipWith/zip/unzip with List versions by @kim-em in #5972
• chore: exclude leanruntest_task_test_io for now by @TwoFX in #5973
• feat: add another List.find?_eq_some lemma by @kim-em in #5974
• chore: CI: bump mymindstorm/setup-emsdk from 12 to 14 by @dependabot in #5963
• chore: tag prerelease builds with -pre by @Kha in #5943
• feat: BitVec.twoPow in bv_decide by @hargoniX in #5979
• feat: minor lemmas about List.ofFn by @kim-em in #5982
• chore: upstream List.insertIdx from Batteries, lemmas from Mathlib, and revise lemmas by @kim-em in #5969
• feat: interactions between List.foldX and List.filterX by @kim-em in #5984
• feat: lemmas relating Array.findX and List.findX by @kim-em in #5985
• feat: BitVec.getMsbD in bv_decide by @hargoniX in #5987
• refactor: name the default SizeOf instance by @nomeata in #5981
• chore: fix test exclusion by @Kha in #5990
• style: fix style in bv_decide normalizer by @hargoniX in #5992
• feat: BitVec.sshiftRight' in bv_decide by @hargoniX in #5995
• chore: new PR changelog template by @Kha in #5976
• chore: revert "CI: give Linux Debug unlimited test stack size" by @Kha in #6001
• chore: List.modifyTailIdx naming fix by @kim-em in #6007
• chore: missing @[ext] attribute on monad transformer ext lemmas by @kim-em in #6008
• feat: verify keys method on HashMaps by @monsterkrampe in #5866
• fix: unset trailing for simpa? "try this" suggestion by @kmill in #5907
• feat: change bv_decide to an elaborated config by @hargoniX in #6010
• fix: ensure instantiateMVarsProfiling adds a trace node by @alexkeizer in #5501
• fix: avoid max heartbeat error in completion by @mhuisi in #5996
• perf: avoid negative environment lookup by @Kha in #5429
• chore: CI: exempt drafts from PR body check by @Kha in #6002
• feat: decide +revert and improvements to native_decide by @kmill in #5999
• feat: prop instance yields theorems by @kmill in #5856
• fix: avoid delaborating with field notation if object is a metavariable by @kmill in #6014
• fix: bv_decide benchmarks by @hargoniX in #6017
• chore: cleanup by @JovanGerb in #6021
• feat: BitVec lemmas for smtUDiv, smtSDiv when denominator is zero by @bollu in #5616
• feat: variants of List.forIn_eq_foldlM by @kim-em in #6023
• chore: deprecate duplicated Fin.size_pos by @kim-em in #6025
• feat: change Array.set to take a Nat and a tactic provided bound by @kim-em in #5988
• feat: BitVec normalization rule for udiv by twoPow by @bollu in #6029
• fix: simp only [· ∈ ·] by @nomeata in #6030
• feat: bv_decide and flattening by @hargoniX in #6035
• fix: avoid new term info around def bodies by @Kha in #6031
• fix: bv_decide embedded constraint substitution changes models by @hargoniX in #6037
• feat: only direct parents of classes create projections by @kmill in #5920
• feat: change Array.get to take a Nat and a proof by @kim-em in #6032
• chore: review Array operations argument order by @kim-em in #6041
• feat: various minor changes to List/Array API by @kim-em in #6044
• chore: deprecate Array.sequenceMap by @kim-em in #6027
• chore: mark Meta.Context.config as private by @leodemoura in #6051
• refactor: mark the Simp.Context constructor as private by @leodemoura in #6054
• refactor: omega: avoid MVar machinery by @nomeata in #5991
• chore: pr-body: run as part of merge_group, but do not do anything by @nomeata in #6069
• fix: line break in simp? output by @Kha in #6048
• feat: Bool.to(U)IntX by @hargoniX in #6060
• test: synthetic simp_arith benchmark by @nomeata in #6061
• perf: optimize Nat.Linear.Expr.toPoly by @nomeata in #6062
• fix: make sure monad lift coercion elaborator has no side effects by @kmill in #6024
• perf: optimize Nat.Linear.Poly.norm by @nomeata in #6064
• feat: message kinds by @tydeu in #5945
• chore: add newline at end of file for lake new templates by @alissa-tung in #6026
• chore: remove >6 month old deprecations by @kim-em in #6057
• chore: upstream some NameMap functions by @kim-em in #6056
• feat: lemmas about for loops...

v4.14.0

Full Changelog: v4.13.0...v4.14.0

Language features, tactics, and metaprograms

• structure and inductive commands

  • #5517 improves universe level inference for the resulting type of an inductive or structure. Recall that a Prop-valued inductive type is a syntactic subsingleton if it has at most one constructor and all the arguments to the constructor are in Prop. Such types have large elimination, so they could be defined in Type or Prop without any trouble. The way inference has changed is that if a type is a syntactic subsingleton with exactly one constructor, and the constructor has at least one parameter/field, then the inductive/structure command will prefer creating a Prop instead of a Type. The upshot is that the : Prop in structure S : Prop is often no longer needed. (With @arthur-adjedj).
  • #5842 and #5783 implement a feature where the structure command can now define recursive inductive types:

    structure Tree where
      n : Nat
      children : Fin n → Tree
    
    def Tree.size : Tree → Nat
      | {n, children} => Id.run do
        let mut s := 0
        for h : i in [0 : n] do
          s := s + (children ⟨i, h.2⟩).size
        pure s

  • #5814 fixes a bug where Mathlib's Type* elaborator could lead to incorrect universe parameters with the inductive command.
  • #3152 and #5844 fix bugs in default value processing for structure instance notation (with @arthur-adjedj).
  • #5399 promotes instance synthesis order calculation failure from a soft error to a hard error.
  • #5542 deprecates := variants of inductive and structure (see breaking changes).

• Application elaboration improvements

  • #5671 makes @[elab_as_elim] require at least one discriminant, since otherwise there is no advantage to this alternative elaborator.
  • #5528 enables field notation in explicit mode. The syntax @x.f elaborates as @S.f with x supplied to the appropriate parameter.
  • #5692 modifies the dot notation resolution algorithm so that it can apply CoeFun instances. For example, Mathlib has Multiset.card : Multiset α →+ Nat, and now with m : Multiset α, the notation m.card resolves to ⇑Multiset.card m.
  • #5658 fixes a bug where 'don't know how to synthesize implicit argument' errors might have the incorrect local context when the eta arguments feature is activated.
  • #5933 fixes a bug where .. ellipses in patterns made use of optparams and autoparams.
  • #5770 makes dot notation for structures resolve using all ancestors. Adds a resolution order for generalized field notation. This is the order of namespaces visited during resolution when trying to resolve names. The algorithm to compute a resolution order is the commonly used C3 linearization (used for example by Python), which when successful ensures that immediate parents' namespaces are considered before more distant ancestors' namespaces. By default we use a relaxed version of the algorithm that tolerates inconsistencies, but using set_option structure.strictResolutionOrder true makes inconsistent parent orderings into warnings.

• Recursion and induction principles

  • #5619 fixes functional induction principle generation to avoid over-eta-expanding in the preprocessing step.
  • #5766 fixes structural nested recursion so that it is not confused when a nested type appears first.
  • #5803 fixes a bug in functional induction principle generation when there are let bindings.
  • #5904 improves functional induction principle generation to unfold aux definitions more carefully.
  • #5850 refactors code for Predefinition.Structural.

• Error messages

  • #5276 fixes a bug in "type mismatch" errors that would structurally assign metavariables during the algorithm to expose differences.
  • #5919 makes "type mismatch" errors add type ascriptions to expose differences for numeric literals.
  • #5922 makes "type mismatch" errors expose differences in the bodies of functions and pi types.
  • #5888 improves the error message for invalid induction alternative names in match expressions (@josojo).
  • #5719 improves calc error messages.

• #5627 and #5663 improve the #eval command and introduce some new features.

  • Now results can be pretty printed if there is a ToExpr instance, which means hoverable output. If ToExpr fails, it then tries looking for a Repr or ToString instance like before. Setting set_option eval.pp false disables making use of ToExpr instances.
  • There is now auto-derivation of Repr instances, enabled with the pp.derive.repr option (default to true). For example:

    inductive Baz
    | a | b
    
    #eval Baz.a
    -- Baz.a

    It simply does deriving instance Repr for Baz when there's no way to represent Baz.
  • The option eval.type controls whether or not to include the type in the output. For now the default is false.
  • Now expressions such as #eval do return 2, where monad is unknown, work. It tries unifying the monad with CommandElabM, TermElabM, or IO.
  • The classes Lean.Eval and Lean.MetaEval have been removed. These each used to be responsible for adapting monads and printing results. Now the MonadEval class is responsible for adapting monads for evaluation (it is similar to MonadLift, but instances are allowed to use default data when initializing state), and representing results is handled through a separate process.
  • Error messages about failed instance synthesis are now more precise. Once it detects that a MonadEval class applies, then the error message will be specific about missing ToExpr/Repr/ToString instances.
  • Fixes bugs where evaluating MetaM and CoreM wouldn't collect log messages.
  • Fixes a bug where let rec could not be used in #eval.

• partial definitions

  • #5780 improves the error message when partial fails to prove a type is inhabited. Add delta deriving.
  • #5821 gives partial inhabitation the ability to create local Inhabited instances from parameters.

• New tactic configuration syntax. The configuration syntax for all core tactics has been given an upgrade. Rather than simp (config := { contextual := true, maxSteps := 22}), one can now write simp +contextual (maxSteps := 22). Tactic authors can migrate by switching from (config)? to optConfig in tactic syntaxes and potentially deleting mkOptionalNode in elaborators. #5883, #5898, #5928, and #5932. (Tactic authors, see breaking changes.)

• simp tactic

  • #5632 fixes the simpproc for Fin literals to reduce more consistently.
  • #5648 fixes a bug in simpa ... using t where metavariables in t were not properly accounted for, and also improves the type mismatch error.
  • #5838 fixes the docstring of simp! to actually talk about simp!.
  • #5870 adds support for attribute [simp ←] (note the reverse direction). This adds the reverse of a theorem as a global simp theorem.

• decide tactic

  • #5665 adds decide! tactic for using kernel reduction (warning: this is renamed to decide +kernel in a future release).

• bv_decide tactic

  • #5714 adds inequality regression tests (@alexkeizer).
  • #5608 adds bv_toNat tag for toNat_ofInt (@bollu).
  • #5618 adds support for at in ac_nf and uses it in bv_normalize (@tobiasgrosser).
  • #5628 adds udiv support.
  • #5635 adds auxiliary bitblasters for negation and subtraction.
  • #5637 adds more getLsbD bitblaster theory.
  • #5652 adds umod support.
  • #5653 adds performance benchmark for modulo.
  • [#5655](#5655...

v4.14.0-rc3

feat: lake: detailed Reservoir fetch error (#6231)

This PR improves the errors Lake produces when it fails to fetch a
dependency from Reservoir. If the package is not indexed, it will
produce a suggestion about how to require it from GitHub.

Closes #5330.

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 (…