Lean 4.12.0 (2024-10-01)🔗

Language features, tactics, and metaprograms

bv_decide tactic. This release introduces a new tactic for proving goals involving BitVec and Bool. 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 use Lean.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 of bv_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 in tests/lean/run/bv_* for examples.

#5013, #5074, #5100, #5113, #5137, #5203, #5212, #5220.
simp tactic
- #4988 fixes a panic in the reducePow simproc.
- #5071 exposes the index option to the dsimp tactic, introduced to simp in #4202.
- #5159 fixes a panic at Fin.isValue simproc.
- #5167 and #5175 rename the simpCtorEq simproc to reduceCtorEq and makes it optional. (See breaking changes.)
- #5187 ensures reduceCtorEq is enabled in the norm_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 for trace.Debug.Meta.Tactic.simp trace messages.
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.
omega tactic
- #5157 fixes a panic.
conv tactic
- #5149 improves arg n to handle subsingleton instance arguments.
#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 in decreasing_by. This can be disabled with set_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 to false to get the old behavior. See breaking changes.
- #5141 adds f.eq_unfold lemmas. Now Lean produces the following zoo of rewrite rules:
```
Option.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)
```
  The f.eq_unfold variant is especially useful to rewrite with rw under binders.
- #5136 fixes bugs in recursion over predicates.
Variable inclusion
- #5206 documents that include currently only applies to theorems.
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 as fun x1 x2 => x1 + x2 rather than fun 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.

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.

Pretty printing

#4976 introduces @[app_delab], a macro for creating delaborators for particular constants. The @[app_delab ident] syntax resolves ident to its constant name name and then expands to @[delab app.name].
#4982 fixes a bug where the pretty printer assumed structure projections were type correct (such terms can appear in type mismatch errors). Improves hoverability of #print output for structures.
#5218 and #5239 add pp.exprSizes debugging option. When true, each pretty printed expression is prefixed with [size a/b/c], where a is the size without sharing, b is the actual size, and c is the size with the maximum possible sharing.

Library

#5020 swaps the parameters to Membership.mem. A purpose of this change is to make set-like CoeSort coercions to refer to the eta-expanded function fun x => Membership.mem s x, which can reduce in many computations. Another is that having the s argument first leads to better discrimination tree keys. (See breaking changes.)
Array
- #4970 adds @[ext] attribute to Array.ext.
- #4957 deprecates Array.get_modify.
List
- #4995 upstreams List.findIdx lemmas.
- #5029, #5048 and #5132 add List.Sublist lemmas, some upstreamed. #5077 fixes implicitness in refl/rfl lemma binders. add List.Sublist theorems.
- #5047 upstreams List.Pairwise lemmas.
- #5053, #5124, and #5161 add List.find?/findSome?/findIdx? theorems.
- #5039 adds List.foldlRecOn and List.foldrRecOn recursion principles to prove things about List.foldl and List.foldr.
- #5069 upstreams List.Perm.
- #5092 and #5107 add List.mergeSort and a fast @[csimp] implementation.
- #5103 makes the simp lemmas for List.subset more aggressive.
- #5106 changes the statement of List.getLast?_cons.
- #5123 and #5158 add List.range and List.iota lemmas.
- #5130 adds List.join lemmas.
- #5131 adds List.append lemmas.
- #5152 adds List.erase(|P|Idx) lemmas.
- #5127 makes miscellaneous lemma updates.
- #5153 and #5160 add lemmas about List.attach and List.pmap.
- #5164, #5177, and #5215 add List.find? and List.range'/range/iota lemmas.
- #5196 adds List.Pairwise_erase and related lemmas.
- #5151 and #5163 improve confluence of List simp lemmas. #5105 and #5102 adjust List simp lemmas.
- #5178 removes List.getLast_eq_iff_getLast_eq_some as a simp lemma.
- #5210 reverses the meaning of List.getElem_drop and List.getElem_drop'.
- #5214 moves @[csimp] lemmas earlier where possible.
Nat and Int
- #5104 adds Nat.add_left_eq_self and relatives.
- #5146 adds missing Nat.and_xor_distrib_(left|right).
- #5148 and #5190 improve Nat and Int simp lemma confluence.
- #5165 adjusts Int simp lemmas.
- #5166 adds Int lemmas relating neg and emod/mod.
- #5208 reverses the direction of the Int.toNat_sub simp lemma.
- #5209 adds Nat.bitwise lemmas.
- #5230 corrects the docstrings for integer division and modulus.
Option
- #5128 and #5154 add Option lemmas.
BitVec
- #4889 adds sshiftRight bitblasting.
- #4981 adds Std.Associative and Std.Commutative instances for BitVec.[and|or|xor].
- #4913 enables missingDocs error for BitVec modules.
- #4930 makes parameter names for BitVec more consistent.
- #5098 adds BitVec.intMin. Introduces boolToPropSimps simp set for converting from boolean to propositional expressions.
- #5200 and #5217 rename BitVec.getLsb to BitVec.getLsbD, etc., to bring naming in line with List/Array/etc.
- Theorems: #4977, #4951, #4667, #5007, #4997, #5083, #5081, #4392
UInt
- #4514 fixes naming convention for UInt lemmas.
Std.HashMap and Std.HashSet
- #4943 deprecates variants of hash map query methods. (See breaking changes.)
- #4917 switches the library and Lean to Std.HashMap and Std.HashSet almost everywhere.
- #4954 deprecates Lean.HashMap and Lean.HashSet.
- #5023 cleans up lemma parameters.
Std.Sat (for bv_decide)
- #4933 adds definitions of SAT and CNF.
- #4953 defines "and-inverter graphs" (AIGs) as described in section 3 of Davis-Swords 2013.
Parsec
- #4774 generalizes the Parsec library, allowing parsing of iterable data beyond String such as ByteArray. (See breaking changes.)
- #5115 moves Lean.Data.Parsec to Std.Internal.Parsec for bootstrappng reasons.
Thunk
- #4969 upstreams Thunk.ext.
IO
- #4973 modifies IO.FS.lines to handle \r\n on all operating systems instead of just on Windows.
- #5125 adds createTempFile and withTempFile for creating temporary files that can only be read and written by the current user.
Other fixes or improvements
- #4945 adds Array, Bool and Prod utilities from LeanSAT.
- #4960 adds Relation.TransGen.trans.
- #5012 states WellFoundedRelation Nat using <, not Nat.lt.
- #5011 uses ≠ instead of Not (Eq ...) in Fin.ne_of_val_ne.
- #5197 upstreams Fin.le_antisymm.
- #5042 reduces usage of refine'.
- #5101 adds about if-then-else and Option.
- #5112 adds basic instances for ULift and PLift.
- #5133 and #5168 make fixes from running the simpNF linter over Lean.
- #5156 removes a bad simp lemma in omega theory.
- #5155 improves confluence of Bool simp lemmas.
- #5162 improves confluence of Function.comp simp lemmas.
- #5191 improves confluence of if-then-else simp lemmas.
- #5147 adds @[elab_as_elim] to Quot.rec, Nat.strongInductionOn and Nat.casesStrongInductionOn, and also renames the latter two to Nat.strongRecOn and Nat.casesStrongRecOn (deprecated in #5179).
- #5180 disables some simp lemmas with bad discrimination tree keys.
- #5189 cleans up internal simp lemmas that had leaked.
- #5198 cleans up allowUnsafeReducibility.
- #5229 removes unused lemmas from some simp tactics.
- #5199 removes >6 month deprecations.

Lean internals

Performance
- Some core algorithms have been rewritten in C++ for performance.
  - #4910 and #4912 reimplement instantiateLevelMVars.
  - #4915, #4922, and #4931 reimplement instantiateExprMVars, 30% faster on a benchmark.
- #4934 has optimizations for the kernel's Expr equality test.
- #4990 fixes bug in hashing for the kernel's Expr equality test.
- #4935 and #4936 skip some PreDefinition transformations if they are not needed.
- #5225 adds caching for visited exprs at CheckAssignmentQuick in ExprDefEq.
- #5226 maximizes term sharing at instantiateMVarDeclMVars, used by runTactic.
Diagnostics and profiling
- #4923 adds profiling for instantiateMVars in Lean.Elab.MutualDef, which can be a bottleneck there.
- #4924 adds diagnostics for large theorems, controlled by the diagnostics.threshold.proofSize option.
- #4897 improves display of diagnostic results.
Other fixes or improvements
- #4921 cleans up Expr.betaRev.
- #4940 fixes tests by not writing directly to stdout, which is unreliable now that elaboration and reporting are executed in separate threads.
- #4955 documents that stderrAsMessages is now the default on the command line as well.
- #4647 adjusts documentation for building on macOS.
- #4987 makes regular mvar assignments take precedence over delayed ones in instantiateMVars. Normally delayed assignment metavariables are never directly assigned, but on errors Lean assigns sorry to unassigned metavariables.
- #4967 adds linter name to errors when a linter crashes.
- #5043 cleans up command line snapshots logic.
- #5067 minimizes some imports.
- #5068 generalizes the monad for addMatcherInfo.
- f71a1f adds missing test for #5126.
- #5201 restores a test.
- #3698 fixes a bug where label attributes did not pass on the attribute kind.
- Typos: #5080, #5150, #5202

Compiler, runtime, and FFI

#3106 moves frontend to new snapshot architecture. Note that Frontend.processCommand and FrontendM are no longer used by Lean core, but they will be preserved.
#4919 adds missing include in runtime for AUTO_THREAD_FINALIZATION feature on Windows.
#4941 adds more LEAN_EXPORTs for Windows.
#4911 improves formatting of CLI help text for the frontend.
#4950 improves file reading and writing.
- readBinFile and readFile now only require two system calls (stat + read) instead of one read per 1024 byte chunk.
- Handle.getLine and Handle.putStr no longer get tripped up by NUL characters.
#4971 handles the SIGBUS signal when detecting stack overflows.
#5062 avoids overwriting existing signal handlers, like in rust-lang/rust#69685.
#4860 improves workarounds for building on Windows. Splits libleanshared on Windows to avoid symbol limit, removes the LEAN_EXPORT denylist workaround, adds missing LEAN_EXPORTs.
#4952 output panics into Lean's redirected stderr, ensuring panics ARE visible as regular messages in the language server and properly ordered in relation to other messages on the command line.
#4963 links LibUV.

Lake

#5030 removes dead code.
#4770 adds additional fields to the package configuration which will be used by Reservoir. See the PR description for details.

DevOps/CI

#4914 and #4937 improve the release checklist.
#4925 ignores stale leanpkg tests.
#5003 upgrades actions/cache in CI.
#5010 sets save-always in cache actions in CI.
#5008 adds more libuv search patterns for the speedcenter.
#5009 reduce number of runs in the speedcenter for "fast" benchmarks from 10 to 3.
#5014 adjusts lakefile editing to use new git syntax in pr-release workflow.
#5025 has pr-release workflow pass --retry to curl.
#5022 builds MacOS Aarch64 release for PRs by default.
#5045 adds libuv to the required packages heading in macos docs.
#5034 fixes the install name of libleanshared_1 on macOS.
#5051 fixes Windows stage 0.
#5052 fixes 32bit stage 0 builds in CI.
#5057 avoids rebuilding leanmanifest in each build.
#5099 makes restart-on-label workflow also filter by commit SHA.
#4325 adds CaDiCaL.

Breaking changes

LibUV is now required to build Lean. This change only affects developers who compile Lean themselves instead of obtaining toolchains via elan. We have updated the official build instructions with information on how to obtain LibUV on our supported platforms. (#4963)
Recursive definitions with a decreasing_by clause that begins with simp_wf may break. Try removing simp_wf or replacing it with simp. (#5016)
The behavior of rw [f] where f is a non-recursive function defined by pattern matching changed.

For example, preciously, rw [Option.map] would rewrite Option.map f o to match o with … . Now this rewrite fails because it will use the equational lemmas, and these require constructors – just like for List.map.

Remedies:
- Split on o before rewriting.
- Use rw [Option.map.eq_def], which rewrites any (saturated) application of Option.map.
- Use set_option backward.eqns.nonrecursive false when defining the function in question. (#4154)
The unified handling of equation lemmas for recursive and non-recursive functions can break existing code, as there now can be extra equational lemmas:
- Explicit uses of f.eq_2 might have to be adjusted if the numbering changed.
- Uses of rw [f] or simp [f] may no longer apply if they previously matched (and introduced a match statement), when the equational lemmas got more fine-grained.
  
  In this case either case analysis on the parameters before rewriting helps, or setting the option backward.eqns.deepRecursiveSplit false while defining the function.
(#5129, #5207)
The reduceCtorEq simproc is now optional, and it might need to be included in lists of simp lemmas, like simp only [reduceCtorEq]. This simproc is responsible for reducing equalities of constructors. (#5167)
Nat.strongInductionOn is now Nat.strongRecOn and Nat.caseStrongInductionOn to Nat.caseStrongRecOn. (#5147)
The parameters to Membership.mem have been swapped, which affects all Membership instances. (#5020)
The meanings of List.getElem_drop and List.getElem_drop' have been reversed and the first is now a simp lemma. (#5210)
The Parsec library has moved from Lean.Data.Parsec to Std.Internal.Parsec. The Parsec type is now more general with a parameter for an iterable. Users parsing strings can migrate to Parser in the Std.Internal.Parsec.String namespace, which also includes string-focused parsing combinators. (#4774)
The Lean module has switched from Lean.HashMap and Lean.HashSet to Std.HashMap and Std.HashSet (#4943). Lean.HashMap and Lean.HashSet are now deprecated (#4954) and will be removed in a future release. Users of Lean APIs that interact with hash maps, for example Lean.Environment.const2ModIdx, might encounter minor breakage due to the following changes from Lean.HashMap to Std.HashMap:
- query functions use the term get instead of find, (#4943)
- the notation map[key] no longer returns an optional value but instead expects a proof that the key is present in the map. The previous behavior is available via the map[key]? notation.