Releases: leanprover/lean4
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 involvingBitVec
andBool
. 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 useLean.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 ofbv_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 intests/lean/run/bv_*
for examples. -
simp
tactic- #4988 fixes a panic in the
reducePow
simproc. - #5071 exposes the
index
option to thedsimp
tactic, introduced tosimp
in #4202. - #5159 fixes a panic at
Fin.isValue
simproc. - #5167 and #5175 rename the
simpCtorEq
simproc toreduceCtorEq
and makes it optional. (See breaking changes.) - #5187 ensures
reduceCtorEq
is enabled in thenorm_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 fortrace.Debug.Meta.Tactic.simp
trace messages.
- #4988 fixes a panic in the
-
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.
- #5117 fixes a bug where
-
omega
tactic- #5157 fixes a panic.
-
conv
tactic- #5149 improves
arg n
to handle subsingleton instance arguments.
- #5149 improves
-
#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 indecreasing_by
. This can be disabled withset_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 tofalse
to get the old behavior. See breaking changes. - #5141 adds
f.eq_unfold
lemmas. Now Lean produces the following zoo of rewrite rules:TheOption.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)
f.eq_unfold
variant is especially useful to rewrite withrw
under binders. - #5136 fixes bugs in recursion over predicates.
- #5016 and #5066 add
-
Variable inclusion
- #5206 documents that
include
currently only applies to theorems.
- #5206 documents that
-
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 asfun x1 x2 => x1 + x2
rather thanfun 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.
- #5118 changes the definition of the
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
.
- #5031 localizes an instance in
Pretty printing
- #4976 introduces
@[app_delab]
, a macro for creating delaborators for particular constants. The@[app_delab ident]
syntax resolvesident
to its constant namename
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'`.
v4.11.0
Language features, tactics, and metaprograms
-
The variable inclusion mechanism has been changed. Like before, when a definition mentions a variable, Lean will add it as an argument of the definition, but now in theorem bodies, variables are not included based on usage in order to ensure that changes to the proof cannot change the statement of the overall theorem. Instead, variables are only available to the proof if they have been mentioned in the theorem header or in an
include
command or are instance implicit and depend only on such variables. Theomit
command can be used to omit included variables.See breaking changes below.
-
Recursive definitions
-
Structural recursion can now be explicitly requested using
termination_by structural x
in analogy to the existing
termination_by x
syntax that causes well-founded recursion to be used.
#4542 -
#4672 fixes a bug that could lead to ill-typed terms.
-
The
termination_by?
syntax no longer forces the use of well-founded recursion, and when structural
recursion is inferred, it will print the result using thetermination_by structural
syntax. -
Mutual structural recursion is now supported. This feature supports both mutual recursion over a non-mutual
data type, as well as recursion over mutual or nested data types:mutual def Even : Nat → Prop | 0 => True | n+1 => Odd n def Odd : Nat → Prop | 0 => False | n+1 => Even n end mutual inductive A | other : B → A | empty inductive B | other : A → B | empty end mutual def A.size : A → Nat | .other b => b.size + 1 | .empty => 0 def B.size : B → Nat | .other a => a.size + 1 | .empty => 0 end inductive Tree where | node : List Tree → Tree mutual def Tree.size : Tree → Nat | node ts => Tree.list_size ts def Tree.list_size : List Tree → Nat | [] => 0 | t::ts => Tree.size t + Tree.list_size ts end
Functional induction principles are generated for these functions as well (
A.size.induct
,A.size.mutual_induct
).Nested structural recursion is still not supported.
PRs: #4639, #4715, #4642, #4656, #4684, #4715, #4728, #4575, #4731, #4658, #4734, #4738, #4718, #4733, #4787, #4788, #4789, #4807, #4772
-
#4809 makes unnecessary
termination_by
clauses cause warnings, not errors. -
#4831 improves handling of nested structural recursion through non-recursive types.
-
#4839 improves support for structural recursive over inductive predicates when there are reflexive arguments.
-
-
simp
tactic- #4784 sets configuration
Simp.Config.implicitDefEqProofs
totrue
by default.
- #4784 sets configuration
-
omega
tactic -
decide
tactic- #4711 switches from using default transparency to at least default transparency when reducing the
Decidable
instance. - #4674 adds detailed feedback on
decide
tactic failure. It tells you whichDecidable
instances it unfolded, if it get stuck onEq.rec
it gives a hint about avoiding tactics when definingDecidable
instances, and if it gets stuck onClassical.choice
it gives hints about classical instances being in scope. During this process, it processesDecidable.rec
s and matches to pin blame on a non-reducing instance.
- #4711 switches from using default transparency to at least default transparency when reducing the
-
@[ext]
attribute- #4543 and #4762 make
@[ext]
realizeext_iff
theorems from userext
theorems. Fixes the attribute so that@[local ext]
and@[scoped ext]
are usable. The@[ext (iff := false)]
option can be used to turn offext_iff
realization. - #4694 makes "go to definition" work for the generated lemmas. Also adjusts the core library to make use of
ext_iff
generation. - #4710 makes
ext_iff
theorem preserve inst implicit binder types, rather than making all binder types implicit.
- #4543 and #4762 make
-
#eval
command- #4810 introduces a safer
#eval
command that prevents evaluation of terms that containsorry
. The motivation is that failing tactics, in conjunction with operations such as array accesses, can lead to the Lean process crashing. Users can use the new#eval!
command to use the previous unsafe behavior. (#4829 adjusts a test.)
- #4810 introduces a safer
-
#4447 adds
#discr_tree_key
and#discr_tree_simp_key
commands, for helping debug discrimination tree failures. The#discr_tree_key t
command prints the discrimination tree keys for a termt
(or, if it is a single identifier, the type of that constant). It uses the default configuration for generating keys. The#discr_tree_simp_key
command is similar to#discr_tree_key
, but treats the underlying type as one of a simp lemma, that is it transforms it into an equality and produces the key of the left-hand side.For example,
#discr_tree_key (∀ {a n : Nat}, bar a (OfNat.ofNat n)) -- bar _ (@OfNat.ofNat Nat _ _) #discr_tree_simp_key Nat.add_assoc -- @HAdd.hAdd Nat Nat Nat _ (@HAdd.hAdd Nat Nat Nat _ _ _) _
-
#4741 changes option parsing to allow user-defined options from the command line. Initial options are now re-parsed and validated after importing. Command line option assignments prefixed with
weak.
are silently discarded if the option name without the prefix does not exist. -
Deriving handlers
-
Metaprogramming
- #4593 adds
unresolveNameGlobalAvoidingLocals
. - #4618 deletes deprecated functions from 2022.
- #4642 adds
Meta.lambdaBoundedTelescope
. - #4731 adds
Meta.withErasedFVars
, to enter a context with some fvars erased from the local context. - #4777 adds assignment validation at
closeMainGoal
, preventing users from circumventing the occurs check for tactics such asexact
. - #4807 introduces
Lean.Meta.PProdN
module for packing and projecting nestedPProd
s. - #5170 fixes
Syntax.unsetTrailing
. A consequence of this is that "go to definition" now works on the last module name in animport
block (issue #4958).
- #4593 adds
Language server, widgets, and IDE extensions
- #4727 makes it so that responses to info view requests come as soon as the relevant tactic has finished execution.
- #4580 makes it so that whitespace changes do not invalidate imports, and so starting to type the first declaration after imports should no longer cause them to reload.
- [#4780](https://github.com/leanprover/lean4/pull...
v4.11.0-rc3
v4.11.0-rc2
chore: adapt stdlib to new `variable` behavior