v4.9.0
版本发布时间: 2024-07-01 08:21:09
leanprover/lean4最新发布版本:v4.12.0-rc1(2024-09-03 11:01:10)
Language features, tactics, and metaprograms
-
Definition transparency
-
#4053 adds the
seal
andunseal
commands, which make definitions locally be irreducible or semireducible. -
#4061 marks functions defined by well-founded recursion with
@[irreducible]
by default, which should prevent the expensive and often unfruitful unfolding of such definitions (see breaking changes below).
-
#4053 adds the
-
Incrementality
- #3940 extends incremental elaboration into various steps inside of declarations: definition headers, bodies, and tactics. .
-
250994 and 67338b add
@[incremental]
attribute to mark an elaborator as supporting incremental elaboration. - #4259 improves resilience by ensuring incremental commands and tactics are reached only in supported ways.
-
#4268 adds special handling for
:= by
so that stray tokens in tactic blocks do not inhibit incrementality. -
#4308 adds incremental
have
tactic. - #4340 fixes incorrect info tree reuse.
-
#4364 adds incrementality for careful command macros such as
set_option in theorem
,theorem foo.bar
, andlemma
. - #4395 adds conservative fix for whitespace handling to avoid incremental reuse leading to goals in front of the text cursor being shown.
- #4407 fixes non-incremental commands in macros blocking further incremental reporting.
- #4436 fixes incremental reporting when there are nested tactics in terms.
-
Functional induction
- #4135 ensures that the names used for functional induction are reserved.
-
#4327 adds support for structural recursion on reflexive types.
For example,
inductive Many (α : Type u) where | none : Many α | more : α → (Unit → Many α) → Many α def Many.map {α β : Type u} (f : α → β) : Many α → Many β | .none => .none | .more x xs => .more (f x) (fun _ => (xs ()).map f) #check Many.map.induct /- Many.map.induct {α β : Type u} (f : α → β) (motive : Many α → Prop) (case1 : motive Many.none) (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) : ∀ (a : Many α), motive a -/
- #3903 makes the Lean frontend normalize all line endings to LF before processing. This lets Lean be insensitive to CRLF vs LF line endings, improving the cross-platform experience and making Lake hashes be faithful to what Lean processes.
- #4130 makes the tactic framework be able to recover from runtime errors (for example, deterministic timeouts or maximum recursion depth errors).
-
split
tactic -
apply
tactic-
#3929 makes error message for
apply
show implicit arguments in unification errors as needed. ModifiesMessageData
type (see breaking changes below).
-
#3929 makes error message for
-
cases
tactic-
#4224 adds support for unification of offsets such as
x + 20000 = 20001
incases
tactic.
-
#4224 adds support for unification of offsets such as
-
omega
tactic -
simp
tactic-
#4176 makes names of erased lemmas clickable.
-
#4208 adds a pretty printer for discrimination tree keys.
-
#4202 adds
Simp.Config.index
configuration option, which controls whether to use the full discrimination tree when selecting candidate simp lemmas. Whenindex := false
, only the head function is taken into account, like in Lean 3. This feature can help users diagnose tricky simp failures or issues in code from libraries developed using Lean 3 and then ported to Lean 4.In the following example, it will report that
foo
is a problematic theorem.opaque f : Nat → Nat → Nat @[simp] theorem foo : f x (x, y).2 = y := by sorry example : f a b ≤ b := by set_option diagnostics true in simp (config := { index := false }) /- [simp] theorems with bad keys foo, key: f _ (@Prod.mk ℕ ℕ _ _).2 -/
With the information above, users can annotate theorems such as
foo
usingno_index
for problematic subterms. Example:opaque f : Nat → Nat → Nat @[simp] theorem foo : f x (no_index (x, y).2) = y := by sorry example : f a b ≤ b := by simp -- `foo` is still applied with `index := true`
-
#4274 prevents internal
match
equational theorems from appearing in simp trace. -
#4177 and #4359 make
simp
continue even if a simp lemma does not elaborate, if the tactic state is in recovery mode. -
#4341 fixes panic when applying
@[simp]
to malformed theorem syntax. -
#4345 fixes
simp
so that it does not use the forward version of a user-specified backward theorem. -
#4352 adds missing
dsimp
simplifications for fixed parameters of generated congruence theorems. -
#4362 improves trace messages for
simp
so that constants are hoverable.
-
-
Elaboration
-
#4046 makes subst notation (
he ▸ h
) try rewriting in both directions even when there is no expected type available. -
#3328 adds support for identifiers in autoparams (for example,
rfl
in(h : x = y := by exact rfl)
). -
#4096 changes how the type in
let
andhave
is elaborated, requiring that any tactics in the type be evaluated before proceeding, improving performance. - #4215 ensures the expression tree elaborator commits to the computed "max type" for the entire arithmetic expression.
- #4267 cases signature elaboration errors to show even if there are parse errors in the body.
-
#4368 improves error messages when numeric literals fail to synthesize an
OfNat
instance, including special messages warning when the expected type of the numeral can be a proposition.
-
#4046 makes subst notation (
- Metaprogramming
- Work toward implementing
grind
tactic-
0a515e and #4164 add
grind_norm
andgrind_norm_proc
attributes and@[grind_norm]
theorems. -
#4170, #4221, and #4249 create
grind
preprocessor and core module. -
#4235 and d6709e add special
cases
tactic togrind
along with@[grind_cases]
attribute to mark types that thiscases
tactic should automatically apply to. -
#4243 adds special
injection?
tactic togrind
.
-
0a515e and #4164 add
-
Other fixes or improvements
-
#4065 fixes a bug in the
Nat.reduceLeDiff
simproc. - #3969 makes deprecation warnings activate even for generalized field notation ("dot notation").
-
#4132 fixes the
sorry
term so that it does not activate the implicit lambda feature -
9803c5 and 47c8e3 move
cdot
andcalc
parsers toLean
namespace. -
#4252 fixes the
case
tactic so that it is usable in macros by having it erase macro scopes from the tag. -
26b671 and cc33c3 extract
haveId
syntax. -
#4335 fixes bugs in partial
calc
tactic when there is mdata or metavariables. -
#4329 makes
termination_by?
report unused each unused parameter as_
.
-
#4065 fixes a bug in the
- Docs: #4238, #4294, #4338.
Language server, widgets, and IDE extensions
- #4066 fixes features like "Find References" when browsing core Lean sources.
- #4254 allows embedding user widgets in structured messages. Companion PR is vscode-lean4#449.
- #4445 makes watchdog more resilient against badly behaving clients.
Library
-
#4059 upstreams many
List
andArray
operations and theorems from Batteries. -
#4055 removes the unused
Inhabited
instance forSubtype
. -
#3967 adds dates in existing
@[deprecated]
attributes. -
#4231 adds boilerplate
Char
,UInt
, andFin
theorems. -
#4205 fixes the
MonadStore
type classes to usesemiOutParam
. -
#4350 renames
IsLawfulSingleton
toLawfulSingleton
. -
Nat
-
Array
-
#4074 improves the functional induction principle
Array.feraseIdx.induct
.
-
#4074 improves the functional induction principle
-
List
-
#4172 removes
@[simp]
fromList.length_pos
.
-
#4172 removes
-
Option
-
BitVec
- Theorems: #3920, #4095, #4075, #4148, #4165, #4178, #4200, #4201, #4298, #4299, #4257, #4179, #4321, #4187.
-
#4193 adds simprocs for reducing
x >>> i
andx <<< i
wherei
is a bitvector literal. -
#4194 adds simprocs for reducing
(x <<< i) <<< j
and(x >>> i) >>> j
wherei
andj
are natural number literals. -
#4229 redefines
rotateLeft
/rotateRight
to use modulo reduction of shift offset. -
0d3051 makes
<num>#<term>
bitvector literal notation global.
-
Char
/String
-
HashMap
-
#4248 fixes implicitness of typeclass arguments in
HashMap.ofList
.
-
#4248 fixes implicitness of typeclass arguments in
-
IO
-
#4036 adds
IO.Process.getCurrentDir
andIO.Process.setCurrentDir
for adjusting the current process's working directory.
-
#4036 adds
- Cleanup: #4077, #4189, #4304.
- Docs: #4001, #4166, #4332.
Lean internals
- Defeq and WHNF algorithms
-
Definition transparency
-
#4052 adds validation to application of
@[reducible]
/@[semireducible]
/@[irreducible]
attributes (withlocal
/scoped
modifiers as well). Settingset_option allowUnsafeReductibility true
turns this validation off.
-
#4052 adds validation to application of
- Inductive types
- Diagnostics and profiling
-
Typeclass resolution
-
#4119 fixes multiple issues with TC caching interacting with
synthPendingDepth
, addsmaxSynthPendingDepth
option with default value1
. - #4210 ensures local instance cache does not contain multiple copies of the same instance.
-
#4216 fix handling of metavariables, to avoid needing to set the option
backward.synthInstance.canonInstances
tofalse
.
-
#4119 fixes multiple issues with TC caching interacting with
-
Other fixes or improvements
-
#4080 fixes propagation of state for
Lean.Elab.Command.liftCoreM
andLean.Elab.Command.liftTermElabM
. -
#3944 makes the
Repr
deriving handler be consistent betweenstructure
andinductive
for how types and proofs are erased. -
#4113 propagates
maxHeartbeats
to kernel to control "(kernel) deterministic timeout" error. -
#4125 reverts #3970 (monadic generalization of
FindExpr
). - #4128 catches stack overflow in auto-bound implicits feature.
-
#4129 adds
tryCatchRuntimeEx
combinator to replacecatchRuntimeEx
reader state. - #4155 simplifies the expression canonicalizer.
- #4151 and #4369 add many missing trace classes.
- #4185 makes congruence theorem generators clean up type annotations of argument types.
- #4192 fixes restoration of infotrees when auto-bound implicit feature is activated, fixing a pretty printing error in hovers and strengthening the unused variable linter.
-
dfb496 fixes
declareBuiltin
to allow it to be called multiple times per declaration. - Cleanup: #4112, #4126, #4091, #4139, #4153.
- Tests: 030406, #4133.
-
#4080 fixes propagation of state for
Compiler, runtime, and FFI
- #4100 improves reset/reuse algorithm; it now runs a second pass relaxing the constraint that reused memory cells must only be for the exact same constructor.
-
#2903 fixes segfault in old compiler from mishandling
noConfusion
applications. - #4311 fixes bug in constant folding.
- #3915 documents the runtime memory layout for inductive types.
Lake
-
#4057 adds support for docstrings on
require
commands. -
#4088 improves hovers for
family_def
andlibrary_data
commands. -
#4147 adds default
README.md
to package templates -
#4261 extends
lake test
help page, adds help page forlake check-test
, addslake lint
and tag@[lint_driver]
, adds support for specifying test and lint drivers from dependencies, addstestDriverArgs
andlintDriverArgs
options, adds support for library test drivers, makeslake check-test
andlake check-lint
only load the package without dependencies. -
#4270 adds
lake pack
andlake unpack
for packing and unpacking Lake build artifacts from an archive. -
#4083 Switches the manifest format to use
major.minor.patch
semantic versions. Major version increments indicate breaking changes (e.g., new required fields and semantic changes to existing fields). Minor version increments (after0.x
) indicate backwards-compatible extensions (e.g., adding optional fields, removing fields). This change is backwards compatible. Lake will still successfully read old manifests with numeric versions. It will treat the numeric versionN
as semantic version0.N.0
. Lake will also accept manifest versions with-
suffixes (e.g.,x.y.z-foo
) and then ignore the suffix. -
#4273 adds a lift from
JobM
toFetchM
for backwards compatibility reasons. -
#4351 fixes
LogIO
-to-CliM
-lifting performance issues. - #4343 make Lake store the dependency trace for a build in the cached build long and then verifies that it matches the trace of the current build before replaying the log.
-
#4402 moves the cached log into the trace file (no more
.log.json
). This means logs are no longer cached on fatal errors and this ensures that an out-of-date log is not associated with an up-to-date trace. Separately,.hash
file generation was changed to be more reliable as well. The.hash
files are deleted as part of the build and always regenerate with--rehash
. - Other fixes or improvements
DevOps
-
#3984 adds a script (
script/rebase-stage0.sh
) forgit rebase -i
that automatically updates each stage0. - #4108 finishes renamings from transition to Std to Batteries.
- #4109 adjusts the Github bug template to mention testing using live.lean-lang.org.
-
#4136 makes CI rerun only when
full-ci
label is added or removed. -
#4175 and 72b345 switch to using
#guard_msgs
to run tests as much as possible. -
#3125 explains the Lean4
pygments
lexer. - #4247 sets up a procedure for preparing release notes.
- #4032 modernizes build instructions and workflows.
- #4255 moves some expensive checks from merge queue to releases.
- #4265 adds aarch64 macOS as native compilation target for CI.
- f05a82 restores macOS aarch64 install suffix in CI
- #4317 updates build instructions for macOS.
-
#4333 adjusts workflow to update Batteries in manifest when creating
lean-pr-testing-NNNN
Mathlib branches. -
#4355 simplifies
lean4checker
step of release checklist. -
#4361 adds installing elan to
pr-release
CI step.
Breaking changes
While most changes could be considered to be a breaking change, this section makes special note of API changes.
-
Nat.zero_or
andNat.or_zero
have been swapped (#4094). -
IsLawfulSingleton
is nowLawfulSingleton
(#4350). -
BitVec.rotateLeft
andBitVec.rotateRight
now take the shift modulo the bitwidth (#4229). - These are no longer simp lemmas:
List.length_pos
(#4172),Option.bind_eq_some
(#4314). - Types in
let
andhave
(both the expressions and tactics) may fail to elaborate due to new restrictions on what sorts of elaboration problems may be postponed (#4096). In particular, tactics embedded in the type will no longer make use of the type ofvalue
in expressions such aslet x : type := value; body
. - Now functions defined by well-founded recursion are marked with
@[irreducible]
by default (#4061). Existing proofs that hold by definitional equality (e.g.rfl
) can be rewritten to explictly unfold the function definition (usingsimp
,unfold
,rw
), or the recursive function can be temporarily made semireducible (usingunseal f in
before the command), or the function definition itself can be marked as@[semireducible]
to get the previous behavior. - Due to #3929:
-
The
MessageData.ofPPFormat
constructor has been removed. Its functionality has been split into two:- for lazy structured messages, please use
MessageData.lazy
; - for embedding
Format
orFormatWithInfos
, useMessageData.ofFormatWithInfos
.
An example migration can be found in #3929.
- for lazy structured messages, please use
-
The
MessageData.ofFormat
constructor has been turned into a function. If you need to inspectMessageData
, you can pattern-match onMessageData.ofFormatWithInfos
.
-
1、 lean-4.9.0-darwin.tar.zst 183.89MB
2、 lean-4.9.0-darwin.zip 256.82MB
3、 lean-4.9.0-darwin_aarch64.tar.zst 179.85MB
4、 lean-4.9.0-darwin_aarch64.zip 252.26MB
5、 lean-4.9.0-linux.tar.zst 189.34MB
6、 lean-4.9.0-linux.zip 323.43MB
7、 lean-4.9.0-linux_aarch64.tar.zst 187.34MB
8、 lean-4.9.0-linux_aarch64.zip 327.81MB
9、 lean-4.9.0-linux_wasm32.tar.zst 134.53MB
10、 lean-4.9.0-linux_wasm32.zip 183.55MB
11、 lean-4.9.0-linux_x86.tar.zst 166.79MB
12、 lean-4.9.0-linux_x86.zip 226.35MB
13、 lean-4.9.0-windows.tar.zst 189.75MB
14、 lean-4.9.0-windows.zip 265.78MB