nightly-2025-01-10

Changes since nightly-2025-01-09:

Full commit log

• d2c4471 feat: BitVec.{toInt, toFin, msb}_udiv (#6402)
• c07948a feat: add simp? and dsimp? in conversion mode (#6593)
• d369976 feat: improve inequality offset support theorems for grind (#6595)
• a6789a7 feat: Std.Net.Addr (#6563)
• 1b42728 feat: add UInt32.{lt, le} (#6591)

nightly-2025-01-09

Changes since nightly-2025-01-08:

Full commit log

• dd64455 feat: improve grind canonicalizer diagnostics (#6588)
• 827c667 feat: align List/Array lemmas for filter/filterMap (#6589)
• 623dec1 feat: aligning List/Array/Vector lemmas for map (#6586)
• cb9f198 fix: grind canonicalizer (#6585)
• c5314da feat: add helper theorems for handling offsets in grind (#6584)
• 0afa1d1 feat: apply E-matching for local lemmas in grind (#6582)
• ddd454c feat: add grind configuration options to control case-splitting (#6581)
• 5be241c fix: forall propagation in grind (#6578)
• 034bc26 feat: make classical tactic incremental (#6575)
• 680ede7 fix: set LLVM sysroot consistently (#6574)
• 48eb308 perf: speed up JSON serialisation (#6479)
• f01471f fix: proper "excess binders" error locations for rintro and intro (#6565)

nightly-2025-01-08

Changes since nightly-2025-01-07:

Full commit log

• 00ef231 feat: split on match-expressions in the grind tactic (#6569)
• 9040108 feat: add BitVec.[toNat|toInt|toFin|getLsbD|getMsbD|getElem|msb]_fill (#6177)
• 91cbd7c feat: BitVec.toInt_shiftLeft theorem (#6346)
• 18b183f feat: let induction take zero alteratives (#6486)
• 78ed072 feat: add Int.emod_sub_emod and Int.sub_emod_emod (#6507)
• 22a7995 feat: add support for cast, Eq.rec, Eq.ndrec to grind (#6568)
• 5decd2c feat: trace messages for working and closing goals in the grind tactic (#6567)
• 0da5be1 feat: add support for erasing the [grind] attribute (#6566)
• 83098cd chore: typos / improvements to grind messages (#6561)
• a2a525f fix: set absolute linker path (#6547)

nightly-2025-01-07

Changes since nightly-2025-01-06:

Full commit log

• 97d07a5 feat: basic case-split for grind (#6559)
• a424029 feat: Array lemma alignment; fold and map (#6546)
• db3ab39 feat: propagate implication in the grind tactic (#6556)
• 8dec579 feat: grind tests for basic category theory (#6543)
• 3ca3f84 fix: avoid new tokens _=_ and =_ (#6554)
• 2c9641f doc: modify aesop usage example of omegaDefault (#6549)

nightly-2025-01-06

Changes since nightly-2025-01-05:

Full commit log

• 78ddee9 feat: release checklist script (#6542)
• 2ed77f3 feat: attribute [grind] (#6545)
• 76f883b fix: remove unused -static-libgcc MinGW linker arg (#6535)
• 675244d feat: [grind_eq] attribute for the grind tactic (#6539)
• fd091d1 feat: pattern normalization in the grind tactic (#6538)
• 7b29f48 fix: E-matching thresholds in the grind tactic (#6536)
• fb506b9 fix: allow projections in E-matching patterns (#6534)

nightly-2025-01-05

Changes since nightly-2025-01-04:

Full commit log

• dc5c809 feat: add term offset support to the grind E-matching modulo (#6533)
• 9dcbc33 chore: fix signature of perm_insertIdx (#6532)
• d22233f fix: let_fun support in grind (#6531)
• a5b1ed9 fix: nondeterministic failure in grind (#6530)
• ad2c16d feat: add support for let-declarations to grind (#6529)
• 37127ea fix: missing propagation in grind (#6528)
• 31435e9 doc: fix broken code blocks in RELEASES.md (#6527)

nightly-2025-01-04

Changes since nightly-2025-01-03:

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](https://github.com/leanprover/lean4/pull/6381) fixes a bug in `withTrackingZetaDelta` and
`withTrackingZetaDeltaSet`. The `MetaM` caches need to be reset. See new
test.

* [#6385](https://github.com/leanprover/lean4/pull/6385) fixes a bug in `simp_all?` that caused some local declarations
to be omitted from the `Try this:` suggestions.

* [#6386](https://github.com/leanprover/lean4/pull/6386) ensures that `revertAll` clears auxiliary declarations when
invoked directly by users.

* [#6387](https://github.com/leanprover/lean4/pull/6387) fixes a type error in the proof generated by the `contradiction`
tactic.

* [#6397](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/6398) ensures `Meta.check` check projections.

* [#6412](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/6419) fixes multiple bugs in the WIP `grind` tactic. It also adds
support for printing the `grind` internal state.

* [#6428](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/6435) implements the congruence table for the (WIP) `grind` tactic. It
also fixes several bugs, and adds a new preprocessing step.

* [#6437](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/6438) ensures `norm_cast` doesn't fail to act in the presence of
`no_index` annotations

* [#6441](https://github.com/leanprover/lean4/pull/6441) adds basic truth value propagation rules to the (WIP) `grind`
tactic.

* [#6442](https://github.com/leanprover/lean4/pull/6442) fixes the `checkParents` sanity check in `grind`.

* [#6443](https://github.com/leanprover/lean4/pull/6443) adds support for propagating the truth value of equalities in
the (WIP) `grind` tactic.

* [#6447](https://github.com/leanprover/lean4/pull/6447) refactors `grind` and adds support for invoking the simplifier
using the `GrindM` monad.

* [#6448](https://github.com/leanprover/lean4/pull/6448) declares the command `builtin_grind_propagator` for registering
equation propagator for `grind`. It also declares the auxiliary the
attribute.

* [#6449](https://github.com/leanprover/lean4/pull/6449) completes the implementation of the command
`builtin_grind_propagator`.

* [#6452](https://github.com/leanprover/lean4/pull/6452) adds support for generating (small) proofs for any two
expressions that belong to the same equivalence class in the `grind`
tactic state.

* [#6453](https://github.com/leanprover/lean4/pull/6453) improves bv_decide's performance in the presence of large
literals.

* [#6455](https://github.com/leanprover/lean4/pull/6455) fixes a bug in the equality proof generator in the (WIP) `grind`
tactic.

* [#6456](https://github.com/leanprover/lean4/pull/6456) fixes another bug in the equality proof generator in the (WIP)
`grind` tactic.

*...

nightly-2025-01-03

Changes since nightly-2025-01-02:

Full commit log

• 1907865 perf: avoid unnecessary assert/intro pairs in grind (#6514)
• df9ed20 feat: ite and dite support in grind (#6513)
• 3e2f1fa feat: add user-defined fallback procedure for the grind tactic (#6512)
• 9d62227 feat: custom congruence rule for equality in grind (#6510)
• e46b5f3 fix: congruence closure in the grind tactic (#6509)
• 3cba171 fix: missing case in checkParents (#6508)
• 092449a chore: update stage0
• e9f0691 feat: partial_fixpoint: monotonicity tactic (#6506)
• 7d0c0d4 feat: partial_fixpoint: theory (#6477)
• 9eb173e fix: ignore no_index around OfNat.ofNat in norm_cast (#6438)

nightly-2025-01-02

Changes since nightly-2025-01-01:

Full commit log

• 8d9d814 feat: grind simple strategy (#6503)
• a08379c fix: proof generation for grind tactic (#6502)
• f0c5936 feat: add PersistentHashSet.toList (#6501)
• c0d67e2 fix: bug in markNestedProofs within grind (#6500)
• a8d09da fix: proof canonicalizer in grind (#6499)
• f7c4edc feat: dependent forall propagator in grind (#6498)
• 82bae24 fix: another bug in theorem instantiation in grind (#6497)
• fedaf85 fix: theorem instantiation in grind (#6492)

nightly-2025-01-01

Changes since nightly-2024-12-31:

Full commit log

• 6d44715 fix: make sure parent structure projections have 'go to definition' information (#6487)
• 3427630 feat: configuration options for the grind tactic (#6490)
• 5ba4761 fix: E-matching module for grind (#6488)
• 8899c7e feat: instantiate ematch theorems in grind (#6485)
• 640b356 chore: add missing diff-exposing in type/value mismatch errors (#6484)
• 8f5ce3a feat: upstream ToExpr deriving handler from Mathlib (#6473)