Highlights🔗

example (i j : Nat) (xs : Array Nat) (hi : i < xs.size) (hj: j < xs.size) :=
  我与
  | 0 => x
  | _ => xs[i]'?_ + xs[j]'?_
其中 x := 13
最后all_goals假设

Language🔗

• #6672 filters out all declarations from Lean.*, *.Tactic.*, and *.Linter.* from the results of exact? and rw?.

• #7395 changes the show t tactic to match its documentation. Previously it was a synonym for change t, but now it finds the first goal that unifies with the term t and moves it to the front of the goal list.

• #7639 changes the generated below and brecOn implementations for reflexive inductive types to support motives in Sort u rather than Type u.

• #8337 adjusts the experimental module system to not export any private declarations from modules.

• #8373 enables transforming nondependent lets into haves in a number of contexts: the bodies of nonrecursive definitions, equation lemmas, smart unfolding definitions, and types of theorems. A motivation for this change is that when zeta reduction is disabled, simp can only effectively rewrite have expressions (e.g. split uses simp with zeta reduction disabled), and so we cache the nondependence calculations by transforming lets to haves. The transformation can be disabled using set_option cleanup.letToHave false.

• #8387 improves the error messages produced by end and prevents invalid end commands from closing scopes on failure.

• #8419 introduces an explicit defeq attribute to mark theorems that can be used by dsimp. The benefit of an explicit attribute over the prior logic of looking at the proof body is that we can reliably omit theorem bodies across module boundaries. It also helps with intra-file parallelism.

• #8519 makes the equational theorems of non-exposed defs private. If the author of a module chose not to expose the body of their function, then they likely don't want that implementation to leak through equational theorems. Helps with #8419.

• #8543 adds type classes for grind to embed types into Int, for cutsat. This allows, for example, treating Fin n, or Mathlib's ℕ+ in a uniform and extensible way.

• #8568 modifies the structure elaborator to add local terminfo for structure fields and explicit parent projections, enabling "go to definition" when there are dependent fields.

• #8574 adds an additional diff mode to the error-message hint suggestion widget that displays diffs per word rather than per character.

• #8596 makes guard_msgs.diff=true the default. The main usage of #guard_msgs is for writing tests, and this makes staring at altered test outputs considerably less tiring.

• #8609 uses grind to shorten some proofs in the LRAT checker. The intention is not particularly to improve the quality or maintainability of these proofs (although hopefully this is a side effect), but just to give grind a work out.

• #8619 fixes an internalization (aka preprocessing) issue in grind when applying injectivity theorems.

• #8621 fixes a bug in the equality-resolution procedure used by grind. The procedure now performs a topological sort so that every simplified theorem declaration is emitted before any place where it is referenced. Previously, applying equality resolution to

  h : ∀ x, p x a → ∀ y, p y b → x ≠ y
  

  in the example

  例子
    （p：Nat → Nat → Prop）
    (a b c : 纳特)
    (h : ∀ x, p x a → ∀ y, p y b → x ≠ y)
    (h₁：p c a)
    (h2：PCB)：
    错误 := 通过
    磨
  

  caused grind to produce the incorrect term

  p ?y a → ∀ y, p y b → 假
  

  The patch eliminates this error, and the following correct simplified theorem is generated

  ∀ y, p y a → p y b → 假
  

• #8622 adds a test case / use case example for grind, setting up the very basics of IndexMap, modelled on Rust's indexmap. It is not intended as a complete implementation: just enough to exercise grind.

• #8625 improves the diagnostic information produced by grind when it succeeds. We now include the list of case-splits performed, and the number of application per function symbol.

• #8633 implements case-split tracking in grind. The information is displayed when grind fails or diagnostic information is requested. Examples:

  • Failure

• #8637 adds background theorems for normalizing IntModule expressions using reflection.

• #8638 improves the diagnostic information produced by grind. It now sorts the equivalence classes by generation and then Expr.lt.

• #8639 completes the ToInt family of type classes which grind will use to embed types into the integers for cutsat. It contains instances for the usual concrete data types (Fin, UIntX, IntX, BitVec), and is extensible (e.g. for Mathlib's PNat).

• #8641 adds the #print sig $ident variant of the #print command, which omits the body. This is useful for testing meta-code, in the

  #guard_msgs (drop trace, all) in #print sig foo
  

  idiom. The benefit over #check is that it shows the declaration kind, reducibility attributes (and in the future more built-in attributes, like @[defeq] in #8419). (One downside is that #check shows unused function parameter names, e.g. in induction principles; this could probably be refined.)

• #8645 adds many helper theorems for the future IntModule linear arithmetic procedure in grind. It also adds helper theorems for normalizing input atoms and support for disequality in the new linear arithmetic procedure in grind.

• #8650 adds helper theorems for coefficient normalization and equality detection. This theorems are for the linear arithmetic procedure in grind.

• #8662 adds a warn.sorry option (default true) that logs the "declaration uses 'sorry'" warning when declarations contain sorryAx. When false, the warning is not logged.

• #8670 adds helper theorems that will be used to interface the CommRing module with the linarith procedure in grind.

• #8671 allow structures to have non-bracketed binders, making it consistent with inductive.

• #8677 adds the basic infrastructure for the linarith module in grind.

• #8680 adds the reify? and denoteExpr for the new linarith module in grind.

• #8682 uses the CommRing module to normalize linarith inequalities.

• #8687 implements the infrastructure for constructing proof terms in the linarith procedure in grind. It also adds the ToExpr instances for the reified objects.

• #8689 implements proof term generation for the CommRing and linarith interface. It also fixes the CommRing helper theorems.

• #8690 implements the main framework of the model search procedure for the linarith component in grind. It currently handles only inequalities. It can already solve simple goals such as

  example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b c : α)
      : a < b → b < c → c < a → False := by
    磨
  
  

• #8693 修复了用于连接环和环的表示函数 磨削中的 linarith 模块。

• #8694 在 linarith 中实现对 One.one 的特殊支持 structure is a ordered ring. It also fixes bugs during initialization.

• #8697 实现对 grind 线性不等式的支持 算法过程并简化其设计。一些例子可以 已经解决：

  open Lean.Grind
  example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b c d : α)
      : a + d < c → b = a + (2:Int)*d → b - d > c → False := by
    grind
  
  

• #8708 fixes an internalization bug in the interface between linarith and ring modules in grind. The CommRing module may create new terms during normalization.

• #8713 fixes a bug in the commutative ring module used in grind. It was missing simplification opportunities.

• #8715 implements the basic infrastructure for processing disequalities in the grind linarith module. We still have to implement backtracking.

• #8723 implements a finally section following a (potentially empty) where block. where ... finally opens a tactic sequence block in which the goals are the unassigned metavariables from the definition body and its auxiliary definitions that arise from use of let rec and where.

• #8730 adds support for throwing named errors with associated error explanations. In particular, it adds elaborators for the syntax defined in #8649, which use the error-explanation infrastructure added in #8651. This includes completions, hovers, and jump-to-definition for error names.

• #8733 implements disequality splitting and non-chronological backtracking for the grind linarith procedure.

  example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c d : α)
      : a ≤ b → a - c ≥ 0 + d → d ≤ 0 → d ≥ 0 → b = c → a ≠ b → False := by
    磨
  

• #8751 adds the nondep field of Expr.letE to the C++ data model. Previously this field has been unused, and in followup PRs the elaborator will use it to encode have expressions (non-dependent lets). The kernel does not verify that nondep is correctly applied during typechecking. The letE delaborator now prints haves when nondep is true, though have still elaborates as letFun for now. Breaking change: Expr.updateLet! is renamed to Expr.updateLetE!.

• #8753 fixes a bug in simp where it was not resetting the set of zeta-delta reduced let definitions between simp calls. It also fixes a bug where simp would report zeta-delta reduced let definitions that weren't given as simp arguments (these extraneous let definitions appear due to certain processes temporarily setting zetaDelta := true). This PR also modifies the metaprogramming interface for the zeta-delta tracking functions to be re-entrant and to prevent this kind of no-reset bug from occurring again. Closes #6655.

• #8756 implements counterexamples for grind linarith. Example:

  example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c d : α)
      : b ≥ 0 → c > b → d > b → a ≠ b + c → a > b + c → a < b + d → False := by
    磨
  

  produces the counterexample

  := 7/2
  乙：= 1
  c := 2
  d:=3
  

• #8759 implements model-based theory combination for grind linarith. Example:

  example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (f : α → α → α) (x y z : α)
      : z ≤ x → x ≤ 1 → z = 1 → f x y = 2 → f 1 y = 2 := 通过
    磨
  

• #8763 corrects the handling of explicit monotonicity proofs for mutual partial_fixpoint definitions.

• #8773 implements support for the heterogeneous (k : Nat) * (a : R) in ordered modules. Example:

  variable (R : Type u) [IntModule R] [LinearOrder R] [IntModule.IsOrdered R]
  
  

• #8774 添加了一个用于禁用 grind 中的 cutsat 过程的选项。 linarith 模块接管线性整数/nat 约束。例子：

  set_option trace.grind.cutsat.assert true in -- cutsat should **not** process the following constraints
  example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) : ¬ 12*y - 4* z < 0 := by
    grind -cutsat -- `linarith` module solves it
  

• #8775 为 Int.negSucc 添加 grind 归一化定理。例子：

  example (p : Int) (n : Nat) (hmp : Int.negSucc (n + 1) + 1 = p)
      (hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)) : p = Int.negSucc n := by
    grind
  

• #8776 确保用户提供的 natCast 应用程序正确 内化在grinding cutsat模块中。

• #8777 在交换环模块中实现基本的 Field 支持 在 grind 中。目前只是按数字除法。示例：

  open Lean Grind
  
  

• #8780 makes Lean code generation respect the module name provided through lean --setup.

• #8786 improves the support for fields in grind. New supported examples:

  example [Field α] [IsCharP α 0] (x : α) : x ≠ 0 → (4 / x)⁻¹ * ((3 * x^3) / x)^2 * ((1 / (2 * x))⁻¹)^3 = 18 * x^8 := by grind
  example [Field α] (a : α) : 2 * a ≠ 0 → 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind
  example [Field α] [IsCharP α 0] (a : α) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind
  example [Field α] [IsCharP α 0] (a b : α) : 2*b - a = a + b → 1 / a + 1 / (2 * a) = 3 / b := by grind
  example [Field α] [NoNatZeroDivisors α] (a : α) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind
  example [Field α] {x y z w : α} : x / y = z / w → y ≠ 0 → w ≠ 0 → x * w = z * y := by grind
  example [Field α] (a : α) : a = 0 → a ≠ 1 := by grind
  example [Field α] (a : α) : a = 0 → a ≠ 1 - a := by grind
  

• #8789 implements the Rabinowitsch transformation for Field disequalities in grind. For example, this transformation is necessary for solving:

  example [Field α] (a : α) : a^2 = 0 → a = 0 := by
    磨
  

• #8791 ensures the grind linarith module is activated for any type that implements only IntModule. That is, the type does not need to be a preorder anymore.

• #8792 makes the clear_value tactic preserve the order of variables in the local context. This is done by adding Lean.MVarId.withRevertedFrom, which reverts all local variables starting from a given variable, rather than only the ones that depend on it.

• #8794 adds a module Lean.Util.CollectLooseBVars with a function Expr.collectLooseBVars that collects the set of loose bound variables in an expression. That is, it computes the set of all i such that e.hasLooseBVar i is true.

• #8795 ensures that auxliary terms are not internalized by the ring and linarith modules.

• #8796 fixes grind linarith term internalization and support for HSMul.

• #8798 adds the following instance

  instance [Field α] [LinearOrder α] [Ring.IsOrdered α] : IsCharP α 0
  

  The goal is to ensure we do not perform unnecessary case-splits in our test suite.

• #8804 implements first-class support for nondependent let expressions in the elaborator; recall that a let expression let x : t := v; b is called nondependent if fun x : t => b typechecks, and the notation for a nondependent let expression is have x := v; b. Previously we encoded have using the letFun function, but now we make use of the nondep flag in the Expr.letE constructor for the encoding. This has been given full support throughout the metaprogramming interface and the elaborator. Key changes to the metaprogramming interface:

  • Local context ldecls with nondep := true are generally treated as cdecls. This is because in the body of a have expression the variable is opaque. Functions like LocalDecl.isLet by default return false for nondependent ldecls. In the rare case where it is needed, they take an additional optional allowNondep : Bool flag (defaults to false) if the variable is being processed in a context where the value is relevant.

  • Functions such as mkLetFVars by default generalize nondependent let variables and create lambda expressions for them. The generalizeNondepLet flag (default true) can be set to false if have expressions should be produced instead. Breaking change: Uses of letLambdaTelescope/mkLetFVars need to use generalizeNondepLet := false. See the next item.

  • There are now some mapping functions to make telescoping operations more convenient. See mapLetTelescope and mapLambdaLetTelescope. There is also mapLetDecl as a counterpart to withLetDecl for creating let/have expressions.

  • Important note about the generalizeNondepLet flag: it should only be used for variables in a local context that the metaprogram "owns". Since nondependent let variables are treated as constants in most cases, the value field might refer to variables that do not exist, if for example those variables were cleared or reverted. Using mapLetDecl is always fine.

  • The simplifier will cache its let dependence calculations in the nondep field of let expressions.

  • The intro tactic still produces dependent local variables. Given that the simplifier will transform lets into haves, it would be surprising if that would prevent intro from creating a local variable whose value cannot be used.

• #8809 introduces the basic theory of ordered modules over Nat (i.e. without subtraction), for grind. We'll solve problems here by embedding them in the IntModule envelope.

• #8810 implements equality elimination in grind linarith. The current implementation supports only IntModule and IntModule + NoNatZeroDivisors

• #8813 adds some basic lemmas about grind internal notions of modules.

• #8815 refactors the way simp arguments are elaborated: Instead of changing the SimpTheorems structure as we go, this elaborates each argument to a more declarative description of what it does, and then apply those. This enables more interesting checks of simp arguments that need to happen in the context of the eventually constructed simp context (the checks in #8688), or after simp has run (unused argument linter #8901).

• #8828 extends the experimental module system to support resolving private names imported (transitively) through import all.

• #8835 defines the embedding of a CommSemiring into its CommRing envelope, injective when the CommSemiring is cancellative. This will be used by grind to prove results in Nat.

• #8836 generalizes #8835 to the noncommutative case, allowing us to embed a Lean.Grind.Semiring into a Lean.Grind.Ring.

• #8845 implements the proof-by-reflection infrastructure for embedding semiring terms as ring ones.

• #8847 relaxes the assumptions for Lean.Grind.IsCharP from Ring to Semiring, and provides an alternative constructor for rings.

• #8848 generalizes the internal grind instance

  instance [Field α] [LinearOrder α] [Ring.IsOrdered α] : IsCharP α 0
  

  to

  instance [Ring α] [Preorder α] [Ring.IsOrdered α] : IsCharP α 0
  

• #8855 refactors Lean.Grind.NatModule/IntModule/Ring.IsOrdered.

• #8859 shows the equivalence between Lean.Grind.NatModule.IsOrdered and Lean.Grind.IntModule.IsOrdered over an IntModule.

• #8865 allows simp to recognize and warn about simp lemmas that are likely looping in the current simp set. It does so automatically whenever simplification fails with the dreaded “max recursion depth” error fails, but it can be made to do it always with set_option linter.loopingSimpArgs true. This check is not on by default because it is somewhat costly, and can warn about simp calls that still happen to work.

• #8874 skips attempting to compute a module name from the file name and root directory (i.e., lean -R) if a name is already provided via lean --setup.

• #8880 makes simp consult its own cache more often, to avoid replicating work.

• #8882 adds @[expose] annotations to terms that appear in grind proof certificates, so grind can be used in the module system. It's possible/likely that I haven't identified all of them yet.

• #8890 adds docstrings to the Lean.Grind algebra type classes, as these will appear in the reference manual explaining how to extend grind algebra solvers to new types. Also removes some redundant fields.

• #8892 corrects the pretty printing of grind modifiers. Previously @[grind →] was being pretty printed as @[grind→ ] (Space on the right of the symbol, rather than left.) This fixes the pretty printing of attributes, and preserves the presence of spaces after the symbol in the output of grind?.

• #8893 fixes a bug in the dvd propagation function in cutsat.

• #8901 adds a linter (linter.unusedSimpArgs) that complains when a simp argument (simp [foo]) is unused. It should do the right thing if the simp invocation is run multiple times, e.g. inside all_goals. It does not trigger when the simp call is inside a macro. The linter message contains a clickable hint to remove the simp argument.

• #8903 makes sure that the local instance cache calculation applies more reductions. In #2199 there was an issue where metavariables could prevent local variables from being considered as local instances. We use a slightly different approach that ensures that, for example, lets at the ends of telescopes do not cause similar problems. These reductions were already being calculated, so this does not require any additional work to be done.

• #8909 refactors the NoNatZeroDivisors to make sure it will work with the new Semiring support.

• #8910 adds the NoNatZeroDivisors instance for OfSemiring.Q α

• #8913 cleans up grind's internal order type classes, removing unnecessary duplication.

• #8914 modifies let and have term syntaxes to be consistent with each other. Adds configuration options; for example, have is equivalent to let +nondep, for nondependent lets. Other options include +usedOnly (for let_tmp), +zeta (for letI/haveI), and +postponeValue (for let_delayed). There is also let (eq := h) x := v; b for introducing h : x = v when elaborating b. The eq option works for pattern matching as well, for example let (eq := h) (x, y) := p; b.

• #8918 fixes the guard_msgs.diff default behavior so that the default specified in the option definition is actually used everywhere.

• #8921 implements support for (commutative) semirings in grind. It uses the Grothendieck completion to construct a (commutative) ring Lean.Grind.Ring.OfSemiring.Q α from a (commutative) semiring α. This construction is mostly useful for semirings that implement AddRightCancel α. Otherwise, the function toQ is not injective. Examples:

  example (x y : Nat) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
    磨
  
  

• #8935 将 +generalize 选项添加到 let 和 have 语法中。 例如，have +generalize n := a + b; body 替换所有实例 精化body 时，a + b 与 n 的预期类型相同。这个 可以比作 generalize策略的术语版本。一个可以 将此与 have +generalize (eq := h) n := a + b; body 中的 eq 结合起来 作为 generalize h : n = a + b 的类似物。

• #8937 更改生成的 below 的输出 Universe 非自反归纳类型的实现以匹配 #7639 中自反归纳类型的实现。

• #8940 引入了支持精化的反调引理 使用定义的混合归纳-共归纳谓词 least_fixpoint / greatest_fixpoint 构造。

• #8943 添加了辅助定理，用于标准化半环，但半环不 实施 AddRightCancel。

• #8953 实现对交换半环标准化的支持 不实现 AddRightCancel。示例：

  variable (R : Type u) [CommSemiring R]
  
  

• #8954 adds a procedure that efficiently transforms let expressions into have expressions (Meta.letToHave). This is exposed as the let_to_have tactic.

• #8955 fixes Lean.MVarId.deltaLocalDecl, which previously replaced the local definition with the target.

• #8957 adds configuration options to the let/have tactic syntaxes. For example, let (eq := h) x := v adds h : x = v to the local context. The configuration options are the same as those for the let/have term syntaxes.

• #8958 improves the case splitting strategy used in grind, and ensures grind also considers simple match-conditions for case-splitting. Example:

  example (x y : Nat)
      : 0 < 将 x, y 与
            | 0, 0 => 1
            | _, _ => x + y := by -- x 或 y 必须大于 0
    磨
  

• #8959 add instances showing that the Grothendieck (i.e. additive) envelope of a semiring is an ordered ring if the original semiring is ordered (and satisfies ExistsAddOfLE), and in this case the embedding is monotone.

• #8963 embeds a NatModule into its IntModule completion, which is injective when we have AddLeftCancel, and monotone when the modules are ordered. Also adds some (failing) grind test cases that can be verified once grind uses this embedding.

• #8964 adds @[expose] attributes to proof terms constructed by grind that need to be evaluated in the kernel.

• #8965 revises @[grind] annotations on Nat bitwise operations.

• #8968 adds the following features to simp:

  • A routine for simplifying have telescopes in a way that avoids quadratic complexity arising from locally nameless expression representations, like what #6220 did for letFun telescopes. Furthermore, simp converts letFuns into haves (nondependent lets), and we remove the #6220 routine since we are moving away from letFun encodings of nondependent lets.

  • A +letToHave configuration option (enabled by default) that converts lets into haves when possible, when -zeta is set. Previously Lean would need to do a full typecheck of the bodies of lets, but the letToHave procedure can skip checking some subexpressions, and it modifies the lets in an entire expression at once rather than one at a time.

  • A +zetaHave configuration option, to turn off zeta reduction of haves specifically. The motivation is that dependent lets can only be dsimped by let, so zeta reducing just the dependent lets is a reasonable way to make progress. The +zetaHave option is also added to the meta configuration.

  • When simp is zeta reducing, it now uses an algorithm that avoids complexity quadratic in the depth of the let telescope.

  • Additionally, the zeta reduction routines in simp, whnf, and isDefEq now all are consistent with how they apply the zeta, zetaHave, and zetaUnused configurations.

• #8971 fixes linter.simpUnusedSimpArgs to check the syntax kind, to not fire on simp calls behind macros. Fixes #8969

• #8973 refactors the juggling of universes in the linear noConfusionType construction: Instead of using PUnit.{…} → in the to get the branches of withCtorType to the same universe level, we use PULift.

• #8978 updates the solveMonoStep function used in the monotonicity tactic to check for definitional equality between the current goal and the monotonicity proof obtained from a recursive call. This ensures soundness by preventing incorrect applications when Lean.Order.PartialOrder instances differ—an issue that can arise with mutual blocks defined using the partial_fixpoint keyword, where different Lean.Order.CCPO structures may be involved.

• #8980 improves the consistency of error message formatting by rendering addenda of several existing error messages as labeled notes and hints.

• #8983 fixes a bug in congruence proof generation in grind for over-applied functions.

• #8986 improves the error messages produced by invalid projections and field notation. It also adds a hint to the "function expected" error message noting the argument to which the term is being applied, which can be helpful for debugging spurious "function expected" messages actually caused by syntax errors.

• #8991 adds some missing ToInt.X type class instances for grind.

• #8995 introduces a Hoare logic for monadic programs in Std.Do.Triple, and assorted tactics:

  • mspec for applying Hoare triple specifications

  • mvcgen to turn a Hoare triple proof obligation ⦃P⦄ prog ⦃Q⦄ into pure verification conditions (i.e., without any traces of Hoare triples or weakest preconditions reminiscent of prog). The resulting verification conditions in the stateful logic of Std.Do.SPred can be discharged manually with the tactics coming with its custom proof mode or with automation such as simp and grind.

• #8996 provides the remaining instances for the Lean.Grind.ToInt type classes.

• #9004 ensures that type-class synthesis failure errors in interpolated strings are displayed at the interpolant at which they occurred.

• #9005 changes the definition of Lean.Grind.ToInt.OfNat, introducing a wrap on the right-hand-side.

• #9008 implements the basic infrastructure for the generic ToInt support in cutsat.

• #9022 completes the generic toInt infrastructure for embedding terms implementing the ToInt type classes into Int.

• #9026 implements support for (non strict) ToInt inequalities in grind cutsat. grind cutsat can solve simple problems such as:

  example (a b c : Fin 11) : a ≤ b → b ≤ c → a ≤ c := by
    磨
  
  

• #9030 修复了新版本中一些与引导相关的问题 添加了 Std.Do 模块。更准确地说，

• #9035 将可接受的字符列表扩展到所有法语字符 以及其他一些人， 通过添加 Latin-1-Suplement 中的字符添加 Latin-Extended-A 统一码块。

• #9038 添加了 VC 生成器的测试用例并实现了一些小的 以及繁琐的修复以确保它们通过。

• #9041 使 mspec 通过 rfl 检测更可行的分配，而不是 生成 VC。

• #9044 调整实验模块系统，使 private module 中的默认可见性修饰符，引入 public 作为新的 改为修饰符。 public section 可用于恢复默认值 整个部分，尽管这更多的是为了方便逐步采用 新语义，例如在 Init（以及很快的 Std）中，它们 应由未来逐个 DECL 的可见性重新审查来取代。

• #9045 修复了 mvcgen 中的类型错误，并使其变得不那么自然 目标转换为合成的不透明目标，以便策略例如 trivial 可以 更容易地实例化它们。

• #9048 在 ToInt 中实现对严格不等式的支持 grind cutsat 中使用的适配器。例子：

  example (a b c : Fin 11) : c ≤ 9 → a ≤ b → b < c → a < c + 1 := by
    grind
  

• #9050 确保为每个 toInt a 断言 ToInt 边界 应用程序内置于 grind cutsat 中。

• #9051 在 grind 中实现对平等和不平等的支持 切萨特。我们仍然需要改进编码。示例：

  example (a b c : Fin 11) : a ≤ 2 → b ≤ 3 → c = a + b → c ≤ 5 := by
    grind
  
  

• #9057 introduces a simple variable-reordering heuristic for cutsat. It is needed by the ToInt adapter to support finite types such as UInt64. The current encoding into Int produces large coefficients, which can enlarge the search space when an unfavorable variable order is used. Example:

  example (a b c : UInt64) : a ≤ 2 → b ≤ 3 → c - a - b = 0 → c ≤ 5 := by
    磨
  

• #9059 adds helper theorems for normalizing coefficients in rings of unknown characteristic.

• #9062 implements support for equations <num> = 0 in rings and fields of unknown characteristic. Examples:

  example [Field α] (a : α) : (2 * a)⁻¹ = a⁻¹ / 2 := by grind
  
  

• #9065 改进了 cutsat 过程生成的反例 使用 ToInt 小工具时在 grind 中。

• #9067 添加 grind策略的文档字符串。

• #9069 实现对类型类 LawfulEqCmp 的支持。示例：

  example (a b c : Vector (List Nat) n)
      : b = c → a.compareLex (List.compareLex compare) b = o → o = .eq → a = c := by
    grind
  
  

• #9073 copies #9069 to handle ReflCmp the same way; we need to call this in propagateUp rather than propagateDown.

• #9074 uses the commutative ring module to normalize nonlinear polynomials in grind cutsat. Examples:

  example (a b : Nat) (h₁ : a + 1 ≠ a * b * a) (h₂ : a * a * b ≤ a + 1) : b * a^2 < a + 1 := by
    磨
  
  

• #9076 为 OfSemiring.toQ 添加一个解扩展器。这是一个辅助 grind 中的 ring 模块使用的函数，但我们希望减少 grind 生成的诊断信息混乱。例子：

  example [CommSemiring α] [AddRightCancel α] [IsCharP α 0] (x y : α)
      : x^2*y = 1 → x*y^2 = y → x + y = 2 → False := by
    grind
  

  产生

    [ring] Ring `Ring.OfSemiring.Q α` ▼
      [basis] Basis ▼
        [_] ↑x + ↑y + -2 = 0
        [_] ↑y + -1 = 0
  

• #9086 弃用 let_fun 语法，转而使用 have 并删除 来自 WHNF 和 simp 的 letFun 支持。

• #9087 从 letFun 中删除 irreducible 属性，该属性是 朝着删除特殊 letFun 支持的方向迈进； #9086 的一部分。

图书馆🔗

• #8003 为 Async 操作添加了新的单子接口。

• #8072 将 DNS 函数添加到标准库

• #8109 将系统信息函数添加到标准库

• #8178 为 sdiv 的 MSB 提供紧凑的公式。大部分的 PR 的工作涉及处理分裂的极端情况 溢出（例如 intMin / -1 = intMin）

• #8203 为无符号和有符号比较添加三分引理， 说明仅可能发生三种情况之一：x < y，x = y, or x > y（对于有符号和无符号比较）。我们使用 显式参数，以便用户可以编写 rcases slt_trichotomy x y 与 hlt |赫克 | hgt。

• #8205 添加了一个 simpl 引理，可简化 T 除法，其中分子 是 Nat 进入 E 分区：

  @[simp] theorem ofNat_tdiv_eq_ediv {a : Nat} {b : Int} : (a : Int).tdiv b = a / b :=
     tdiv_eq_ediv_of_nonneg (by simp)
  

• #8210 向树图添加类似于现有的等价关系 一个用于哈希映射。为了最终得到许多同余引理 用于在扩展树图上定义函数，几乎所有 其余的树图函数也已给出引理来将它们联系起来 列出函数，尽管这些函数目前不用于证明引理 除了同余引理之外。

• #8253 添加了证明所需的 toInt_smod 和辅助引理 （msb_intMin_umod_neg_of_msb_true， msb_neg_umod_neg_of_msb_true_of_msb_true、toInt_dvd_toInt_iff、 toInt_dvd_toInt_iff_of_msb_true_msb_false, toInt_dvd_toInt_iff_of_msb_false_msb_true, neg_toInt_neg_umod_eq_of_msb_true_msb_true、toNat_pos_of_ne_zero、 toInt_umod_neg_add、toInt_sub_neg_umod 和 BitVec.[lt_of_msb_false_of_msb_true, msb_umod_of_msb_false_of_ne_zero, neg_toInt_neg])

• #8420 提供迭代器组合器 drop，可转换任何 迭代器进入删除第一个 n 元素的迭代器。

• #8534 修复了 Windows 上的 IO.FS.realPath，以将符号链接引入 帐户。

• #8545 提供了推理“等效”迭代器的方法。 简单来说，如果两个迭代器的行为相同，那么它们是等价的 只要消费者不反思自己的状态。

• #8546 添加新的 BitVec.clz 操作和相应的 clz 电路连接到 bv_decide，允许对计数前导零进行位爆破 操作。 AIG 电路与位数呈线性关系 原始表达，使位爆破变得方便。重写。 clz 在许多编译器内在函数中很常见（请参阅 此处) 和架构（参见 此处)。

• #8573 避免了 removeDirAll 可能出现的意外行为 通过符号链接删除并添加新功能 IO.FS.symlinkMetadata。

• #8585 使引理 BitVec.extractLsb'_append_eq_ite 更可用 通过更频繁地使用“简单情况”，并使用这种简化来 使BitVec.extractLsb'_append_eq_of_add_lt更强，将其重命名为 BitVec.extractLsb'_append_eq_of_add_le。

• #8587 调整研磨注释 Std.HashMap.map_fst_toList_eq_keys 和变体，因此 grind 可以推理 m.keys 和 m.toList 之间双向。

• #8590 将 @[grind] 添加到 getElem?_pos 及其变体。

• #8615 提供特殊的空迭代器类型。虽然它的行为 可以用列表迭代器（例如）来模拟，具有特殊的 type 的优点是更容易为编译器优化。

• #8620 删除 NatCast (Fin n) 全局实例（直接 实例，以及通过 Lean.Grind.Semiring 的间接实例），因为 instance causes x < n (for x : Fin k, n : Nat) to be 详细说明为 x < ↑n 而不是 ↑x < n，这是不可取的。注意事项 然而，在 Mathlib 中，这种情况无论如何都会发生！

• #8629 替换特殊的、更优化的 IteratorLoop 实例， 未提供合法性证明，已核实违约 实施。循环/收集实现的专门化 优先级较低，但所有迭代器都具有合法性实例 对于验证很重要。

• #8631 概括 Std.Sat.AIG. relabel(Nat)_unsat_iff 以允许 AIG 类型为空。我们通过证明在 当 α 为空时，环境并不重要，因为所有 环境 α → Bool 是同构的。

• #8640 将 BitVec.setWidth'_eq 添加到 bv_normalize，使得 bv_decide 可以减少它并解决涉及 setWidth'_eq 的引理

• #8669 使 unsafeBaseIO noinline。新的编译器更擅长 优化 Result 类类型，这会导致最终操作 要删除的 unsafeBaseIO 块，因为 unsafeBaseIO 是 丢弃状态。

• #8678 使 isSome_finIdxOf? 和 isNone_finIdxOf? 的 LHS 更 一般。

• #8703 更正了 DropWhile 中的 IteratorLoop 实例，该实例 先前为任意迭代器类型触发。

• #8719 添加研磨注释 列表/数组/Vector.eraseP/erase/eraseIdx。它还补充了一些缺失的 引理。

• #8721 添加类型 Std.ExtDTreeMap、Std.ExtTreeMap 和 Std.ExtTreeSet 扩展树图和集合。这些都是非常 在构造上与现有的扩展哈希映射类似，其中一个 例外：扩展树映射和集合提供来自 常规树图和集合。这是可能的，因为与哈希相比 地图、树图始终是有序的。

• #8734 添加缺失的实例

  instance decidableExistsFin (P : Fin n → Prop) [DecidablePred P] : Decidable (∃ i, P i)
  

• #8740 引入了关联规则和保存 (umul, smul, uadd，sadd）溢出标志。

• #8741 添加注释 List/Array/Vector.find?/findSome?/idxOf?/findIdx?。

• #8742 修复了单引号字符 Char.ofNat 39 的错误 将详细说明为 '''，如果粘贴回，则会导致解析错误 到源代码。

• #8745 按顺序将状态谓词 SPred 的逻辑添加到 Std.Do 支持关于一元程序的推理。它配备了专用的 校样模式策略可通过导入访问 Std.Tactic.Do。

• #8747 添加 `List/Array/Vector.finRange` 的研磨注释 定理。

• #8748 添加 Array/Vector.mapIdx 和 mapFinIdx 的研磨注释 定理。

• #8749 为 List/Array/Vector.ofFn 定理添加研磨注释 额外的 List.Impl 查找操作。

• #8750 添加研磨注释 List/Array/Vector.zipWith/zipWithAll/unzip 功能。

• #8765 为 List.Perm 添加研磨注释；涉及修订 还对 List.countP/count 进行研磨注释。

• #8768 引入了 ForIn' 实例和 size 函数 以最小的方式迭代器。 ForIn' 实例未标记为 一个实例，因为尚不清楚 Membership 关系是什么 足够有用。 ForIn' 实例作为 def 存在，并且 引入 ForIn 实例，可以提供更多 专门的 ForIn' 实例，具有良好的 Membership 关系，用于 各种类型的迭代器。 size 函数还没有引理。

• #8784 引入了多态范围，与 现有的Std.Range仅支持自然数。

• #8805 继续为 List/Array/Vector 添加 grind 注释 引理。

• #8808 添加缺失的 le_of_add_left_le {n m k : Nat} (h : k + n ≤ m) : n ≤ m and le_add_left_of_le {n m k : Nat} (h : n ≤ m) : n ≤ k + 米。

• #8811 添加定理 BitVec.(toNat, toInt, toFin)_shiftLeftZeroExtend，完成 API BitVec.shiftLeftZeroExtend。

• #8826 更正了 Lean.Grind.NatModule 的定义，该定义不是 以前有用。

• #8827 将 BitVec.getLsb' 重命名为 BitVec.getLsb，现在更旧了 占用该名称的已弃用定义已被删除。 （同样 适用于 BitVec.getMsb'。）

• #8829 避免导入所有 BitVec.Lemmas 和 BitVec.BitBlast 进入 UInt.Lemmas。 （它们仍然导入到 SInt.Lemmas 中；这 似乎更难避免。）

• #8830 重新排列 Init.Grind 下的文件，移出实例 Init.GrindInstances 中的具体代数类型。

• #8849 为 Sum 添加 grind 注释。

• #8850 为 Prod 添加 grind 注释。

• #8851 添加 Function.curry/uncurry 的研磨注释。

• #8852 添加 Nat.testBit 和按位运算的研磨注释 在 Nat 上。

• #8853 添加与 Nat.fold/foldRev/any/all 和 Fin.foldl/foldr/foldlM/foldrM 上对应的操作 List.finRange。

• #8877 添加研磨注释 List/Array/Vector.attach/attachWith/pmap。

• #8878 为列表/数组/向量一元函数添加研磨注释。

• #8886 添加并行的 IO.FS.Stream.readToEnd IO.FS.Handle.readToEnd 及其上游定义（即 readBinToEndInto 和 readBinToEnd)。它还删除了不必要的 partial 来自 IO.FS.Handle.readBinToEnd。

• #8887 将 IO.FS.lines 概括为 IO.FS.Handle.lines 并添加 用于流的并行 IO.FS.Stream.lines。

• #8897 简化了一些 simp 调用。

• #8905 使用来自 https://github.com/leanprover/lean4/pull/8901 清理简单 论据。

• #8920 使用 #8901 中的 linter 来清理更多 simp 参数， 完成#8905。

• #8928 将状态谓词 SPred 的逻辑添加到 Std.Do，以便 支持关于一元程序的推理。它配备了专用的 校样模式策略可通过导入访问 标准策略.Do。

• #8941 添加 BitVec.(getElem, getLsbD, getMsbD)_(smod, sdiv, srem) 定理来完成 sdiv、srem、smod 的 API。尽管 rhs 并不是特别简洁（很难找到它的含义） 意思是“有符号除法/模结果的第n位 操作”），这些引理阻止了 unfold 操作的需要。

• #8947 以最基本的形式引入多态切片。他们 带有类似于新范围符号的符号。 Subarray 是 现在也是一个切片并且可以生成一个迭代器。其目的是 将 Subarray 的更多操作迁移到 Slice 包装类型 也使它们可用于其他类型的切片。

• #8950 添加 BitVec.toFin_(sdiv, smod, srem) 和 BitVec.toNat_srem。 toFin_* 引理的 rhs 的策略是考虑什么 相应的 toNat_* 定理使 toFin 更接近 操作数。对于 BitVec.toNat_srem 的 rhs 我使用了相同的 策略为 BitVec.toNat_smod。

• #8967 都为 BitVec 添加初始 @[grind] 注释，并使用 grind 从 BitVec/Lemmas 中删除许多校样。

• #8974 添加 BitVec.msb_(smod, srem)。

• #8977 添加通用 MonadLiftT Id m 实例。我们不实施 MonadLift Id m 实例，因为它会减慢实例解析速度 因为它会创建更多非规范实例。这个改变 使得迭代纯迭代器成为可能，例如[1, 2, 3].iter，在任意单子中。

• #8992 添加了 PULift，这是 ULift 和 PLift 的更通用形式， 包含两者。

• #8995 为单子程序引入了霍尔逻辑 Std.Do.Triple, and assorted策略:

  • mspec 适用于霍尔三重规格

  • mvcgen 将霍尔三重证明义务 ⦃P⦄ prog ⦃Q⦄ 转变为 纯验证条件（即，没有任何霍尔三元组的痕迹 或最弱的先决条件，例如 prog）。由此产生的 Std.Do.SPred 状态逻辑中的验证条件可以是 使用具有自定义校样模式的策略手动放电 或使用 simp 和 grind 等自动化系统。

• #9027 提供一个迭代器组合器，用于提升发出的值 通过 ULift 进入更高的 宇宙层级。然后使用这个组合器 使子数组迭代器具有全域多态性。此前，他们 仅适用于 Subarray α（如果是 α : Type）。

• #9030 修复了新版本中一些与引导相关的问题 添加了 Std.Do 模块。更准确地说，

• #9038 添加了 VC 生成器的测试用例并实现了一些小的 以及繁琐的修复以确保它们通过。

• #9049 证明默认的 toList、toListRev 和 toArray 切片上的函数可以用切片迭代器来描述。 依赖 uLift 和 attachWith 迭代器的新引理 组合器，给出了所述功能的更具体描述 Subarray。

• #9054 更正了 TreeMap/HashMap 研磨中的一些不一致之处 注释，适用于 isSome_get?_eq_contains 和 empty_eq_emptyc。

• #9055 将 Array/Vector.extract_push 重命名为 extract_push_of_le，并且 将引理替换为没有附加条件的引理。

• #9058 为切片提供 ToStream 实例，以便它们可以 以 for i in xs, j in ys do 表示法使用。

• #9075 为 ByteArray 和 FloatArray 添加 BEq 实例（也是 ByteArray 的 DecidableEq 实例）。

编译器🔗

• #8594 从中删除了 strictOr/strictAnd 的错误优化 旧的编译器，并删除不正确的测试。为了做到 这些优化正确，需要非终止分析。 可以说，表达这些优化的正确方法是公开 将 strictOr/strictAnd 实现到非终止感知阶段 编译器的，然后让它们遵循更一般的 转变。

• #8595 将新编译器的调用包装在 withoutExporting 中。 这对于旧的编译器来说是不必要的，因为它使用更直接的 访问内核环境。

• #8602 添加了对 Eq.recOn 的新编译器的支持（即 旧编译器支持但缺少测试）。

• #8604 在新版本中添加了对 compiler.extract_closed 选项的支持 编译器，因为这是由 unsafeBaseIO 的定义使用的。我们会 一旦我们切换到新的编译器并重新考虑它，就重新审视这一点 与 IO 的关系。

• #8614 在新编译器中实现 toNat 的常量折叠， 这提高了与旧编译器的奇偶性。

• #8616 在新编译器中添加了 Nat.pow 的常量折叠， 遵循与旧编译器相同的限制。

• #8618 为 Nat.nextPowerOfTwo 实现 LCNF 常量折叠。

• #8634 使 hasTrivialStructure? 对于以下类型返回 false 构造函数具有被删除的类型，例如如果他们建造一个 Prop。

• #8636 添加一个名为 lean_setup_libuv 的函数，用于初始化 所需的 LIBUV 组件。它需要在以下范围之外 lean_initialize_runtime_module，因为它需要 argv 和 argc 才能正常工作。

• #8647 提高了新编译器 noncomputable 的精度 检查预测。没有包含测试，因为虽然这是 从 Mathlib 减少，旧编译器不能正确处理 减少测试用例。我不太清楚检查是否通过 出于正确的原因使用旧编译器。将添加一个测试 新编译器的分支。

• #8675 提高了新编译器不可计算的精度 检查，特别是关于 noncomputable defs 的不相关使用 应用程序。

• #8681 向 LCNF simp pass 添加优化，其中 cases 构造的判别式只有在具有 非默认替代方案。

• #8683 向 LCNF simp pass 添加优化，其中 仅当有任何参数时，单个 alt 情况的判别才被标记为已使用 被使用。

• #8709 处理 toMonoType 中已删除类型的常量。这是很多 为此编写测试用例比您想象的更难，因为大多数 对此类类型的引用之前已替换为 lcErased。

• #8712 将擦除类型的 let decls 优化为擦除值。 专业化可以创建产生 Prop 的局部函数，并且 把它们留在身边是没有意义的。

• #8716 使已擦除术语的任何类型应用程序都被擦除。这个 在 Lean 的实现中出现的情况比人们预期的要多一些 本身。

• #8717 使用 fvar 替换机制来替换已擦除的代码。 这并不完全令人满意，因为 LCNF 的 .return 不支持 一个通用的 Arg （它有一个 .erased 构造函数），它只支持 FVarId。这与 IR .ret 形成对比，后者确实支持 一般Arg。

• #8729 将 LCNF 的 FVarSubst 更改为使用 Arg 而不是 Expr。这个 强制执行符合要求的替换要求 在 Arg 上。

• #8752 修复了 extendJoinPointContext 通行证可以解除的问题 连接包含到顶层的投影的点，作为 cases 构造对相同基值的其他投影的匹配。 这可以防止 structProjCases 通道同时投影两者， 延长父值的生命周期并打破线性 运行时。

• #8754 更改了新版本中计算字段的实现 编译器，它应该能够实现更多优化（并删除 toLCNF 中的可疑黑客仅适合启动）。我们 将 casesOn 转换为 cases，就像我们对其他归纳类型所做的那样，所有 构造函数在基础后期被其实际实现所取代 相，然后重写 cases 表达式以使用实数 toMono 中的构造函数。

• #8758 为 LCNF 的 hasTrivialStructure? 函数添加缓存 类型。这是新编译器中最热门的小函数之一， 所以添加缓存很有意义。

• #8764 更改 LCNF 传递管道，因此检查不再由 每次通过后默认，仅在 init、saveBase、toMono 和 saveMono。这是编译时间的改进，这些的实用性 在决定不再尝试之后，检查有所减少 在整个编译过程中保留类型。他们并没有成为一个重要的 在新编译器的开发过程中发现问题的方法。

• #8802 修复了 floatLetIn 中的一个错误，其中如果一个 decl（例如，一个 join 点）被浮动到一个案例臂中，并且它使用另一个 decl（例如另一个 连接点）在该臂中没有任何其他现有用途，那么 尽管这是完美的，但第二个 decl 并未浮动 合法的。这导致了人为阵列线性问题 Lean.Elab.Tactic.BVDecide.LRAT.trim.useAnalysis。

• #8816 在 LCNF simp 中为 Char.ofNat 添加常量折叠。这个 隐式依赖于 Char 作为 UInt32 的表示 而不是制作一个单独的 .char 文字类型，这似乎是合理的 Char 通过 toMono 中的琐碎结构优化而被擦除。

• #8822 在 toIR 中添加构造函数信息的缓存。这是要求 所有构造函数、投影和案例替代方案，所以这是有道理的 缓存。

• #8825 改进了归纳类型构造函数的 IR 生成， 由标量表示。令人惊讶的是，这不是必需的 正确性，因为拳击传球会修复它。额外的 unbox 当编译为本机代码时，它插入的操作应该不重要， 因为对于 C 编译器来说优化是微不足道的，但它确实很重要 对于口译员来说。

• #8831 缓存 lowerEnumToScalarType 的结果，以供使用 主要从事 LCNF 到 IR 的转换。

• #8885 删除了围绕未实现的 C++11 功能的旧解决方法 在线程终结中。

• #8923 为 Thunk 和 Task 实现 casesOn。由于这些是 内置类型，需要在 toMono 中进行特殊处理。

• #8952 修复了 never_extract 属性的处理 编译器的 CSE 通过。有一场有趣的辩论 编译器到底应该如何努力避免重复任何内容 传递使用 never_extract，但这是最简单的形式 并大致匹配旧编译器中的检查（尽管由于 两个编译器中对本地函数 decl 的不同处理， 结果可能略有不同）。

• #8956 更改 toLCNF 以停止缓存表达式的翻译 当看到标记为 never_extract 的表达式时。这更 粒度比需要的要粗，但是很难做到任何 更好，因为新编译器的 Expr 缓存是基于结构的 身份（而不是旧编译器的指针身份）。

• #9003 实现新版本中 main 类型的有效性检查 编译器。由于没有对此进行测试，因此它没有受到关注。

漂亮的印刷🔗

• #7954 改进了 pp.oneline，现在它会在以下情况下保留标签： 将格式化语法截断为一行。请注意，[...] Continuation 尚不具备任何功能来支持查看 未截断的语法。关闭#3681。

• #8617 修复了 (1) 在以下情况下私有名称未被解析的问题： 它们打印得很漂亮，(2) pp.universes 模式名称中的问题 允许隐藏本地名称，(3) match 中的问题 阴影局部变量的模式常量不会使用 _root_，并且 (4) 策略可能会出现错误的“尝试这个”问题 pp.fullNames 已设置。添加更多名称详细测试 未解决。

• #8626 关闭 #3791，确保语法格式化程序插入 前导和尾随文本中注释前后的空格 语法以避免注释注释掉任何以下语法，并 避免注释的词法语法被解释为是 另一种语法。如果文本在任何内容之前或之后包含换行符 注释，它们被格式化为硬换行符而不是软换行符。 例如，-- 注释后将有一个硬换行符。注意： 生成带有注释的语法的元程序应确保包括 -- 注释末尾的换行符。

文档🔗

• #8934 添加了对一些有关不可计算性的错误的解释， 冗余匹配替代项和无效的归纳声明。

• #8990 为 grind 的内部代数添加缺失的文档字符串 类型类，包含在参考手册中。

• #8998 使与 Format 和 Repr 相关的文档字符串具有 一致的格式和风格，并添加缺失的文档字符串。

服务器🔗

• #8105 添加了对服务器端 RpcRef 重用的支持并修复了错误 当文件仍然存在时，InfoView 中的跟踪节点将关闭 正在处理中。

• #8511 实现签名帮助支持。当输入函数时 应用程序中，支持签名帮助的编辑器现在将显示 指定当前（剩余）函数类型的弹出窗口。这个 无需在键入时记住函数签名 功能应用程序，或者必须在悬停之间不断循环 通过函数标识符并键入应用程序。在 VS 代码中， 可以使用 Ctrl+Shift+Space 手动触发签名帮助。

• #8654 添加了对新模块层次结构组件的服务器端支持 VS Code 可用于导航模块的导入树 以及模块的导入树。具体来说，它实现了新的 请求 $/lean/prepareModuleHierarchy， $/lean/moduleHierarchy/imports 和 $/lean/moduleHierarchy/importedBy。这些请求不被支持 标准 LSP。同伴公关 leanprover/vscode-lean4#620。

• #8699 添加了对服务器新模块设置过程的支持 更改 lake setup-file 的使用方式。

• #8868 确保代码操作不必等待完整文件 详细说明。这个回归是在 #7665 中意外引入的。

• #9019 修复了语义突出显示仅突出显示的错误 以字母数字字符开头的关键字。现在，它使用 Lean.isIdFirst。

Lake🔗

• #7738 使内置构面的记忆可通过 构面配置上的 memoize 选项。内置的方面是 本质上别名（例如，default、o）已被记忆 禁用。

• #8447 在 Lake 版本的 Lean 模块中使用 lean --setup，并且 添加了对模块生成的新 .olean 工件的 Lake 支持 系统。

• #8613 将 Lake 版本语法（更改为 5.0.0-src+<commit>）更改为 确保它是格式良好的 SemVer，

• #8656 在 Lake 数学模板中启用自动隐式。这解决了 新用户有时会设置新的数学项目的问题 形式化，然后很快意识到没有任何代码示例 我们的官方书籍和文档在其使用自动隐式工作 项目。随着[镶嵌提示]的引入 自动隐式](https://github.com/leanprover/lean4/pull/6768)，我们 认为自动隐式用户体验足够可用，可以 在数学模板中默认启用。 值得注意的是，此更改不会影响 Mathlib 本身，它将继续 禁用自动隐式。

• #8701 从 Lake 导出 Lean 命名空间中的 LeanOption 命名空间。 LeanOption 在#8447 中从 Lean 移至 Lake，其中 如果没有这个，可能会导致不必要的损坏。

• #8736 部分恢复 #8024，它引入了重要的 Lake 构建期间的性能回归。一旦发现原因并 已修复，将发布类似的 PR 来恢复此问题。

• #8846 重新引入了 lean --setup 集成到 Lake 中的基础知识 没有仍在进行性能的模块计算 在#8787 中进行调试。

• #8866 将 lake init 和 lake new 的 math 模板升级为 配置新项目以满足严格的 Mathlib 维护 标准。与以前的版本相比（现在可用 lake new ... math-lax)，这会自动提供：

  • 与 Mathlib 匹配的严格 linting 选项。

  • GitHub 自动升级到较新的 Lean 和 Mathlib 的工作流程 发布。

  • 用于工具链升级的自动发布标记。

  • API 文档生成者 doc-gen4 并托管于 github.io。

  • 自述文件包含一些 GitHub 特定说明。

• #8922 引入了 Lake 的本地工件缓存。启用后，Lake 将在不同实例之间共享构建工件（构建文件） 使用输入和内容寻址缓存的同一包。

• #8981 删除了 Lake 对 lean -R 和 moduleNameOfFileName 的使用 将模块名称传递给 Lean。对于工作区名称，它现在依赖于 直接通过lean --setup传递模块名称。对于 非工作区模块传递到 lake lean 或 lake setup-file，它 使用固定模块名称 _unknown。

• #9068 修复了本地 Lake 工件缓存的一些错误并进行了清理 周围的API。它还增加了选择加入缓存的能力 没有使用 enableArtifactCache 设置的软件包 LAKE_ARTIFACT_CACHE 环境变量。

• #9081 修复了 Lake 中作业监视器位于 顶级构建（例如，mathlib/Mathlib:default）而不是报告 模块构建进度。

• #9101 修复了 #9081 引入的源文件被删除的错误 从模块输入跟踪中删除了一些条目 模块作业日志。

其他🔗

• #8702 增强了 PR 发布工作流程，以创建短格式和 SHA 后缀的发布标签。创建预发布-{PR_NUMBER} 和 pr-release-{PR_NUMBER}-{SHORT_SHA} 标签，生成单独的版本 两种格式，添加单独的 GitHub 状态检查和更新 Batteries/Mathlib 测试分支使用 SHA 后缀标签进行精确测试 提交可追溯性。

• #8710 将 softprops/action-gh-release 的精确散列固定到

• #9033 添加了类似 Mathlib 的测试和反馈系统 参考手册。 Lean PR 将收到反映状态的评论 PR 相关的语言参考。

• #9092 进一步更新发布自动化。每个存储库的更新 脚本 script/release_steps.py 现在实际执行测试， 而不是输出脚本供发布管理器逐行运行 线。它已经在 v4.21.0 上进行了测试（即稳定的简单情况） 发布），今晚我们将在 v4.22.0-rc1 上调试其行为。