nightly-2024-12-10

Changes since nightly-2024-12-09:

Full commit log

• 8a3a806 chore: update stage0
• 5c333ef fix: Float32 runtime support (#6350)
• e69bcb0 chore: improve BitVec ext lemmas (#6349)
• c5b82e0 feat: BitVec.[toFin|getMsbD]_setWidth and [getMsbD|msb]_signExtend (#6338)
• b6177ba chore: update stage0
• 2e11b8a feat: add support for Float32 to the Lean runtime (#6348)
• ff3d12c doc: clarify difference between Expr.hasLooseBVars and Expr.hasLooseBVar (#6344)
• 520d4b6 chore: cleanup of Array lemmas (#6343)
• c7b8c5c chore: alignment of Array and List lemmas (#6342)

nightly-2024-12-09

Changes since nightly-2024-12-08:

Full Changelog: leanprover/lean4@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 reduces error on bv_check to warning.
  • [#5670...

nightly-2024-12-08

Changes since nightly-2024-12-07:

Full commit log

• 4dd182c chore: remove deprecated aliases for Int.tdiv and Int.tmod (#6322)
• 762c575 doc: missing (type := true) in reader monad example (#6196)

nightly-2024-12-07

Changes since nightly-2024-12-06:

Full commit log

• 6447fda feat: FunInd: omit unused parameters (#6330)
• 279f36b chore: update stage0
• d2853ec feat: FunInd: omit unused parameters (#6330)

nightly-2024-12-06

Changes since nightly-2024-12-05:

Full commit log

• 6e60d13 feat: getElem lemmas for Vector operations (#6324)

nightly-2024-12-05

Changes since nightly-2024-12-04:

Full commit log

• 019f8e1 chore: protect Fin.cast and BitVec.cast (#6315)
• c366a29 chore: generalize universe in Array.find? (#6318)
• 1400b95 feat: upstream ToLevel from mathlib (#6285)
• 00c7b85 feat: lemmas about for loops over Option (#6316)
• f6e88e5 fix: missing HEq support at ToLCNF (#6311)
• 88573c8 test: do not filter output for non-diff tests (#6308)
• faf07e5 chore: remove unused imports (#6305)

nightly-2024-12-04

Changes since nightly-2024-12-03:

Full commit log

• c518156 feat: BitVec.[toInt|toFin]_concat and Bool.toInt (#6182)
• 7721102 feat: BitVec.toFin/ToInt BitVec.ushiftRight (#6238)
• da9a0c4 chore: update stage0
• b9bf943 feat: add debug.proofAsSorry (#6300)
• 2a891a3 chore: CMAKE_CXX_SYSROOT_FLAG is also needed for linking (#6297)
• 00718c3 chore: clean up Elab.async handling (#6299)
• 473274f chore: update stage0
• 7b98fbe feat: reverse HashMap.toList, so it agrees with HashMap.toArray (#6244)
• 24b412e refactor: move IO.Channel and IO.Mutex to Std.Sync (#6282)

nightly-2024-12-03

Changes since nightly-2024-12-02:

Full commit log

• cb600ed chore: restore broken proofs
• 57d83c8 feat: add simp configuration to norm_cast macros
• ce27d49 chore: update stage0
• 8a7889d chore: temporarily sorry broken proofs
• 6934029 chore: add simp configuration to norm_cast syntax
• 222abdd feat: simprocs for other Fin operations (#6295)
• 490be92 chore: specialize fold loops (#6293)
• cda6d5c chore: upstream List.length_flatMap (#6294)
• 9044043 chore: robustify for byAsSorry (#6287)
• f6bc6b2 fix: lake: properly prepend job log in ensureJob (#6291)
• d9d54c1 chore: lake: use & check prelude (#6289)
• b2336fd perf: speed up bv_decide reflection using Lean.RArray (#6288)
• f156f22 feat: lake: build without leanc (#6176)
• 3c348d4 chore: CI: bump dawidd6/action-download-artifact from 6 to 7 (#6274)
• 0b8f50f feat: async linting (#4460)
• 0d89f01 perf: bv_decide uses rfl in reflection if possible (#6286)
• e157fcb chore: missing Array/Vector injectivity lemmas (#6284)
• 95dbac2 chore: shake Std.Time (#6283)
• be63c82 chore: CI: bump dcarbone/install-jq-action from 2.1.0 to 3.0.1 (#6275)
• 6fcf35e chore: script/mathlib-bench (#6280)
• b3e0c9c fix: use sensible notion of indentation in structure instance field completion (#6279)

nightly-2024-12-02

Changes since nightly-2024-12-01:

v4.16.0
v4.15.0

Release candidate, release notes will be copied from the branch releases/v4.15.0 once completed.

• #3090 handles level parameters in Meta.evalExpr (@eric-wieser)

Full commit log

• 3c5e612 chore: begin development cycle for v4.16.0 (#6277)
• 29e84fa feat: omega doesn't get stuck on bare Int.negSucc (#6276)
• 6bf8ff3 feat: more UInt bitwise theorems (#6188)
• 62b8238 chore: remove accidentally added file (#6262)
• 0a2a8e8 feat: make "foo has been deprecated" warning be hoverable (#6273)
• 23236ef fix: have Lean.Meta.isConstructorApp'? be aware of n + k Nat offsets (#6270)
• b2f70da feat: Array.swap_perm (#6272)
• 819cb87 chore: upstream Vector lemmas (#6271)

nightly-2024-12-01

Changes since nightly-2024-11-30:

Full commit log

• 3ee2842 feat: remove runtime bounds checks and partial from qsort (#6241)
• 7b8504c chore: post-stage0 cleanup for #6165 (#6268)
• ca96922 chore: update stage0
• a1c3a36 feat: parity between structure instance notation and where notation (#6165)
• 734ea30 chore: update stage0
• f3f0045 feat: add structInstFieldDecl syntax category (#6265)