1 Release published by 1 person

• v4.13.0

  published Nov 1, 2024

57 Pull requests merged by 15 people

• fix: .. in patterns should not make use of optparams or autoparams

  #5933 merged Nov 3, 2024

• feat: update omega/solve_by_elim to use new tactic syntax, use new tactic syntax

  #5932 merged Nov 3, 2024

• feat: add --short-version (-V) option to display short version

  #5930 merged Nov 3, 2024

• chore: prepare omega and solve_by_elim for new tactic config syntax

  #5928 merged Nov 3, 2024

• feat: add text option for buildFile* utilities

  #5924 merged Nov 3, 2024

• feat: make MapDeclarationExtension tolerate multiple insertions

  #5911 merged Nov 2, 2024

• chore: remove unused deriving handler argument syntax

  #5265 merged Nov 1, 2024

• feat: better error message for invalid induction alternative name

  #5888 merged Nov 1, 2024

• feat: on "type mismatch" errors, expose differences in functions and pi types

  #5922 merged Nov 1, 2024

• feat: make "type mismatch" error add numeric type ascriptions

  #5919 merged Nov 1, 2024

• fix: bv_normalize loose mvars

  #5918 merged Nov 1, 2024

• chore: CI: build 64-bit platforms consistently with GMP

  #5144 merged Nov 1, 2024

• feat: relate for loops over List with foldlM

  #5913 merged Nov 1, 2024

• feat: conv arg now can access more arguments

  #5894 merged Nov 1, 2024

• feat: activate new tactic configuration syntax for most tactics

  #5898 merged Nov 1, 2024

• chore: minor tweaks to Array lemmas

  #5912 merged Nov 1, 2024

• feat: add BitVec.(msb, getMsbD, getLsbD)_(neg, abs)

  #5721 merged Nov 1, 2024

• chore: remove @[simp] from Sum.forall and Sum.exists

  #5900 merged Nov 1, 2024

• feat: interim implementation of HashMap.modify/alter

  #5880 merged Nov 1, 2024

• feat: resolve generalized field notation using all parents

  #5770 merged Oct 31, 2024

• fix: FunInd: unfold aux definitions more carefully

  #5904 merged Oct 31, 2024

• fix: delta derived instances now have declaration ranges

  #5899 merged Oct 31, 2024

• chore: remove native code for UInt8.modn

  #5901 merged Oct 31, 2024

• chore: rename Array.back to back!

  #5897 merged Oct 31, 2024

• chore: move @[simp] from back_eq_back? to back_push

  #5896 merged Oct 31, 2024

• feat: LawfulBEq (Array α) ↔ LawfulBEq α

  #5895 merged Oct 31, 2024

• chore: remove duplicated ForIn instances

  #5892 merged Oct 31, 2024

• feat: enable recursive structure command

  #5783 merged Oct 31, 2024

• fix: bring elaborator in line with kernel for primitive projections

  #5822 merged Oct 31, 2024

• fix: make structure parent info persist

  #5890 merged Oct 31, 2024

• chore: (belatedly) begin development cycle for v4.14.0

  #5889 merged Oct 31, 2024

• feat: adds optConfig syntax for tactic configuration

  #5883 merged Oct 30, 2024

• feat: upstream and update #where command

  #5065 merged Oct 30, 2024

• fix: declareSimpLikeTactic macro to use mkSynthetic

  #5838 merged Oct 30, 2024

• feat: add embedded constraint substitution to bv_decide

  #5886 merged Oct 30, 2024

• chore: add missing deprecation dates

  #5884 merged Oct 30, 2024

• chore: mention #version in bug report template

  #5769 merged Oct 30, 2024

• feat: prove that intMin is indeed the smallest signed bitvector

  #5778 merged Oct 30, 2024

• [Backport releases/v4.13.0] fix: lake: do not delete path dependencies

  #5882 merged Oct 30, 2024

• fix: lake: do not delete path dependencies

  #5878 merged Oct 30, 2024

• feat: Hashable (BitVec n)

  #5881 merged Oct 30, 2024

• chore: rename List.groupBy to splitBy

  #5879 merged Oct 30, 2024

• feat: add Nat.log2_two_pow

  #5756 merged Oct 30, 2024

• chore: move MessageData.ofConstName earlier

  #5877 merged Oct 29, 2024

• feat: accurate binder names in signatures (like in output of #check)

  #5827 merged Oct 29, 2024

• fix: init git only not inside git work tree

  #5789 merged Oct 29, 2024

• feat: attribute [simp ←]

  #5870 merged Oct 29, 2024

• fix: prevent addPPExplicitToExposeDiff from assigning metavariables

  #5276 merged Oct 28, 2024

• fix: let simp arguments elaborate with error recovery

  #5863 merged Oct 28, 2024

• fix: remove withoutRecover from apply elaboration

  #5862 merged Oct 28, 2024

• feat: improved calc error messages

  #5719 merged Oct 28, 2024

• feat: support all the SMTLIB BitVec divison/remainder operations in bv_decide

  #5869 merged Oct 28, 2024

• feat: add BitVec.(msb, getMsbD)_concat

  #5865 merged Oct 28, 2024

• feat: add BitVec.[zero_ushiftRight|zero_sshiftRight|zero_mul] and cle…

  #5858 merged Oct 28, 2024

• fix: let congr conv tactic handle "over-applied" functions

  #5861 merged Oct 28, 2024

• feat: record all structure parents in StructureInfo

  #5853 merged Oct 28, 2024

• feat: make it possible to use dot notation in m! strings

  #5857 merged Oct 27, 2024

10 Pull requests opened by 8 people

• feat: elaborate theorem bodies in parallel

  #5864 opened Oct 28, 2024

• feat: verify keys method on HashMaps

  #5866 opened Oct 28, 2024

• feat: add Int16/Int32/Int64

  #5885 opened Oct 30, 2024

• feat: Upstream derive handler for `ToExpr` from Mathlib

  #5906 opened Oct 31, 2024

• fix: unset trailing for `simpa?` "try this" suggestion

  #5907 opened Oct 31, 2024

• feat: all direct parents of classes create projections

  #5920 opened Nov 1, 2024

• feat: match_1.float theorems

  #5923 opened Nov 1, 2024

• feat: add `Option.or_some'`

  #5926 opened Nov 2, 2024

• feat: `List.pmap_eq_self`

  #5927 opened Nov 2, 2024

• fix: add cmake COPY_CADICAL option to allow turning off install copy

  #5931 opened Nov 3, 2024

22 Issues closed by 7 people

• Failure of exhaustiveness checker when matching on `Exception`

  #4555 closed Nov 3, 2024

• RFE: add --short-version or --numeric-version

  #5929 closed Nov 3, 2024

• RFC: Improved error msg for induction alternative names

  #5887 closed Nov 1, 2024

• Variables not visible inside calc statement

  #5921 closed Nov 1, 2024

• Lean compiler can worsen the asymptotic running time of programs

  #5908 closed Nov 1, 2024

• incorrect type hover for

  #5914 closed Nov 1, 2024

• conv: "cannot select argument" with funlike coercions

  #5871 closed Nov 1, 2024

• Dot notation resolution has counterintuitive behavior with diamond multiple inheritance

  #3467 closed Oct 31, 2024

• Cannot derive functional induction principle

  #5903 closed Oct 31, 2024

• Miscompilation of `UInt64.modn`

  #5818 closed Oct 31, 2024

• deadlock in l_Array_foldlMUnsafe_fold___at_Lean_Language_SnapshotTree_runAndReport___spec__2

  #5893 closed Oct 31, 2024

• `simp!` docstring does not talk about simp!

  #5597 closed Oct 30, 2024

• `lake update` deletes files outside the `.lake` directory

  #5876 closed Oct 30, 2024

• Automatically quantified variables are either inaccessible, or misprinted

  #5810 closed Oct 29, 2024

• RFC: simp attribute to accept ← modifier

  #5828 closed Oct 29, 2024

• certain tactics don't show term info on error

  #3831 closed Oct 29, 2024

• all_goals + apply elaboration = lost errors

  #4888 closed Oct 28, 2024

• RFC: Better error reports for incomplete `calc`

  #4318 closed Oct 28, 2024

• No distinction between configuration warnings/errors in the root vs dependencies

  #2765 closed Oct 28, 2024

• `conv`-mode `congr` tactic fails with "over-applied" functions

  #2942 closed Oct 28, 2024

• Build breaks: error: no member named 'm_ptr' in 'parray<T, ThreadSafe>'

  #5860 closed Oct 28, 2024

• [RFC] record all parents structures in `StructureInfo`

  #1881 closed Oct 28, 2024

13 Issues opened by 13 people

• A "declaration has metavariables" error

  #5925 opened Nov 2, 2024

• ld: error: undefined symbol: initialize_Lake

  #5917 opened Nov 1, 2024

• lake: add author to lakefile by default?

  #5916 opened Nov 1, 2024

• incorrect hover type for array in syntax quote destruct

  #5915 opened Nov 1, 2024

• `Eq` behaves differently from `_=_`

  #5910 opened Oct 31, 2024

• RFC: Upstreaming the derive handler for `ToExpr`

  #5909 opened Oct 31, 2024

• simp failure

  #5905 opened Oct 31, 2024

• Default instances are not subject to the instance synthesis depth limit

  #5902 opened Oct 31, 2024

• RFC: rename "structure-like" to "non-rec structure"

  #5891 opened Oct 31, 2024

• `#check` does not issue deprecation warning or handle overloaded definitions

  #5873 opened Oct 29, 2024

• Bug in the option `trace.profiler.output.pp`

  #5872 opened Oct 28, 2024

• attribute [-simp] cannot be undone

  #5868 opened Oct 28, 2024

• `import runtime NonsenseModule` emits no diagnostics

  #5867 opened Oct 28, 2024

35 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• feat: add date and time functionality

  #4904 commented on Nov 1, 2024 • 8 new comments

• feat: update toolchain on `lake update`

  #5684 commented on Nov 1, 2024 • 2 new comments

• Elaborator doesn't produce `InfoTree` for incomplete `match` and incomplete terms in `apply`

  #5336 commented on Oct 29, 2024 • 0 new comments

• feat: fat static libraries with all transitive dependencies

  #4271 commented on Oct 30, 2024 • 0 new comments

• chore: bump olean version

  #5089 commented on Oct 30, 2024 • 0 new comments

• feat: set priority in monadic class instances

  #5291 commented on Nov 1, 2024 • 0 new comments

• feat: qsort with proven bounds and correctness proof

  #5346 commented on Oct 31, 2024 • 0 new comments

• fix: consistently show non-mvar term in hovertext

  #5368 commented on Nov 1, 2024 • 0 new comments

• fix: ensure `instantiateMVarsProfiling` adds a trace node

  #5501 commented on Nov 1, 2024 • 0 new comments

• feat: BitVec lemmas for smtUDiv, smtSDiv when denominator is zero

  #5616 commented on Oct 29, 2024 • 0 new comments

• chore: add LNSym omega benchmarks with large problems that take multiple seconds to solve

  #5622 commented on Oct 29, 2024 • 0 new comments

• chore: add example where omega never terminates / runs out of heartbeats

  #5662 commented on Oct 29, 2024 • 0 new comments

• feat: simp local confluence testing

  #5717 commented on Nov 1, 2024 • 0 new comments

• feat: BitVec.toInt_abs

  #5787 commented on Oct 29, 2024 • 0 new comments

• feat: Pass `argv[0]` to `main`

  #5820 commented on Oct 28, 2024 • 0 new comments

• feat: structure auto-completion & partial InfoTrees

  #5835 commented on Oct 30, 2024 • 0 new comments

• feat: rsimp_decide etc

  #5839 commented on Nov 2, 2024 • 0 new comments

• feat: stronger proof strategy for `partial` inhabitation

  #5847 commented on Oct 30, 2024 • 0 new comments

• Misleading error: `match` leads to an error about `cases` where no tactic is used

  #5809 commented on Oct 29, 2024 • 0 new comments

• RFC: `.h` header files should be generated alongside the `.c` source files

  #5829 commented on Oct 29, 2024 • 0 new comments

• `bv_decide`: support for shifting by a natural number

  #5327 commented on Oct 30, 2024 • 0 new comments

• Deep kernel reduction detected after `simp`

  #5724 commented on Nov 1, 2024 • 0 new comments

• Optimizing terms for kernel reduction (meta issue)

  #5806 commented on Nov 2, 2024 • 0 new comments

• Metavariable assignment can fail if created underneath `let`

  #5387 commented on Nov 2, 2024 • 0 new comments

• `unsafe opaque` does not allow unsafe body

  #2191 commented on Nov 3, 2024 • 0 new comments

• The build installs a copy of the already installed cadical binary

  #5603 commented on Nov 3, 2024 • 0 new comments

• feat: mark predefinitions that failed to compile as noncomputable

  #2610 commented on Oct 31, 2024 • 0 new comments

• feat: set_option for conv mode

  #2887 commented on Oct 31, 2024 • 0 new comments

• fix: pass CMAKE_C/CXX_COMPILER to all stages

  #3080 commented on Oct 30, 2024 • 0 new comments

• fix: make lean4 build on FreeBSD

  #3182 commented on Oct 30, 2024 • 0 new comments

• doc: mention maxSteps setting in its error message

  #3287 commented on Oct 30, 2024 • 0 new comments

• fix: remove special handling of numerals in `DiscrTree`

  #3684 commented on Oct 30, 2024 • 0 new comments

• chore: upstream `Nat.binaryRec`

  #3756 commented on Oct 30, 2024 • 0 new comments

• feat: binary recursive implementation of List.mapA

  #3877 commented on Oct 30, 2024 • 0 new comments

• feat: Implement Functor for Array

  #3976 commented on Oct 30, 2024 • 0 new comments