Language features, tactics, and metaprograms

• split tactic:

  • #4401 improves the strategy split uses to generalize discriminants of matches and adds trace.split.failure trace class for diagnosing issues.

• rw tactic:

  • #4385 prevents the tactic from claiming pre-existing goals are new subgoals.
  • dac1da adds configuration for ordering new goals, like for apply.

• simp tactic:

  • #4430 adds dsimprocs for if expressions (ite and dite).
  • #4434 improves heuristics for unfolding. Equational lemmas now have priorities where more-specific equationals lemmas are tried first before a possible catch-all.
  • #4481 fixes an issue where function-valued OfNat numeric literals would become denormalized.
  • #4467 fixes an issue where dsimp theorems might not apply to literals.
  • #4484 fixes the source position for the warning for deprecated simp arguments.
  • #4258 adds docstrings for dsimp configuration.
  • #4567 improves the accuracy of used simp lemmas reported by simp?.
  • fb9727 adds (but does not implement) the simp configuration option implicitDefEqProofs, which will enable including rfl-theorems in proof terms.

• omega tactic:

  • #4360 makes the tactic generate error messages lazily, improving its performance when used in tactic combinators.

• bv_omega tactic:

  • #4579 works around changes to the definition of Fin.sub in this release.

• #4490 sets up groundwork for a tactic index in generated documentation, as there was in Lean 3. See PR description for details.

• Commands

  • #4370 makes the variable command fully elaborate binders during validation, fixing an issue where some errors would be reported only at the next declaration.
  • #4408 fixes a discrepency in universe parameter order between theorem and def declarations.
  • #4493 and #4482 fix a discrepancy in the elaborators for theorem, def, and example, making Prop-valued examples and other definition commands elaborate like theorems.
  • 8f023b, 3c4d6b and 0783d0 change the #reduce command to be able to control what gets reduced. For example, #reduce (proofs := true) (types := false) e reduces both proofs and types in the expression e. By default, neither proofs or types are reduced.
  • #4489 fixes an elaboration bug in #check_tactic.
  • #4505 adds support for open _root_.<namespace>.

• Options

  • #4576 adds the debug.byAsSorry option. Setting set_option debug.byAsSorry true causes all by ... terms to elaborate as sorry.
  • 7b56eb and d8e719 add the debug.skipKernelTC option. Setting set_option debug.skipKernelTC true turns off kernel typechecking. This is meant for temporarily working around kernel performance issues, and it compromises soundness since buggy tactics may produce invalid proofs, which will not be caught if this option is set to true.

• #4301 adds a linter to flag situations where a local variable's name is one of the argumentless constructors of its type. This can arise when a user either doesn't open a namespace or doesn't add a dot or leading qualifier, as in the following:

  inductive Tree (α : Type) where
    | leaf
    | branch (left : Tree α) (val : α) (right : Tree α)
  
  def depth : Tree α → Nat
    | leaf => 0
  

  With this linter, the leaf pattern is highlighted as a local variable whose name overlaps with the constructor Tree.leaf.

  The linter can be disabled with set_option linter.constructorNameAsVariable false.

  Additionally, the error message that occurs when a name in a pattern that takes arguments isn't valid now suggests similar names that would be valid. This means that the following definition:

  def length (list : List α) : Nat :=
    match list with
    | nil => 0
    | cons x xs => length xs + 1
  

  now results in the following warning:

  warning: Local variable 'nil' resembles constructor 'List.nil' - write '.nil' (with a dot) or 'List.nil' to use the constructor.
  note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
  

  and error:

  invalid pattern, constructor or constant marked with '[match_pattern]' expected
  
  Suggestion: 'List.cons' is similar
  

• Metaprogramming

  • #4454 adds public Name.isInternalDetail function for filtering declarations using naming conventions for internal names.

• Other fixes or improvements

  • #4416 sorts the ouput of #print axioms for determinism.
  • #4528 fixes error message range for the cdot focusing tactic.

Language server, widgets, and IDE extensions

• #4443 makes the watchdog be more resilient against badly behaving clients.

Pretty printing

• #4433 restores fallback pretty printers when context is not available, and documents addMessageContext.
• #4556 introduces pp.maxSteps option and sets the default value of pp.deepTerms to false. Together, these keep excessively large or deep terms from overwhelming the Infoview.

Library

• #4560 splits GetElem class into GetElem and GetElem?. This enables removing Decidable instance arguments from GetElem.getElem? and GetElem.getElem!, improving their rewritability. See the docstrings for these classes for more information.
• Array
  • #4389 makes Array.toArrayAux_eq be a simp lemma.
  • #4399 improves robustness of the proof for Array.reverse_data.
• List
  • #4469 and #4475 improve the organization of the List API.
  • #4470 improves the List.set and List.concat API.
  • #4472 upstreams lemmas about List.filter from Batteries.
  • #4473 adjusts @[simp] attributes.
  • #4488 makes List.getElem?_eq_getElem be a simp lemma.
  • #4487 adds missing List.replicate API.
  • #4521 adds lemmas about List.map.
  • #4500 changes List.length_cons to use as.length + 1 instead of as.length.succ.
  • #4524 fixes the statement of List.filter_congr.
  • #4525 changes binder explicitness in List.bind_map.
  • #4550 adds maximum?_eq_some_iff' and minimum?_eq_some_iff?.
• #4400 switches the normal forms for indexing List and Array to xs[n] and xs[n]?.
• HashMap
  • #4372 fixes linearity in HashMap.insert and HashMap.erase, leading to a 40% speedup in a replace-heavy workload.
• Option
  • #4403 generalizes type of Option.forM from Unit to PUnit.
  • #4504 remove simp attribute from Option.elim and instead adds it to individal reduction lemmas, making unfolding less aggressive.
• Nat
  • #4242 adds missing theorems for n + 1 and n - 1 normal forms.
  • #4486 makes Nat.min_assoc be a simp lemma.
  • #4522 moves @[simp] from Nat.pred_le to Nat.sub_one_le.
  • #4532 changes various Nat.succ n to n + 1.
• Int
  • #3850 adds complete div/mod simprocs for Int.
• String/Char
  • #4357 make the byte size interface be Nat-valued with functions Char.utf8Size and String.utf8ByteSize.
  • #4438 upstreams Char.ext from Batteries and adds some Char documentation to the manual.
• Fin
  • #4421 adjusts Fin.sub to be more performant in definitional equality checks.
• Prod
  • #4526 adds missing Prod.map lemmas.
  • #4533 fixes binder explicitness in lemmas.
• BitVec
  • #4428 adds missing simproc for BitVec equality.
  • #4417 adds BitVec.twoPow and lemmas, toward bitblasting multiplication for LeanSAT.
• Std library
  • #4499 introduces Std, a library situated between Init and Lean, providing functionality not in the prelude both to Lean's implementation and to external users.
• Other fixes or improvements
  • #3056 standardizes on using (· == a) over (a == ·).
  • #4502 fixes errors reported by running the library through the the Batteries linters.

Lean internals

• #4391 makes getBitVecValue? recognize BitVec.ofNatLt.
• #4410 adjusts instantiateMVars algorithm to zeta reduce let expressions while beta reducing instantiated metavariables.
• #4420 fixes occurs check for metavariable assignments to also take metavariable types into account.
• #4425 fixes forEachModuleInDir to iterate over each Lean file exactly once.
• #3886 adds support to build Lean core oleans using Lake.
• Defeq and WHNF algorithms
  • #4387 improves performance of isDefEq by eta reducing lambda-abstracted terms during metavariable assignments, since these are beta reduced during metavariable instantiation anyway.
  • #4388 removes redundant code in isDefEqQuickOther.
• Typeclass inference
  • #4530 fixes handling of metavariables when caching results at synthInstance?.
• Elaboration
  • #4426 makes feature where the "don't know how to synthesize implicit argument" error reports the name of the argument more reliable.
  • #4497 fixes a name resolution bug for generalized field notation (dot notation).
  • #4536 blocks the implicit lambda feature for (e :) notation.
  • #4562 makes it be an error for there to be two functions with the same name in a where/let rec block.
• Recursion principles
  • #4549 refactors findRecArg, extracting withRecArgInfo. Errors are now reported in parameter order rather than the order they are tried (non-indices are tried first). For every argument, it will say why it wasn't tried, even if the reason is obvious (e.g. a fixed prefix or is Prop-typed, etc.).
• Porting core C++ to Lean
  • #4474 takes a step to refactor constructions toward a future port to Lean.
  • #4498 ports mk_definition_inferring_unsafe to Lean.
  • #4516 ports recOn construction to Lean.
  • #4517, #4653, and #4651 port below and brecOn construction to Lean.
• Documentation
  • #4501 adds a more-detailed docstring for PersistentEnvExtension.
• Other fixes or improvements
  • #4382 removes @[inline] attribute from NameMap.find?, which caused respecialization at each call site.
  • 5f9ded improves output of trace.Elab.snapshotTree.
  • #4424 removes "you might need to open '{dir}' in your editor" message that is now handled by Lake and the VS Code extension.
  • #4451 improves the performance of CollectMVars and FindMVar.
  • #4479 adds missing DecidableEq and Repr instances for intermediate structures used by the BitVec and Fin simprocs.
  • #4492 adds tests for a previous isDefEq issue.
  • 9096d6 removes PersistentHashMap.size.
  • #4508 fixes @[implemented_by] for functions defined by well-founded recursion.
  • #4509 adds additional tests for apply? tactic.
  • d6eab3 fixes a benchmark.
  • #4563 adds a workaround for a bug in IndPredBelow.mkBelowMatcher.
• Cleanup: #4380, #4431, #4494, e8f768, de2690, d3a756, #4404, #4537.

Compiler, runtime, and FFI

• d85d3d fixes criterion for tail-calls in ownership calculation.
• #3963 adds validation of UTF-8 at the C++-to-Lean boundary in the runtime.
• #4512 fixes missing unboxing in interpreter when loading initialized value.
• #4477 exposes the compiler flags for the bundled C compiler (clang).

Lake

• #4384 deprecates inputFile and replaces it with inputBinFile and inputTextFile. Unlike inputBinFile (and inputFile), inputTextFile normalizes line endings, which helps ensure text file traces are platform-independent.

• #4371 simplifies dependency resolution code.

• #4439 touches up the Lake configuration DSL and makes other improvements: string literals can now be used instead of identifiers for names, avoids using French quotes in lake new and lake init templates, changes the exe template to use Main for the main module, improves the math template error if lean-toolchain fails to download, and downgrades unknown configuration fields from an error to a warning to improve cross-version compatibility.

• #4496 tweaks require syntax and updates docs. Now require in TOML for a package name such as doc-gen4 does not need French quotes.

• #4485 fixes a bug where package versions in indirect dependencies would take precedence over direct dependencies.

• #4478 fixes a bug where Lake incorrectly included the module dynamic library in a platform-independent trace.

• #4529 fixes some issues with bad import errors. A bad import in an executable no longer prevents the executable's root module from being built. This also fixes a problem where the location of a transitive bad import would not been shown. The root module of the executable now respects nativeFacets.

• #4564 fixes a bug where non-identifier script names could not be entered on the CLI without French quotes.

• #4566 addresses a few issues with precompiled libraries.

  • Fixes a bug where Lake would always precompile the package of a module.
  • If a module is precompiled, it now precompiles its imports. Previously, it would only do this if imported.

• #4495, #4692, #4849 add a new type of require that fetches package metadata from a registry API endpoint (e.g. Reservoir) and then clones a Git package using the information provided. To require such a dependency, the new syntax is:

  require <scope> / <pkg-name> [@ git <rev>]
  -- Examples:
  require "leanprover" / "doc-gen4"
  require "leanprover-community" / "proofwidgets" @ git "v0.0.39"
  

  Or in TOML:

  [[require]]
  name = "<pkg-name>"
  scope = "<scope>"
  rev = "<rev>"
  

  Unlike with Git dependencies, Lake can make use of the richer information provided by the registry to determine the default branch of the package. This means for repositories of packages like doc-gen4 which have a default branch that is not master, Lake will now use said default branch (e.g., in doc-gen4's case, main).

  Lake also supports configuring the registry endpoint via an environment variable: RESERVIOR_API_URL. Thus, any server providing a similar interface to Reservoir can be used as the registry. Further configuration options paralleling those of Cargo's Alternative Registries and Source Replacement will come in the future.

DevOps/CI

• #4427 uses Namespace runners for CI for leanprover/lean4.
• #4440 fixes speedcenter tests in CI.
• #4441 fixes that workflow change would break CI for unrebased PRs.
• #4442 fixes Wasm release-ci.
• 6d265b fixes for github.event.pull_request.merge_commit_sha sometimes not being available.
• 16cad2 adds optimization for CI to not fetch complete history.
• #4544 causes releases to be marked as prerelease on GitHub.
• #4446 switches Lake to using src/lake/lakefile.toml to avoid needing to load a version of Lake to build Lake.
• Nix
  • 5eb5fa fixes update-stage0-commit for Nix.
  • #4476 adds gdb to Nix shell.
  • e665a0 fixes update-stage0 for Nix.
  • 4808eb fixes cacheRoots for Nix.
  • #3811 adds platform-dependent flag to lib target.
  • #4587 adds linking of -lStd back into nix build flags on darwin.

Breaking changes

• Char.csize is replaced by Char.utf8Size (#4357).
• Library lemmas now are in terms of (· == a) over (a == ·) (#3056).
• Now the normal forms for indexing into List and Array is xs[n] and xs[n]? rather than using functions like List.get (#4400).
• Sometimes terms created via a sequence of unifications will be more eta reduced than before and proofs will require adaptation (#4387).
• The GetElem class has been split into two; see the docstrings for GetElem and GetElem? for more information (#4560).