perf: precise cache for expr_eq_fn

We also add `m_check_set` flag for controlling whether `check_cache`
should also inspect set of hashconsed objects or not.

RELEASES.md

@@ -14,10 +14,289 @@ Development in progress.
 
 v4.10.0
 ----------
-Release candidate, release notes will be copied from branch `releases/v4.10.0` once completed.
+
+### Language features, tactics, and metaprograms
+
+* `split` tactic:
+  * [#4401](https://github.com/leanprover/lean4/pull/4401) improves the strategy `split` uses to generalize discriminants of matches and adds `trace.split.failure` trace class for diagnosing issues.
+
+* `rw` tactic:
+  * [#4385](https://github.com/leanprover/lean4/pull/4385) prevents the tactic from claiming pre-existing goals are new subgoals.
+  * [dac1da](https://github.com/leanprover/lean4/commit/dac1dacc5b39911827af68247d575569d9c399b5) adds configuration for ordering new goals, like for `apply`.
+
+* `simp` tactic:
+  * [#4430](https://github.com/leanprover/lean4/pull/4430) adds `dsimproc`s for `if` expressions (`ite` and `dite`).
+  * [#4434](https://github.com/leanprover/lean4/pull/4434) improves heuristics for unfolding. Equational lemmas now have priorities where more-specific equationals lemmas are tried first before a possible catch-all.
+  * [#4481](https://github.com/leanprover/lean4/pull/4481) fixes an issue where function-valued `OfNat` numeric literals would become denormalized.
+  * [#4467](https://github.com/leanprover/lean4/pull/4467) fixes an issue where dsimp theorems might not apply to literals.
+  * [#4484](https://github.com/leanprover/lean4/pull/4484) fixes the source position for the warning for deprecated simp arguments.
+  * [#4258](https://github.com/leanprover/lean4/pull/4258) adds docstrings for `dsimp` configuration.
+  * [#4567](https://github.com/leanprover/lean4/pull/4567) improves the accuracy of used simp lemmas reported by `simp?`.
+  * [fb9727](https://github.com/leanprover/lean4/commit/fb97275dcbb683efe6da87ed10a3f0cd064b88fd) adds (but does not implement) the simp configuration option `implicitDefEqProofs`, which will enable including `rfl`-theorems in proof terms.
+* `omega` tactic:
+  * [#4360](https://github.com/leanprover/lean4/pull/4360) makes the tactic generate error messages lazily, improving its performance when used in tactic combinators.
+* `bv_omega` tactic:
+  * [#4579](https://github.com/leanprover/lean4/pull/4579) works around changes to the definition of `Fin.sub` in this release.
+* [#4490](https://github.com/leanprover/lean4/pull/4490) sets up groundwork for a tactic index in generated documentation, as there was in Lean 3. See PR description for details.
+
+* **Commands**
+  * [#4370](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/4408) fixes a discrepency in universe parameter order between `theorem` and `def` declarations.
+  * [#4493](https://github.com/leanprover/lean4/pull/4493) and
+    [#4482](https://github.com/leanprover/lean4/pull/4482) fix a discrepancy in the elaborators for `theorem`, `def`, and `example`,
+    making `Prop`-valued `example`s and other definition commands elaborate like `theorem`s.
+  * [8f023b](https://github.com/leanprover/lean4/commit/8f023b85c554186ae562774b8122322d856c674e), [3c4d6b](https://github.com/leanprover/lean4/commit/3c4d6ba8648eb04d90371eb3fdbd114d16949501) and [0783d0](https://github.com/leanprover/lean4/commit/0783d0fcbe31b626fbd3ed2f29d838e717f09101) 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](https://github.com/leanprover/lean4/pull/4489) fixes an elaboration bug in `#check_tactic`.
+  * [#4505](https://github.com/leanprover/lean4/pull/4505) adds support for `open _root_.<namespace>`.
+
+* **Options**
+  * [#4576](https://github.com/leanprover/lean4/pull/4576) adds the `debug.byAsSorry` option. Setting `set_option debug.byAsSorry true` causes all `by ...` terms to elaborate as `sorry`.
+  * [7b56eb](https://github.com/leanprover/lean4/commit/7b56eb20a03250472f4b145118ae885274d1f8f7) and [d8e719](https://github.com/leanprover/lean4/commit/d8e719f9ab7d049e423473dfc7a32867d32c856f) 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](https://github.com/leanprover/lean4/pull/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:
+
+  ```lean
+  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:
+
+  ```lean
+  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](https://github.com/leanprover/lean4/pull/4454) adds public `Name.isInternalDetail` function for filtering declarations using naming conventions for internal names.
+
+* **Other fixes or improvements**
+  * [#4416](https://github.com/leanprover/lean4/pull/4416) sorts the ouput of `#print axioms` for determinism.
+  * [#4528](https://github.com/leanprover/lean4/pull/4528) fixes error message range for the cdot focusing tactic.
+
+### Language server, widgets, and IDE extensions
+
+* [#4443](https://github.com/leanprover/lean4/pull/4443) makes the watchdog be more resilient against badly behaving clients.
+
+### Pretty printing
+
+* [#4433](https://github.com/leanprover/lean4/pull/4433) restores fallback pretty printers when context is not available, and documents `addMessageContext`.
+* [#4556](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/4389) makes `Array.toArrayAux_eq` be a `simp` lemma.
+  * [#4399](https://github.com/leanprover/lean4/pull/4399) improves robustness of the proof for `Array.reverse_data`.
+* `List`
+  * [#4469](https://github.com/leanprover/lean4/pull/4469) and [#4475](https://github.com/leanprover/lean4/pull/4475) improve the organization of the `List` API.
+  * [#4470](https://github.com/leanprover/lean4/pull/4470) improves the `List.set` and `List.concat` API.
+  * [#4472](https://github.com/leanprover/lean4/pull/4472) upstreams lemmas about `List.filter` from Batteries.
+  * [#4473](https://github.com/leanprover/lean4/pull/4473) adjusts `@[simp]` attributes.
+  * [#4488](https://github.com/leanprover/lean4/pull/4488) makes `List.getElem?_eq_getElem` be a simp lemma.
+  * [#4487](https://github.com/leanprover/lean4/pull/4487) adds missing `List.replicate` API.
+  * [#4521](https://github.com/leanprover/lean4/pull/4521) adds lemmas about `List.map`.
+  * [#4500](https://github.com/leanprover/lean4/pull/4500) changes `List.length_cons` to use `as.length + 1` instead of `as.length.succ`.
+  * [#4524](https://github.com/leanprover/lean4/pull/4524) fixes the statement of `List.filter_congr`.
+  * [#4525](https://github.com/leanprover/lean4/pull/4525) changes binder explicitness in `List.bind_map`.
+  * [#4550](https://github.com/leanprover/lean4/pull/4550) adds `maximum?_eq_some_iff'` and `minimum?_eq_some_iff?`.
+* [#4400](https://github.com/leanprover/lean4/pull/4400) switches the normal forms for indexing `List` and `Array` to `xs[n]` and `xs[n]?`.
+* `HashMap`
+  * [#4372](https://github.com/leanprover/lean4/pull/4372) fixes linearity in `HashMap.insert` and `HashMap.erase`, leading to a 40% speedup in a replace-heavy workload.
+* `Option`
+  * [#4403](https://github.com/leanprover/lean4/pull/4403) generalizes type of `Option.forM` from `Unit` to `PUnit`.
+  * [#4504](https://github.com/leanprover/lean4/pull/4504) remove simp attribute from `Option.elim` and instead adds it to individal reduction lemmas, making unfolding less aggressive.
+* `Nat`
+  * [#4242](https://github.com/leanprover/lean4/pull/4242) adds missing theorems for `n + 1` and `n - 1` normal forms.
+  * [#4486](https://github.com/leanprover/lean4/pull/4486) makes `Nat.min_assoc` be a simp lemma.
+  * [#4522](https://github.com/leanprover/lean4/pull/4522) moves `@[simp]` from `Nat.pred_le` to `Nat.sub_one_le`.
+  * [#4532](https://github.com/leanprover/lean4/pull/4532) changes various `Nat.succ n` to `n + 1`.
+* `Int`
+  * [#3850](https://github.com/leanprover/lean4/pull/3850) adds complete div/mod simprocs for `Int`.
+* `String`/`Char`
+  * [#4357](https://github.com/leanprover/lean4/pull/4357) make the byte size interface be `Nat`-valued with functions `Char.utf8Size` and `String.utf8ByteSize`.
+  * [#4438](https://github.com/leanprover/lean4/pull/4438) upstreams `Char.ext` from Batteries and adds some `Char` documentation to the manual.
+* `Fin`
+  * [#4421](https://github.com/leanprover/lean4/pull/4421) adjusts `Fin.sub` to be more performant in definitional equality checks.
+* `Prod`
+  * [#4526](https://github.com/leanprover/lean4/pull/4526) adds missing `Prod.map` lemmas.
+  * [#4533](https://github.com/leanprover/lean4/pull/4533) fixes binder explicitness in lemmas.
+* `BitVec`
+  * [#4428](https://github.com/leanprover/lean4/pull/4428) adds missing `simproc` for `BitVec` equality.
+  * [#4417](https://github.com/leanprover/lean4/pull/4417) adds `BitVec.twoPow` and lemmas, toward bitblasting multiplication for LeanSAT.
+* `Std` library
+  * [#4499](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/3056) standardizes on using `(· == a)` over `(a == ·)`.
+  * [#4502](https://github.com/leanprover/lean4/pull/4502) fixes errors reported by running the library through the the Batteries linters.
+
+### Lean internals
+
+* [#4391](https://github.com/leanprover/lean4/pull/4391) makes `getBitVecValue?` recognize `BitVec.ofNatLt`.
+* [#4410](https://github.com/leanprover/lean4/pull/4410) adjusts `instantiateMVars` algorithm to zeta reduce `let` expressions while beta reducing instantiated metavariables.
+* [#4420](https://github.com/leanprover/lean4/pull/4420) fixes occurs check for metavariable assignments to also take metavariable types into account.
+* [#4425](https://github.com/leanprover/lean4/pull/4425) fixes `forEachModuleInDir` to iterate over each Lean file exactly once.
+* [#3886](https://github.com/leanprover/lean4/pull/3886) adds support to build Lean core oleans using Lake.
+* **Defeq and WHNF algorithms**
+  * [#4387](https://github.com/leanprover/lean4/pull/4387) improves performance of `isDefEq` by eta reducing lambda-abstracted terms during metavariable assignments, since these are beta reduced during metavariable instantiation anyway.
+  * [#4388](https://github.com/leanprover/lean4/pull/4388) removes redundant code in `isDefEqQuickOther`.
+* **Typeclass inference**
+  * [#4530](https://github.com/leanprover/lean4/pull/4530) fixes handling of metavariables when caching results at `synthInstance?`.
+* **Elaboration**
+  * [#4426](https://github.com/leanprover/lean4/pull/4426) makes feature where the "don't know how to synthesize implicit argument" error reports the name of the argument more reliable.
+  * [#4497](https://github.com/leanprover/lean4/pull/4497) fixes a name resolution bug for generalized field notation (dot notation).
+  * [#4536](https://github.com/leanprover/lean4/pull/4536) blocks the implicit lambda feature for `(e :)` notation.
+  * [#4562](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/4474) takes a step to refactor `constructions` toward a future port to Lean.
+  * [#4498](https://github.com/leanprover/lean4/pull/4498) ports `mk_definition_inferring_unsafe` to Lean.
+  * [#4516](https://github.com/leanprover/lean4/pull/4516) ports `recOn` construction to Lean.
+  * [#4517](https://github.com/leanprover/lean4/pull/4517), [#4653](https://github.com/leanprover/lean4/pull/4653), and [#4651](https://github.com/leanprover/lean4/pull/4651) port `below` and `brecOn` construction to Lean.
+* Documentation
+  * [#4501](https://github.com/leanprover/lean4/pull/4501) adds a more-detailed docstring for `PersistentEnvExtension`.
+* **Other fixes or improvements**
+  * [#4382](https://github.com/leanprover/lean4/pull/4382) removes `@[inline]` attribute from `NameMap.find?`, which caused respecialization at each call site.
+  * [5f9ded](https://github.com/leanprover/lean4/commit/5f9dedfe5ee9972acdebd669f228f487844a6156) improves output of `trace.Elab.snapshotTree`.
+  * [#4424](https://github.com/leanprover/lean4/pull/4424) removes "you might need to open '{dir}' in your editor" message that is now handled by Lake and the VS Code extension.
+  * [#4451](https://github.com/leanprover/lean4/pull/4451) improves the performance of `CollectMVars` and `FindMVar`.
+  * [#4479](https://github.com/leanprover/lean4/pull/4479) adds missing `DecidableEq` and `Repr` instances for intermediate structures used by the `BitVec` and `Fin` simprocs.
+  * [#4492](https://github.com/leanprover/lean4/pull/4492) adds tests for a previous `isDefEq` issue.
+  * [9096d6](https://github.com/leanprover/lean4/commit/9096d6fc7180fe533c504f662bcb61550e4a2492) removes `PersistentHashMap.size`.
+  * [#4508](https://github.com/leanprover/lean4/pull/4508) fixes `@[implemented_by]` for functions defined by well-founded recursion.
+  * [#4509](https://github.com/leanprover/lean4/pull/4509) adds additional tests for `apply?` tactic.
+  * [d6eab3](https://github.com/leanprover/lean4/commit/d6eab393f4df9d473b5736d636b178eb26d197e6) fixes a benchmark.
+  * [#4563](https://github.com/leanprover/lean4/pull/4563) adds a workaround for a bug in `IndPredBelow.mkBelowMatcher`.
+* **Cleanup:** [#4380](https://github.com/leanprover/lean4/pull/4380), [#4431](https://github.com/leanprover/lean4/pull/4431), [#4494](https://github.com/leanprover/lean4/pull/4494), [e8f768](https://github.com/leanprover/lean4/commit/e8f768f9fd8cefc758533bc76e3a12b398ed4a39), [de2690](https://github.com/leanprover/lean4/commit/de269060d17a581ed87f40378dbec74032633b27), [d3a756](https://github.com/leanprover/lean4/commit/d3a7569c97123d022828106468d54e9224ed8207), [#4404](https://github.com/leanprover/lean4/pull/4404), [#4537](https://github.com/leanprover/lean4/pull/4537).
+
+### Compiler, runtime, and FFI
+
+* [d85d3d](https://github.com/leanprover/lean4/commit/d85d3d5f3a09ff95b2ee47c6f89ef50b7e339126) fixes criterion for tail-calls in ownership calculation.
+* [#3963](https://github.com/leanprover/lean4/pull/3963) adds validation of UTF-8 at the C++-to-Lean boundary in the runtime.
+* [#4512](https://github.com/leanprover/lean4/pull/4512) fixes missing unboxing in interpreter when loading initialized value.
+* [#4477](https://github.com/leanprover/lean4/pull/4477) exposes the compiler flags for the bundled C compiler (clang).
+
+### Lake
+
+* [#4384](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/4371) simplifies dependency resolution code.
+* [#4439](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/4485) fixes a bug where package versions in indirect dependencies would take precedence over direct dependencies.
+* [#4478](https://github.com/leanprover/lean4/pull/4478) fixes a bug where Lake incorrectly included the module dynamic library in a platform-independent trace.
+* [#4529](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/4564) fixes a bug where non-identifier script names could not be entered on the CLI without French quotes.
+* [#4566](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/4495), [#4692](https://github.com/leanprover/lean4/pull/4692), [#4849](https://github.com/leanprover/lean4/pull/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:
+
+  ```lean
+  require <scope> / <pkg-name> [@ git <rev>]
+  -- Examples:
+  require "leanprover" / "doc-gen4"
+  require "leanprover-community" / "proofwidgets" @ git "v0.0.39"
+  ```
+
+  Or in TOML:
+  ```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](https://doc.rust-lang.org/cargo/reference/registries.html)
+  and [Source Replacement](https://doc.rust-lang.org/cargo/reference/source-replacement.html)
+  will come in the future.
+
+### DevOps/CI
+* [#4427](https://github.com/leanprover/lean4/pull/4427) uses Namespace runners for CI for `leanprover/lean4`.
+* [#4440](https://github.com/leanprover/lean4/pull/4440) fixes speedcenter tests in CI.
+* [#4441](https://github.com/leanprover/lean4/pull/4441) fixes that workflow change would break CI for unrebased PRs.
+* [#4442](https://github.com/leanprover/lean4/pull/4442) fixes Wasm release-ci.
+* [6d265b](https://github.com/leanprover/lean4/commit/6d265b42b117eef78089f479790587a399da7690) fixes for `github.event.pull_request.merge_commit_sha` sometimes not being available.
+* [16cad2](https://github.com/leanprover/lean4/commit/16cad2b45c6a77efe4dce850dcdbaafaa7c91fc3) adds optimization for CI to not fetch complete history.
+* [#4544](https://github.com/leanprover/lean4/pull/4544) causes releases to be marked as prerelease on GitHub.
+* [#4446](https://github.com/leanprover/lean4/pull/4446) switches Lake to using `src/lake/lakefile.toml` to avoid needing to load a version of Lake to build Lake.
+* Nix
+  * [5eb5fa](https://github.com/leanprover/lean4/commit/5eb5fa49cf9862e99a5bccff8d4ca1a062f81900) fixes `update-stage0-commit` for Nix.
+  * [#4476](https://github.com/leanprover/lean4/pull/4476) adds gdb to Nix shell.
+  * [e665a0](https://github.com/leanprover/lean4/commit/e665a0d716dc42ba79b339b95e01eb99fe932cb3) fixes `update-stage0` for Nix.
+  * [4808eb](https://github.com/leanprover/lean4/commit/4808eb7c4bfb98f212b865f06a97d46c44978a61) fixes `cacheRoots` for Nix.
+  * [#3811](https://github.com/leanprover/lean4/pull/3811) adds platform-dependent flag to lib target.
+  * [#4587](https://github.com/leanprover/lean4/pull/4587) adds linking of `-lStd` back into nix build flags on darwin.
+
+### Breaking changes
+
+* `Char.csize` is replaced by `Char.utf8Size` ([#4357](https://github.com/leanprover/lean4/pull/4357)).
+* Library lemmas now are in terms of `(· == a)` over `(a == ·)` ([#3056](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/4400)).
+* Sometimes terms created via a sequence of unifications will be more eta reduced than before and proofs will require adaptation ([#4387](https://github.com/leanprover/lean4/pull/4387)).
+* The `GetElem` class has been split into two; see the docstrings for `GetElem` and `GetElem?` for more information ([#4560](https://github.com/leanprover/lean4/pull/4560)).
+
 
 v4.9.0
----------- 
+----------
 
 ### Language features, tactics, and metaprograms
 
@@ -40,6 +319,8 @@ v4.9.0
   * [#4395](https://github.com/leanprover/lean4/pull/4395) adds conservative fix for whitespace handling to avoid incremental reuse leading to goals in front of the text cursor being shown.
   * [#4407](https://github.com/leanprover/lean4/pull/4407) fixes non-incremental commands in macros blocking further incremental reporting.
   * [#4436](https://github.com/leanprover/lean4/pull/4436) fixes incremental reporting when there are nested tactics in terms.
+  * [#4459](https://github.com/leanprover/lean4/pull/4459) adds incrementality support for `next` and `if` tactics.
+  * [#4554](https://github.com/leanprover/lean4/pull/4554) disables incrementality for tactics in terms in tactics.
 * **Functional induction**
   * [#4135](https://github.com/leanprover/lean4/pull/4135) ensures that the names used for functional induction are reserved.
   * [#4327](https://github.com/leanprover/lean4/pull/4327) adds support for structural recursion on reflexive types.
@@ -85,7 +366,7 @@ v4.9.0
     When `index := 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.
     ```lean
     opaque f : Nat → Nat → Nat
@@ -105,7 +386,7 @@ v4.9.0
     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`
     ```
@@ -123,6 +404,8 @@ v4.9.0
   * [#4267](https://github.com/leanprover/lean4/pull/4267) cases signature elaboration errors to show even if there are parse errors in the body.
   * [#4368](https://github.com/leanprover/lean4/pull/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.
+  * [#4643](https://github.com/leanprover/lean4/pull/4643) fixes issue leading to nested error messages and info trees vanishing, where snapshot subtrees were not restored on reuse.
+  * [#4657](https://github.com/leanprover/lean4/pull/4657) calculates error suppression per snapshot, letting elaboration errors appear even when there are later parse errors ([RFC #3556](https://github.com/leanprover/lean4/issues/3556)).
 * **Metaprogramming**
   * [#4167](https://github.com/leanprover/lean4/pull/4167) adds `Lean.MVarId.revertAll` to revert all free variables.
   * [#4169](https://github.com/leanprover/lean4/pull/4169) adds `Lean.MVarId.ensureNoMVar` to ensure the goal's target contains no expression metavariables.
@@ -239,6 +522,8 @@ v4.9.0
   * [#4192](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/commit/dfb496a27123c3864571aec72f6278e2dad1cecf) fixes `declareBuiltin` to allow it to be called multiple times per declaration.
+  * [#4569](https://github.com/leanprover/lean4/pull/4569) fixes an issue introduced in a merge conflict, where the interrupt exception was swallowed by some `tryCatchRuntimeEx` uses.
+  * [b056a0](https://github.com/leanprover/lean4/commit/b056a0b395bb728512a3f3e83bf9a093059d4301) adapts kernel interruption to the new cancellation system.
   * Cleanup: [#4112](https://github.com/leanprover/lean4/pull/4112), [#4126](https://github.com/leanprover/lean4/pull/4126), [#4091](https://github.com/leanprover/lean4/pull/4091), [#4139](https://github.com/leanprover/lean4/pull/4139), [#4153](https://github.com/leanprover/lean4/pull/4153).
   * Tests: [030406](https://github.com/leanprover/lean4/commit/03040618b8f9b35b7b757858483e57340900cdc4), [#4133](https://github.com/leanprover/lean4/pull/4133).
 
@@ -249,6 +534,7 @@ v4.9.0
 * [#3915](https://github.com/leanprover/lean4/pull/3915) documents the runtime memory layout for inductive types.
 
 ### Lake
+* [#4518](https://github.com/leanprover/lean4/pull/4518) makes trace reading more robust. Lake now rebuilds if trace files are invalid or unreadable and is backwards compatible with previous pure numeric traces.
 * [#4057](https://github.com/leanprover/lean4/pull/4057) adds support for docstrings on `require` commands.
 * [#4088](https://github.com/leanprover/lean4/pull/4088) improves hovers for `family_def` and `library_data` commands.
 * [#4147](https://github.com/leanprover/lean4/pull/4147) adds default `README.md` to package templates
@@ -298,12 +584,14 @@ v4.9.0
 * [#4333](https://github.com/leanprover/lean4/pull/4333) adjusts workflow to update Batteries in manifest when creating `lean-pr-testing-NNNN` Mathlib branches.
 * [#4355](https://github.com/leanprover/lean4/pull/4355) simplifies `lean4checker` step of release checklist.
 * [#4361](https://github.com/leanprover/lean4/pull/4361) adds installing elan to `pr-release` CI step.
+* [#4628](https://github.com/leanprover/lean4/pull/4628) fixes the Windows build, which was missing an exported symbol.
 
 ### Breaking changes
 While most changes could be considered to be a breaking change, this section makes special note of API changes.
 
 * `Nat.zero_or` and `Nat.or_zero` have been swapped ([#4094](https://github.com/leanprover/lean4/pull/4094)).
 * `IsLawfulSingleton` is now `LawfulSingleton` ([#4350](https://github.com/leanprover/lean4/pull/4350)).
+* The `BitVec` literal notation is now `<num>#<term>` rather than `<term>#<term>`, and it is global rather than scoped. Use `BitVec.ofNat w x` rather than `x#w` when `x` is a not a numeric literal ([0d3051](https://github.com/leanprover/lean4/commit/0d30517dca094a07bcb462252f718e713b93ffba)).
 * `BitVec.rotateLeft` and `BitVec.rotateRight` now take the shift modulo the bitwidth ([#4229](https://github.com/leanprover/lean4/pull/4229)).
 * These are no longer simp lemmas:
   `List.length_pos` ([#4172](https://github.com/leanprover/lean4/pull/4172)),

doc/dev/release_checklist.md

@@ -5,8 +5,11 @@ See below for the checklist for release candidates.
 
 We'll use `v4.6.0` as the intended release version as a running example.
 
-- One week before the planned release, ensure that (1) someone has written the release notes and (2) someone has written the first draft of the release blog post.
-  If there is any material in `./releases_drafts/`, then the release notes are not done. (See the section "Writing the release notes".)
+- One week before the planned release, ensure that
+  (1) someone has written the release notes and
+  (2) someone has written the first draft of the release blog post.
+  If there is any material in `./releases_drafts/` on the `releases/v4.6.0` branch, then the release notes are not done.
+  (See the section "Writing the release notes".)
 - `git checkout releases/v4.6.0`
   (This branch should already exist, from the release candidates.)
 - `git pull`
@@ -187,6 +190,8 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
   Please also make sure that whoever is handling social media knows the release is out.
 - Begin the next development cycle (i.e. for `v4.8.0`) on the Lean repository, by making a PR that:
   - Updates `src/CMakeLists.txt` to say `set(LEAN_VERSION_MINOR 8)`
+  - Replaces the "release notes will be copied" text in the `v4.6.0` section of `RELEASES.md` with the
+    finalized release notes from the `releases/v4.6.0` branch.
   - Replaces the "development in progress" in the `v4.7.0` section of `RELEASES.md` with
     ```
     Release candidate, release notes will be copied from `branch releases/v4.7.0` once completed.
@@ -222,12 +227,15 @@ Please read https://leanprover-community.github.io/contribute/tags_and_branches.
   * This can either be done by the person managing this process directly,
     or by soliciting assistance from authors of files, or generally helpful people on Zulip!
 * Each repo has a `bump/v4.7.0` which accumulates reviewed changes adapting to new versions.
-* Once `nightly-testing` is working on a given nightly, say `nightly-2024-02-15`, we:
+* Once `nightly-testing` is working on a given nightly, say `nightly-2024-02-15`, we will create a PR to `bump/v4.7.0`.
+* For Mathlib, there is a script in `scripts/create-adaptation-pr.sh` that automates this process.
+* For Batteries and Aesop it is currently manual.
+* For all of these repositories, the process is the same:
   * Make sure `bump/v4.7.0` is up to date with `master` (by merging `master`, no PR necessary)
   * Create from `bump/v4.7.0` a `bump/nightly-2024-02-15` branch.
-  * In that branch, `git merge --squash nightly-testing` to bring across changes from `nightly-testing`.
+  * In that branch, `git merge nightly-testing` to bring across changes from `nightly-testing`.
   * Sanity check changes, commit, and make a PR to `bump/v4.7.0` from the `bump/nightly-2024-02-15` branch.
-  * Solicit review, merge the PR into `bump/v4,7,0`.
+  * Solicit review, merge the PR into `bump/v4.7.0`.
 * It is always okay to merge in the following directions:
   `master` -> `bump/v4.7.0` -> `bump/nightly-2024-02-15` -> `nightly-testing`.
   Please remember to push any merges you make to intermediate steps!
@@ -239,7 +247,7 @@ The exact steps are a work in progress.
 Here is the general idea:
 
 * The work is done right on the `releases/v4.6.0` branch sometime after it is created but before the stable release is made.
-  The release notes for `v4.6.0` will be copied to `master`.
+  The release notes for `v4.6.0` will later be copied to `master` when we begin a new development cycle.
 * There can be material for release notes entries in commit messages.
 * There can also be pre-written entries in `./releases_drafts`, which should be all incorporated in the release notes and then deleted from the branch.
   See `./releases_drafts/README.md` for more information.

releases_drafts/varCtorNameLint.md

@@ -1,45 +0,0 @@
-A new linter flags 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
-```
-
-
-#4301

src/Init/Core.lean

@@ -1204,12 +1204,12 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
 
 /-! # Dependent products -/
 
-theorem PSigma.exists {α : Sort u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
+theorem Exists.of_psigma_prop {α : Sort u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
   | ⟨x, hx⟩ => ⟨x, hx⟩
 
-@[deprecated PSigma.exists (since := "2024-07-27")]
+@[deprecated Exists.of_psigma_prop (since := "2024-07-27")]
 theorem ex_of_PSigma {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x) :=
-  PSigma.exists
+  Exists.of_psigma_prop
 
 protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂}
     (h₁ : a₁ = a₂) (h₂ : Eq.ndrec b₁ h₁ = b₂) : PSigma.mk a₁ b₁ = PSigma.mk a₂ b₂ := by

src/Init/Data/Array/Basic.lean

@@ -108,7 +108,7 @@ def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
   a'.set (size_set a i v₂ ▸ j) v₁
 
 /--
-Swaps two entries in an array, or panics if either index is out of bounds.
+Swaps two entries in an array, or returns the array unchanged if either index is out of bounds.
 
 This will perform the update destructively provided that `a` has a reference
 count of 1 when called.

src/Init/Data/BitVec/Bitblast.lean

@@ -403,12 +403,8 @@ theorem shiftLeftRec_eq {x : BitVec w₁} {y : BitVec w₂} {n : Nat} :
   induction n generalizing x y
   case zero =>
     ext i
-    simp only [shiftLeftRec_zero, twoPow_zero, Nat.reduceAdd, truncate_one]
-    suffices (y &&& 1#w₂) = zeroExtend w₂ (ofBool (y.getLsb 0)) by simp [this]
-    ext i
-    by_cases h : (↑i : Nat) = 0
-    · simp [h, Bool.and_comm]
-    · simp [h]; omega
+    simp only [shiftLeftRec_zero, twoPow_zero, Nat.reduceAdd, truncate_one,
+      and_one_eq_zeroExtend_ofBool_getLsb]
   case succ n ih =>
     simp only [shiftLeftRec_succ, and_twoPow]
     rw [ih]
@@ -431,4 +427,67 @@ theorem shiftLeft_eq_shiftLeftRec (x : BitVec w₁) (y : BitVec w₂) :
   · simp [of_length_zero]
   · simp [shiftLeftRec_eq]
 
+/- ### Logical shift right (ushiftRight) recurrence for bitblasting -/
+
+/--
+`ushiftRightRec x y n` shifts `x` logically to the right by the first `n` bits of `y`.
+
+The theorem `shiftRight_eq_ushiftRightRec` proves the equivalence
+of `(x >>> y)` and `ushiftRightRec`.
+
+Together with equations `ushiftRightRec_zero`, `ushiftRightRec_succ`,
+this allows us to unfold `ushiftRight` into a circuit for bitblasting.
+-/
+def ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) (n : Nat) : BitVec w₁ :=
+  let shiftAmt := (y &&& (twoPow w₂ n))
+  match n with
+  | 0 => x >>> shiftAmt
+  | n + 1 => (ushiftRightRec x y n) >>> shiftAmt
+
+@[simp]
+theorem ushiftRightRec_zero (x : BitVec w₁) (y : BitVec w₂) :
+    ushiftRightRec x y 0 = x >>> (y &&& twoPow w₂ 0) := by
+  simp [ushiftRightRec]
+
+@[simp]
+theorem ushiftRightRec_succ (x : BitVec w₁) (y : BitVec w₂) :
+    ushiftRightRec x y (n + 1) = (ushiftRightRec x y n) >>> (y &&& twoPow w₂ (n + 1)) := by
+  simp [ushiftRightRec]
+
+/--
+If `y &&& z = 0`, `x >>> (y ||| z) = x >>> y >>> z`.
+This follows as `y &&& z = 0` implies `y ||| z = y + z`,
+and thus `x >>> (y ||| z) = x >>> (y + z) = x >>> y >>> z`.
+-/
+theorem ushiftRight'_or_of_and_eq_zero {x : BitVec w₁} {y z : BitVec w₂}
+    (h : y &&& z = 0#w₂) :
+    x >>> (y ||| z) = x >>> y >>> z := by
+  simp [← add_eq_or_of_and_eq_zero _ _ h, toNat_add_of_and_eq_zero h, shiftRight_add]
+
+theorem ushiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
+    ushiftRightRec x y n = x >>> (y.truncate (n + 1)).zeroExtend w₂ := by
+  induction n generalizing x y
+  case zero =>
+    ext i
+    simp only [ushiftRightRec_zero, twoPow_zero, Nat.reduceAdd,
+      and_one_eq_zeroExtend_ofBool_getLsb, truncate_one]
+  case succ n ih =>
+    simp only [ushiftRightRec_succ, and_twoPow]
+    rw [ih]
+    by_cases h : y.getLsb (n + 1) <;> simp only [h, ↓reduceIte]
+    · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true h,
+        ushiftRight'_or_of_and_eq_zero]
+      simp
+    · simp [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false, h]
+
+/--
+Show that `x >>> y` can be written in terms of `ushiftRightRec`.
+This can be unfolded in terms of `ushiftRightRec_zero`, `ushiftRightRec_succ` for bitblasting.
+-/
+theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) :
+    x >>> y = ushiftRightRec x y (w₂ - 1) := by
+  rcases w₂ with rfl | w₂
+  · simp [of_length_zero]
+  · simp [ushiftRightRec_eq]
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -731,6 +731,16 @@ theorem getLsb_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} :
     getLsb (x >>> i) j = getLsb x (i+j) := by
   unfold getLsb ; simp
 
+@[simp]
+theorem ushiftRight_zero_eq (x : BitVec w) : x >>> 0 = x := by
+  simp [bv_toNat]
+
+/-! ### ushiftRight reductions from BitVec to Nat -/
+
+@[simp]
+theorem ushiftRight_eq' (x : BitVec w₁) (y : BitVec w₂) :
+    x >>> y = x >>> y.toNat := by rfl
+
 /-! ### sshiftRight -/
 
 theorem sshiftRight_eq {x : BitVec n} {i : Nat} :
@@ -1549,4 +1559,12 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true
     simp [hx]
   · by_cases hik' : k < i + 1 <;> simp [hik, hik'] <;> omega
 
+/-- Bitwise and of `(x : BitVec w)` with `1#w` equals zero extending `x.lsb` to `w`. -/
+theorem and_one_eq_zeroExtend_ofBool_getLsb {x : BitVec w} :
+    (x &&& 1#w) = zeroExtend w (ofBool (x.getLsb 0)) := by
+  ext i
+  simp only [getLsb_and, getLsb_one, getLsb_zeroExtend, Fin.is_lt, decide_True, getLsb_ofBool,
+    Bool.true_and]
+  by_cases h : (0 = (i : Nat)) <;> simp [h] <;> omega
+
 end BitVec

src/Init/Data/List/Sublist.lean

@@ -84,7 +84,7 @@ theorem cons_subset_cons {l₁ l₂ : List α} (a : α) (s : l₁ ⊆ l₂) : a
 @[simp] theorem subset_nil {l : List α} : l ⊆ [] ↔ l = [] :=
   ⟨fun h => match l with | [] => rfl | _::_ => (nomatch h (.head ..)), fun | rfl => Subset.refl _⟩
 
-theorem map_subset {l₁ l₂ : List α} {f : α → β} (h : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ :=
+theorem map_subset {l₁ l₂ : List α} (f : α → β) (h : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ :=
   fun x => by simp only [mem_map]; exact .imp fun a => .imp_left (@h _)
 
 theorem filter_subset {l₁ l₂ : List α} (p : α → Bool) (H : l₁ ⊆ l₂) : filter p l₁ ⊆ filter p l₂ :=

src/Init/Data/List/TakeDrop.lean

@@ -411,11 +411,11 @@ theorem dropWhile_replicate (p : α → Bool) :
   split <;> simp_all
 
 theorem take_takeWhile {l : List α} (p : α → Bool) n :
-    (l.takeWhile p).take n = (l.takeWhile p).take n := by
-  induction l with
-  | nil => rfl
+    (l.takeWhile p).take n = (l.take n).takeWhile p := by
+  induction l generalizing n with
+  | nil => simp
   | cons x xs ih =>
-    by_cases h : p x <;> simp [takeWhile_cons, h, ih]
+    by_cases h : p x <;> cases n <;> simp [takeWhile_cons, h, ih, take_succ_cons]
 
 @[simp] theorem all_takeWhile {l : List α} : (l.takeWhile p).all p = true := by
   induction l with

src/Init/ShareCommon.lean

@@ -109,4 +109,4 @@ A more restrictive but efficient max sharing primitive.
 Remark: it optimizes the number of RC operations, and the strategy for caching results.
 -/
 @[extern "lean_sharecommon_quick"]
-def ShareCommon.shareCommon' (a : α) : α := a
+def ShareCommon.shareCommon' (a : @& α) : α := a

src/Lean/CoreM.lean

@@ -31,7 +31,16 @@ register_builtin_option maxHeartbeats : Nat := {
   descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
 }
 
-def useDiagnosticMsg := s!"use `set_option {diagnostics.name} true` to get diagnostic information"
+/--
+If the `diagnostics` option is not already set, gives a message explaining this option.
+Begins with a `\n`, so an error message can look like `m!"some error occurred{useDiagnosticMsg}"`.
+-/
+def useDiagnosticMsg : MessageData :=
+  MessageData.lazy fun ctx =>
+    if diagnostics.get ctx.opts then
+      pure ""
+    else
+      pure s!"\nAdditional diagnostic information may be available using the `set_option {diagnostics.name} true` command."
 
 namespace Core
 
@@ -300,8 +309,10 @@ register_builtin_option debug.moduleNameAtTimeout : Bool := {
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
   let includeModuleName := debug.moduleNameAtTimeout.get (← getOptions)
   let atModuleName := if includeModuleName then s!" at `{moduleName}`" else ""
-  let msg := s!"(deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\n{useDiagnosticMsg}"
-  throw <| Exception.error (← getRef) (MessageData.ofFormat (Std.Format.text msg))
+  throw <| Exception.error (← getRef) m!"\
+    (deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\n\
+    Use `set_option {optionName} <num>` to set the limit.\
+    {useDiagnosticMsg}"
 
 def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do
   unless max == 0 do

src/Lean/Elab/Calc.lean

@@ -42,7 +42,7 @@ def mkCalcTrans (result resultType step stepType : Expr) : MetaM (Expr × Expr)
     unless (← getCalcRelation? resultType).isSome do
       throwError "invalid 'calc' step, step result is not a relation{indentExpr resultType}"
     return (result, resultType)
-  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}\n{useDiagnosticMsg}"
+  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}{useDiagnosticMsg}"
 
 /--
 Adds a type annotation to a hole that occurs immediately at the beginning of the term.

src/Lean/Elab/Import.lean

@@ -39,7 +39,7 @@ def parseImports (input : String) (fileName : Option String := none) : IO (Array
 def printImports (input : String) (fileName : Option String) : IO Unit := do
   let (deps, _, _) ← parseImports input fileName
   for dep in deps do
-    let fname ← findOLean dep.module
+    let fname ← findOLean (checkExists := false) dep.module
     IO.println fname
 
 end Lean.Elab

src/Lean/Elab/Term.lean

@@ -996,7 +996,7 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
     if (← read).ignoreTCFailures then
       return false
     else
-      throwError "failed to synthesize{indentExpr type}{extraErrorMsg}\n{useDiagnosticMsg}"
+      throwError "failed to synthesize{indentExpr type}{extraErrorMsg}{useDiagnosticMsg}"
 
 def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
   withTraceNode `Elab.coe (fun _ => return m!"adding coercion for {e} : {← inferType e} =?= {expectedType}") do

src/Lean/Environment.lean

@@ -806,8 +806,6 @@ partial def importModulesCore (imports : Array Import) : ImportStateM Unit := do
       continue
     modify fun s => { s with moduleNameSet := s.moduleNameSet.insert i.module }
     let mFile ← findOLean i.module
-    unless (← mFile.pathExists) do
-      throw <| IO.userError s!"object file '{mFile}' of module {i.module} does not exist"
     let (mod, region) ← readModuleData mFile
     importModulesCore mod.imports
     modify fun s => { s with

src/Lean/Language/Lean.lean

@@ -10,8 +10,8 @@ Authors: Sebastian Ullrich
 
 prelude
 import Lean.Language.Basic
+import Lean.Language.Lean.Types
 import Lean.Parser.Module
-import Lean.Elab.Command
 import Lean.Elab.Import
 
 /-!
@@ -166,11 +166,6 @@ namespace Lean.Language.Lean
 open Lean.Elab Command
 open Lean.Parser
 
-private def pushOpt (a? : Option α) (as : Array α) : Array α :=
-  match a? with
-  | some a => as.push a
-  | none   => as
-
 /-- Option for capturing output to stderr during elaboration. -/
 register_builtin_option stderrAsMessages : Bool := {
   defValue := true
@@ -178,101 +173,6 @@ register_builtin_option stderrAsMessages : Bool := {
   descr    := "(server) capture output to the Lean stderr channel (such as from `dbg_trace`) during elaboration of a command as a diagnostic message"
 }
 
-/-! The hierarchy of Lean snapshot types -/
-
-/-- Snapshot after elaboration of the entire command. -/
-structure CommandFinishedSnapshot extends Language.Snapshot where
-  /-- Resulting elaboration state. -/
-  cmdState : Command.State
-deriving Nonempty
-instance : ToSnapshotTree CommandFinishedSnapshot where
-  toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
-
-/-- State after a command has been parsed. -/
-structure CommandParsedSnapshotData extends Snapshot where
-  /-- Syntax tree of the command. -/
-  stx : Syntax
-  /-- Resulting parser state. -/
-  parserState : Parser.ModuleParserState
-  /--
-  Snapshot for incremental reporting and reuse during elaboration, type dependent on specific
-  elaborator.
-   -/
-  elabSnap : SnapshotTask DynamicSnapshot
-  /-- State after processing is finished. -/
-  finishedSnap : SnapshotTask CommandFinishedSnapshot
-  /-- Cache for `save`; to be replaced with incrementality. -/
-  tacticCache : IO.Ref Tactic.Cache
-deriving Nonempty
-
-/-- State after a command has been parsed. -/
--- workaround for lack of recursive structures
-inductive CommandParsedSnapshot where
-  /-- Creates a command parsed snapshot. -/
-  | mk (data : CommandParsedSnapshotData)
-    (nextCmdSnap? : Option (SnapshotTask CommandParsedSnapshot))
-deriving Nonempty
-/-- The snapshot data. -/
-abbrev CommandParsedSnapshot.data : CommandParsedSnapshot → CommandParsedSnapshotData
-  | mk data _ => data
-/-- Next command, unless this is a terminal command. -/
-abbrev CommandParsedSnapshot.nextCmdSnap? : CommandParsedSnapshot →
-    Option (SnapshotTask CommandParsedSnapshot)
-  | mk _ next? => next?
-partial instance : ToSnapshotTree CommandParsedSnapshot where
-  toSnapshotTree := go where
-    go s := ⟨s.data.toSnapshot,
-      #[s.data.elabSnap.map (sync := true) toSnapshotTree,
-        s.data.finishedSnap.map (sync := true) toSnapshotTree] |>
-        pushOpt (s.nextCmdSnap?.map (·.map (sync := true) go))⟩
-
-/-- State after successful importing. -/
-structure HeaderProcessedState where
-  /-- The resulting initial elaboration state. -/
-  cmdState : Command.State
-  /-- First command task (there is always at least a terminal command). -/
-  firstCmdSnap : SnapshotTask CommandParsedSnapshot
-
-/-- State after the module header has been processed including imports. -/
-structure HeaderProcessedSnapshot extends Snapshot where
-  /-- State after successful importing. -/
-  result? : Option HeaderProcessedState
-  isFatal := result?.isNone
-instance : ToSnapshotTree HeaderProcessedSnapshot where
-  toSnapshotTree s := ⟨s.toSnapshot, #[] |>
-    pushOpt (s.result?.map (·.firstCmdSnap.map (sync := true) toSnapshotTree))⟩
-
-/-- State after successfully parsing the module header. -/
-structure HeaderParsedState where
-  /-- Resulting parser state. -/
-  parserState : Parser.ModuleParserState
-  /-- Header processing task. -/
-  processedSnap : SnapshotTask HeaderProcessedSnapshot
-
-/-- State after the module header has been parsed. -/
-structure HeaderParsedSnapshot extends Snapshot where
-  /-- Parser input context supplied by the driver, stored here for incremental parsing. -/
-  ictx : Parser.InputContext
-  /-- Resulting syntax tree. -/
-  stx : Syntax
-  /-- State after successful parsing. -/
-  result? : Option HeaderParsedState
-  isFatal := result?.isNone
-  /-- Cancellation token for interrupting processing of this run. -/
-  cancelTk? : Option IO.CancelToken
-
-instance : ToSnapshotTree HeaderParsedSnapshot where
-  toSnapshotTree s := ⟨s.toSnapshot,
-    #[] |> pushOpt (s.result?.map (·.processedSnap.map (sync := true) toSnapshotTree))⟩
-
-/-- Shortcut accessor to the final header state, if successful. -/
-def HeaderParsedSnapshot.processedResult (snap : HeaderParsedSnapshot) :
-    SnapshotTask (Option HeaderProcessedState) :=
-  snap.result?.bind (·.processedSnap.map (sync := true) (·.result?)) |>.getD (.pure none)
-
-/-- Initial snapshot of the Lean language processor: a "header parsed" snapshot. -/
-abbrev InitialSnapshot := HeaderParsedSnapshot
-
 /-- Lean-specific processing context. -/
 structure LeanProcessingContext extends ProcessingContext where
   /-- Position of the first file difference if there was a previous invocation. -/

src/Lean/Language/Lean/Types.lean

@@ -0,0 +1,119 @@
+/-
+Copyright (c) 2023 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Implementation of the Lean language: parsing and processing of header and commands, incremental
+recompilation
+
+Authors: Sebastian Ullrich
+-/
+
+prelude
+import Lean.Language.Basic
+import Lean.Elab.Command
+
+set_option linter.missingDocs true
+
+namespace Lean.Language.Lean
+open Lean.Elab Command
+open Lean.Parser
+
+private def pushOpt (a? : Option α) (as : Array α) : Array α :=
+  match a? with
+  | some a => as.push a
+  | none   => as
+
+/-! The hierarchy of Lean snapshot types -/
+
+/-- Snapshot after elaboration of the entire command. -/
+structure CommandFinishedSnapshot extends Language.Snapshot where
+  /-- Resulting elaboration state. -/
+  cmdState : Command.State
+deriving Nonempty
+instance : ToSnapshotTree CommandFinishedSnapshot where
+  toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
+
+/-- State after a command has been parsed. -/
+structure CommandParsedSnapshotData extends Snapshot where
+  /-- Syntax tree of the command. -/
+  stx : Syntax
+  /-- Resulting parser state. -/
+  parserState : Parser.ModuleParserState
+  /--
+  Snapshot for incremental reporting and reuse during elaboration, type dependent on specific
+  elaborator.
+   -/
+  elabSnap : SnapshotTask DynamicSnapshot
+  /-- State after processing is finished. -/
+  finishedSnap : SnapshotTask CommandFinishedSnapshot
+  /-- Cache for `save`; to be replaced with incrementality. -/
+  tacticCache : IO.Ref Tactic.Cache
+deriving Nonempty
+
+/-- State after a command has been parsed. -/
+-- workaround for lack of recursive structures
+inductive CommandParsedSnapshot where
+  /-- Creates a command parsed snapshot. -/
+  | mk (data : CommandParsedSnapshotData)
+    (nextCmdSnap? : Option (SnapshotTask CommandParsedSnapshot))
+deriving Nonempty
+/-- The snapshot data. -/
+abbrev CommandParsedSnapshot.data : CommandParsedSnapshot → CommandParsedSnapshotData
+  | mk data _ => data
+/-- Next command, unless this is a terminal command. -/
+abbrev CommandParsedSnapshot.nextCmdSnap? : CommandParsedSnapshot →
+    Option (SnapshotTask CommandParsedSnapshot)
+  | mk _ next? => next?
+partial instance : ToSnapshotTree CommandParsedSnapshot where
+  toSnapshotTree := go where
+    go s := ⟨s.data.toSnapshot,
+      #[s.data.elabSnap.map (sync := true) toSnapshotTree,
+        s.data.finishedSnap.map (sync := true) toSnapshotTree] |>
+        pushOpt (s.nextCmdSnap?.map (·.map (sync := true) go))⟩
+
+/-- State after successful importing. -/
+structure HeaderProcessedState where
+  /-- The resulting initial elaboration state. -/
+  cmdState : Command.State
+  /-- First command task (there is always at least a terminal command). -/
+  firstCmdSnap : SnapshotTask CommandParsedSnapshot
+
+/-- State after the module header has been processed including imports. -/
+structure HeaderProcessedSnapshot extends Snapshot where
+  /-- State after successful importing. -/
+  result? : Option HeaderProcessedState
+  isFatal := result?.isNone
+instance : ToSnapshotTree HeaderProcessedSnapshot where
+  toSnapshotTree s := ⟨s.toSnapshot, #[] |>
+    pushOpt (s.result?.map (·.firstCmdSnap.map (sync := true) toSnapshotTree))⟩
+
+/-- State after successfully parsing the module header. -/
+structure HeaderParsedState where
+  /-- Resulting parser state. -/
+  parserState : Parser.ModuleParserState
+  /-- Header processing task. -/
+  processedSnap : SnapshotTask HeaderProcessedSnapshot
+
+/-- State after the module header has been parsed. -/
+structure HeaderParsedSnapshot extends Snapshot where
+  /-- Parser input context supplied by the driver, stored here for incremental parsing. -/
+  ictx : Parser.InputContext
+  /-- Resulting syntax tree. -/
+  stx : Syntax
+  /-- State after successful parsing. -/
+  result? : Option HeaderParsedState
+  isFatal := result?.isNone
+  /-- Cancellation token for interrupting processing of this run. -/
+  cancelTk? : Option IO.CancelToken
+
+instance : ToSnapshotTree HeaderParsedSnapshot where
+  toSnapshotTree s := ⟨s.toSnapshot,
+    #[] |> pushOpt (s.result?.map (·.processedSnap.map (sync := true) toSnapshotTree))⟩
+
+/-- Shortcut accessor to the final header state, if successful. -/
+def HeaderParsedSnapshot.processedResult (snap : HeaderParsedSnapshot) :
+    SnapshotTask (Option HeaderProcessedState) :=
+  snap.result?.bind (·.processedSnap.map (sync := true) (·.result?)) |>.getD (.pure none)
+
+/-- Initial snapshot of the Lean language processor: a "header parsed" snapshot. -/
+abbrev InitialSnapshot := HeaderParsedSnapshot

src/Lean/Meta/SynthInstance.lean

@@ -636,7 +636,7 @@ def main (type : Expr) (maxResultSize : Nat) : MetaM (Option AbstractMVarsResult
        (action.run { maxResultSize := maxResultSize, maxHeartbeats := getMaxHeartbeats (← getOptions) } |>.run' {})
        fun ex =>
          if ex.isRuntime then
-           throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}\n{useDiagnosticMsg}"
+           throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}{useDiagnosticMsg}"
          else
            throw ex
 
@@ -810,7 +810,7 @@ def trySynthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM
     (fun _ => pure LOption.undef)
 
 def throwFailedToSynthesize (type : Expr) : MetaM Expr :=
-  throwError "failed to synthesize{indentExpr type}\n{useDiagnosticMsg}"
+  throwError "failed to synthesize{indentExpr type}{useDiagnosticMsg}"
 
 def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Expr :=
   catchInternalId isDefEqStuckExceptionId

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -60,6 +60,16 @@ builtin_dsimproc [simp, seval] reducePow ((_ ^ _ : Nat)) := fun e => do
   unless (← checkExponent m) do return .continue
   return .done <| toExpr (n ^ m)
 
+builtin_dsimproc [simp, seval] reduceAnd ((_ &&& _ : Nat)) := reduceBin ``HOr.hOr 6 (· &&& ·)
+builtin_dsimproc [simp, seval] reduceXor ((_ ^^^ _ : Nat)) := reduceBin ``HXor.hXor 6 (· ^^^ ·)
+builtin_dsimproc [simp, seval] reduceOr ((_ ||| _ : Nat)) := reduceBin ``HOr.hOr 6 (· ||| ·)
+
+builtin_dsimproc [simp, seval] reduceShiftLeft ((_ <<< _ : Nat)) :=
+  reduceBin ``HShiftLeft.hShiftLeft 6 (· <<< ·)
+
+builtin_dsimproc [simp, seval] reduceShiftRight ((_ >>> _ : Nat)) :=
+  reduceBin ``HShiftRight.hShiftRight 6 (· >>> ·)
+
 builtin_dsimproc [simp, seval] reduceGcd (gcd _ _)       := reduceBin ``gcd 2 gcd
 
 builtin_simproc [simp, seval] reduceLT  (( _ : Nat) < _)  := reduceBinPred ``LT.lt 4 (. < .)

src/Lean/Parser/Command.lean

@@ -703,6 +703,9 @@ list, so it should be brief.
 @[builtin_command_parser] def genInjectiveTheorems := leading_parser
   "gen_injective_theorems% " >> ident
 
+/-- To be implemented. -/
+@[builtin_command_parser] def «include» := leading_parser "include " >> many1 (checkColGt >> ident)
+
 /-- No-op parser used as syntax kind for attaching remaining whitespace at the end of the input. -/
 @[run_builtin_parser_attribute_hooks] def eoi : Parser := leading_parser ""
 

src/Lean/Server/FileWorker.lean

@@ -16,7 +16,7 @@ import Lean.Data.Json.FromToJson
 
 import Lean.Util.FileSetupInfo
 import Lean.LoadDynlib
-import Lean.Language.Basic
+import Lean.Language.Lean
 
 import Lean.Server.Utils
 import Lean.Server.AsyncList

src/Lean/Server/FileWorker/Utils.lean

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki, Marc Huisinga
 -/
 prelude
-import Lean.Language.Lean
+import Lean.Language.Lean.Types
 import Lean.Server.Utils
 import Lean.Server.Snapshots
 import Lean.Server.AsyncList

src/Lean/Server/Snapshots.lean

@@ -9,7 +9,6 @@ import Init.System.IO
 
 import Lean.Elab.Import
 import Lean.Elab.Command
-import Lean.Language.Lean
 
 import Lean.Widget.InteractiveDiagnostic
 

src/Lean/Util/Path.lean

@@ -40,25 +40,52 @@ where
   | Name.anonymous => base
   | Name.num _ _ => panic! "ill-formed import"
 
+variable (base : FilePath) (ext : String) in
+/--
+Checks whether a module of the given name and extension exists in `base`; this uses case-sensitive
+path comparisons regardless of underlying file system to ensure the check is consistent across
+platforms.
+-/
+partial def moduleExists : Name → IO Bool := go ext
+where go (ext : String)
+  | .mkStr parent str => do
+    -- Case-sensitive check for file with extension in top-level call, for directory recursively
+    let entryName := if ext.isEmpty then str else s!"{str}.{ext}"
+    unless (← go "" parent) do
+      return false
+    return (← (modToFilePath base parent "").readDir).any (·.fileName == entryName)
+  | .anonymous => base.pathExists
+  | .num .. => panic! "ill-formed import"
+
 /-- A `.olean' search path. -/
 abbrev SearchPath := System.SearchPath
 
 namespace SearchPath
 
+def findRoot (sp : SearchPath) (ext : String) (pkg : String) : IO (Option FilePath) := do
+  sp.findM? fun p => do
+    unless (← p.isDir) do  -- Lake may pass search roots that do not exist (yet)
+      return false
+    if (← (p / pkg).isDir) then
+      return (← p.readDir).any (·.fileName == pkg)
+    else
+      let fileName := s!"{pkg}.{ext}"
+      return (← p.readDir).any (·.fileName == fileName)
+
 /-- If the package of `mod` can be found in `sp`, return the path with extension
 `ext` (`lean` or `olean`) corresponding to `mod`. Otherwise, return `none`. Does
 not check whether the returned path exists. -/
 def findWithExt (sp : SearchPath) (ext : String) (mod : Name) : IO (Option FilePath) := do
   let pkg := mod.getRoot.toString (escape := false)
-  let root? ← sp.findM? fun p =>
-    (p / pkg).isDir <||> ((p / pkg).addExtension ext).pathExists
+  let root? ← findRoot sp ext pkg
   return root?.map (modToFilePath · mod ext)
 
 /-- Like `findWithExt`, but ensures the returned path exists. -/
 def findModuleWithExt (sp : SearchPath) (ext : String) (mod : Name) : IO (Option FilePath) := do
-  if let some path ← findWithExt sp ext mod then
-    if ← path.pathExists then
-      return some path
+  let pkg := mod.getRoot.toString (escape := false)
+  if let some root ← findRoot sp ext pkg then
+    if (← moduleExists root ext mod) then
+      return some <| modToFilePath root mod ext
   return none
 
 def findAllWithExt (sp : SearchPath) (ext : String) : IO (Array FilePath) := do
@@ -105,12 +132,20 @@ def initSearchPath (leanSysroot : FilePath) (sp : SearchPath := ∅) : IO Unit :
 private def initSearchPathInternal : IO Unit := do
   initSearchPath (← getBuildDir)
 
-partial def findOLean (mod : Name) : IO FilePath := do
+/--
+Returns the path of the .olean file for `mod`. Throws an error if no search path entry for `mod`
+could be located, or if `checkExists` is true and the resulting path does not exist.
+-/
+partial def findOLean (mod : Name) (checkExists := true) : IO FilePath := do
   let sp ← searchPathRef.get
-  if let some fname ← sp.findWithExt "olean" mod then
-    return fname
+  let pkg := mod.getRoot.toString (escape := false)
+  if let some root ← sp.findRoot "olean" pkg then
+    let path := modToFilePath root mod "olean"
+    if !checkExists || (← moduleExists root "olean" mod) then
+      return path
+    else
+      throw <| IO.userError s!"object file '{path}' of module {mod} does not exist"
   else
-    let pkg := FilePath.mk <| mod.getRoot.toString (escape := false)
     let mut msg := s!"unknown module prefix '{pkg}'
 
 No directory '{pkg}' or file '{pkg}.olean' in the search path entries:

src/kernel/environment.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <limits>
 #include "runtime/sstream.h"
 #include "runtime/thread.h"
+#include "runtime/sharecommon.h"
 #include "util/map_foreach.h"
 #include "util/io.h"
 #include "kernel/environment.h"
@@ -220,12 +221,15 @@ environment environment::add_theorem(declaration const & d, bool check) const {
     theorem_val const & v = d.to_theorem_val();
     if (check) {
         type_checker checker(*this, diag.get());
-        if (!checker.is_prop(v.get_type()))
-            throw theorem_type_is_not_prop(*this, v.get_name(), v.get_type());
+        sharecommon_persistent_fn share;
+        expr val(share(v.get_value().raw()));
+        expr type(share(v.get_type().raw()));
+        if (!checker.is_prop(type))
+            throw theorem_type_is_not_prop(*this, v.get_name(), type);
         check_constant_val(*this, v.to_constant_val(), checker);
-        check_no_metavar_no_fvar(*this, v.get_name(), v.get_value());
-        expr val_type = checker.check(v.get_value(), v.get_lparams());
-        if (!checker.is_def_eq(val_type, v.get_type()))
+        check_no_metavar_no_fvar(*this, v.get_name(), val);
+        expr val_type = checker.check(val, v.get_lparams());
+        if (!checker.is_def_eq(val_type, type))
             throw definition_type_mismatch_exception(*this, d, val_type);
     }
     return diag.update(add(constant_info(d)));

src/kernel/expr_eq_fn.cpp

@@ -11,65 +11,49 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 #include "kernel/expr_sets.h"
 
-#ifndef LEAN_EQ_CACHE_CAPACITY
-#define LEAN_EQ_CACHE_CAPACITY 1024*8
-#endif
-
 namespace lean {
-struct eq_cache {
-    struct entry {
-        object * m_a;
-        object * m_b;
-        entry():m_a(nullptr), m_b(nullptr) {}
-    };
-    unsigned              m_capacity;
-    std::vector<entry>    m_cache;
-    std::vector<unsigned> m_used;
-    eq_cache():m_capacity(LEAN_EQ_CACHE_CAPACITY), m_cache(LEAN_EQ_CACHE_CAPACITY) {}
+/**
+\brief Functional object for comparing expressions.
 
-    bool check(expr const & a, expr const & b) {
-        if (!is_shared(a) || !is_shared(b))
-            return false;
-        unsigned i = hash(hash(a), hash(b)) % m_capacity;
-        if (m_cache[i].m_a == a.raw() && m_cache[i].m_b == b.raw()) {
-            return true;
-        } else {
-            if (m_cache[i].m_a == nullptr)
-                m_used.push_back(i);
-            m_cache[i].m_a = a.raw();
-            m_cache[i].m_b = b.raw();
-            return false;
-        }
-    }
-
-    void clear() {
-        for (unsigned i : m_used)
-            m_cache[i].m_a = nullptr;
-        m_used.clear();
-    }
-};
-
-/* CACHE_RESET: No */
-MK_THREAD_LOCAL_GET_DEF(eq_cache, get_eq_cache);
-
-/** \brief Functional object for comparing expressions.
-
-    Remark if CompareBinderInfo is true, then functional object will also compare
-    binder information attached to lambda and Pi expressions */
+Remark if CompareBinderInfo is true, then functional object will also compare
+binder information attached to lambda and Pi expressions
+*/
 template<bool CompareBinderInfo>
 class expr_eq_fn {
-    eq_cache & m_cache;
-
+    struct key_hasher {
+        std::size_t operator()(std::pair<lean_object *, lean_object *> const & p) const {
+            return hash((size_t)p.first >> 3, (size_t)p.first >> 3);
+        }
+    };
+    typedef std::unordered_set<std::pair<lean_object *, lean_object *>, key_hasher> cache;
+    cache * m_cache = nullptr;
+    bool check_cache(expr const & a, expr const & b) {
+        if (!is_shared(a) || !is_shared(b))
+            return false;
+        if (!m_cache)
+            m_cache = new cache();
+        std::pair<lean_object *, lean_object *> key(a.raw(), b.raw());
+        if (m_cache->find(key) != m_cache->end())
+            return true;
+        m_cache->insert(key);
+        return false;
+    }
     static void check_system() {
         ::lean::check_system("expression equality test");
     }
-
-    bool apply(expr const & a, expr const & b) {
+    bool apply(expr const & a, expr const & b, bool root = false) {
         if (is_eqp(a, b))          return true;
         if (hash(a) != hash(b))    return false;
         if (a.kind() != b.kind())  return false;
-        if (is_bvar(a))            return bvar_idx(a) == bvar_idx(b);
-        if (m_cache.check(a, b))
+        switch (a.kind()) {
+        case expr_kind::BVar: return bvar_idx(a) == bvar_idx(b);
+        case expr_kind::Lit:  return lit_value(a) == lit_value(b);
+        case expr_kind::MVar: return mvar_name(a) == mvar_name(b);
+        case expr_kind::FVar: return fvar_name(a) == fvar_name(b);
+        case expr_kind::Sort: return sort_level(a) == sort_level(b);
+        default: break;
+        }
+        if (!root && check_cache(a, b))
             return true;
         /*
            We increase the number of heartbeats here because some code (e.g., `simp`) may spend a lot of time comparing
@@ -78,6 +62,10 @@ class expr_eq_fn {
         lean_inc_heartbeat();
         switch (a.kind()) {
         case expr_kind::BVar:
+        case expr_kind::Lit:
+        case expr_kind::MVar:
+        case expr_kind::FVar:
+        case expr_kind::Sort:
             lean_unreachable(); // LCOV_EXCL_LINE
         case expr_kind::MData:
             return
@@ -88,16 +76,10 @@ class expr_eq_fn {
                 apply(proj_expr(a), proj_expr(b)) &&
                 proj_sname(a) == proj_sname(b) &&
                 proj_idx(a) == proj_idx(b);
-        case expr_kind::Lit:
-            return lit_value(a) == lit_value(b);
         case expr_kind::Const:
             return
                 const_name(a) == const_name(b) &&
                 compare(const_levels(a), const_levels(b), [](level const & l1, level const & l2) { return l1 == l2; });
-        case expr_kind::MVar:
-            return mvar_name(a) == mvar_name(b);
-        case expr_kind::FVar:
-            return fvar_name(a) == fvar_name(b);
         case expr_kind::App:
             check_system();
             return
@@ -117,15 +99,13 @@ class expr_eq_fn {
                 apply(let_value(a), let_value(b)) &&
                 apply(let_body(a), let_body(b)) &&
                 (!CompareBinderInfo || let_name(a) == let_name(b));
-        case expr_kind::Sort:
-            return sort_level(a) == sort_level(b);
         }
         lean_unreachable(); // LCOV_EXCL_LINE
     }
 public:
-    expr_eq_fn():m_cache(get_eq_cache()) {}
-    ~expr_eq_fn() { m_cache.clear(); }
-    bool operator()(expr const & a, expr const & b) { return apply(a, b); }
+    expr_eq_fn() {}
+    ~expr_eq_fn() { if (m_cache) delete m_cache; }
+    bool operator()(expr const & a, expr const & b) { return apply(a, b, true); }
 };
 
 bool is_equal(expr const & a, expr const & b) {

src/kernel/replace_fn.cpp

@@ -14,7 +14,7 @@ namespace lean {
 class replace_rec_fn {
     struct key_hasher {
         std::size_t operator()(std::pair<lean_object *, unsigned> const & p) const {
-            return hash((size_t)p.first, p.second);
+            return hash((size_t)p.first >> 3, p.second);
         }
     };
     std::unordered_map<std::pair<lean_object *, unsigned>, expr, key_hasher> m_cache;

src/lake/Lake/Build/Module.lean

@@ -31,6 +31,9 @@ Recursively parse the Lean files of a module and its imports
 building an `Array` product of its direct local imports.
 -/
 def Module.recParseImports (mod : Module) : FetchM (Array Module) := do
+  -- Make sure we fail reading the file independently of the FS case sensitivity
+  unless (← Lean.moduleExists mod.lib.srcDir "lean" mod.name) do
+    error s!"module source file not found: {mod.leanFile}"
   let contents ← IO.FS.readFile mod.leanFile
   let imports ← Lean.parseImports' contents mod.leanFile.toString
   let mods ← imports.foldlM (init := OrdModuleSet.empty) fun set imp =>

src/runtime/sharecommon.cpp

@@ -4,11 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <vector>
 #include <cstring>
-#include <unordered_map>
-#include <unordered_set>
-#include "runtime/object.h"
+#include "runtime/sharecommon.h"
 #include "runtime/hash.h"
 
 namespace lean {
@@ -271,176 +268,168 @@ extern "C" LEAN_EXPORT obj_res lean_state_sharecommon(b_obj_arg tc, obj_arg s, o
     return sharecommon_fn(tc, s)(a);
 }
 
+
 /*
-A faster version of `sharecommon_fn` which only uses a local state.
-It optimizes the number of RC operations, the strategy for caching results,
-and uses C++ hashmap.
+  We do not increment reference counters when inserting Lean objects at `m_cache` and `m_set`.
+  This is correct because
+  - The domain of `m_cache` contains only sub-objects of `lean_sharecommon_quick` parameter,
+    and we know the object referenced by this parameter will remain alive.
+  - The range of `m_cache` contains only new objects that have been maxed shared, and these
+    objects will be are sub-objects of the object returned by `lean_sharecommon_quick`.
+  - `m_set` is like the range of `m_cache`.
 */
-class sharecommon_quick_fn {
-    struct set_hash {
-        std::size_t operator()(lean_object * o) const { return lean_sharecommon_hash(o); }
-    };
-    struct set_eq {
-        std::size_t operator()(lean_object * o1, lean_object * o2) const { return lean_sharecommon_eq(o1, o2); }
-    };
 
-    /*
-    We use `m_cache` to ensure we do **not** traverse a DAG as a tree.
-    We use pointer equality for this collection.
-    */
-    std::unordered_map<lean_object *, lean_object *> m_cache;
-    /* Set of maximally shared terms. AKA hash-consing table. */
-    std::unordered_set<lean_object *, set_hash, set_eq> m_set;
-
-    /*
-      We do not increment reference counters when inserting Lean objects at `m_cache` and `m_set`.
-      This is correct because
-      - The domain of `m_cache` contains only sub-objects of `lean_sharecommon_quick` parameter,
-        and we know the object referenced by this parameter will remain alive.
-      - The range of `m_cache` contains only new objects that have been maxed shared, and these
-        objects will be are sub-objects of the object returned by `lean_sharecommon_quick`.
-      - `m_set` is like the range of `m_cache`.
-    */
-
-    lean_object * check_cache(lean_object * a) {
-        if (!lean_is_exclusive(a)) {
-            // We only check the cache if `a` is a shared object
-            auto it = m_cache.find(a);
-            if (it != m_cache.end()) {
-                // All objects stored in the range of `m_cache` are single threaded.
-                lean_assert(lean_is_st(it->second));
-                // We increment the reference counter because this object
-                // will be returned by `lean_sharecommon_quick` or stored into a new object.
-                it->second->m_rc++;
-                return it->second;
+lean_object * sharecommon_quick_fn::check_cache(lean_object * a) {
+    if (!lean_is_exclusive(a)) {
+        // We only check the cache if `a` is a shared object
+        auto it = m_cache.find(a);
+        if (it != m_cache.end()) {
+            // All objects stored in the range of `m_cache` are single threaded.
+            lean_assert(lean_is_st(it->second));
+            // We increment the reference counter because this object
+            // will be returned by `lean_sharecommon_quick` or stored into a new object.
+            it->second->m_rc++;
+            return it->second;
+        }
+        if (m_check_set) {
+            auto it = m_set.find(a);
+            if (it != m_set.end()) {
+                lean_object * result = *it;
+                lean_assert(lean_is_st(result));
+                result->m_rc++;
+                return result;
             }
         }
-        return nullptr;
     }
+    return nullptr;
+}
 
-    /*
-    `new_a` is a new object that is equal to `a`, but its subobjects are maximally shared.
-    */
-    lean_object * save(lean_object * a, lean_object * new_a) {
-        lean_assert(lean_is_st(new_a));
-        lean_assert(new_a->m_rc == 1);
-        auto it = m_set.find(new_a);
-        lean_object * result;
-        if (it == m_set.end()) {
-            // `new_a` is a new object
-            m_set.insert(new_a);
-            result = new_a;
-        } else {
-            // We already have a maximally shared object that is equal to `new_a`
-            result = *it;
-            DEBUG_CODE({
-                    if (lean_is_ctor(new_a)) {
-                        lean_assert(lean_is_ctor(result));
-                        unsigned num_objs = lean_ctor_num_objs(new_a);
-                        lean_assert(lean_ctor_num_objs(result) == num_objs);
-                        for (unsigned i = 0; i < num_objs; i++) {
-                            lean_assert(lean_ctor_get(result, i) == lean_ctor_get(new_a, i));
-                        }
+/*
+  `new_a` is a new object that is equal to `a`, but its subobjects are maximally shared.
+*/
+lean_object * sharecommon_quick_fn::save(lean_object * a, lean_object * new_a) {
+    lean_assert(lean_is_st(new_a));
+    lean_assert(new_a->m_rc == 1);
+    auto it = m_set.find(new_a);
+    lean_object * result;
+    if (it == m_set.end()) {
+        // `new_a` is a new object
+        m_set.insert(new_a);
+        result = new_a;
+    } else {
+        // We already have a maximally shared object that is equal to `new_a`
+        result = *it;
+        DEBUG_CODE({
+                if (lean_is_ctor(new_a)) {
+                    lean_assert(lean_is_ctor(result));
+                    unsigned num_objs = lean_ctor_num_objs(new_a);
+                    lean_assert(lean_ctor_num_objs(result) == num_objs);
+                    for (unsigned i = 0; i < num_objs; i++) {
+                        lean_assert(lean_ctor_get(result, i) == lean_ctor_get(new_a, i));
                     }
-                });
-            lean_dec_ref(new_a); // delete `new_a`
-            // All objects in `m_set` are single threaded.
-            lean_assert(lean_is_st(result));
-            result->m_rc++;
-            lean_assert(result->m_rc > 1);
-        }
-        if (!lean_is_exclusive(a)) {
-            // We only cache the result if `a` is a shared object.
-            m_cache.insert(std::make_pair(a, result));
-        }
-        lean_assert(result == new_a || result->m_rc > 1);
-        lean_assert(result != new_a || result->m_rc == 1);
-        return result;
+                }
+            });
+        lean_dec_ref(new_a); // delete `new_a`
+        // All objects in `m_set` are single threaded.
+        lean_assert(lean_is_st(result));
+        result->m_rc++;
+        lean_assert(result->m_rc > 1);
     }
+    if (!lean_is_exclusive(a)) {
+        // We only cache the result if `a` is a shared object.
+        m_cache.insert(std::make_pair(a, result));
+    }
+    lean_assert(result == new_a || result->m_rc > 1);
+    lean_assert(result != new_a || result->m_rc == 1);
+    return result;
+}
 
-    // `sarray` and `string`
-    lean_object * visit_terminal(lean_object * a) {
-        auto it = m_set.find(a);
-        if (it == m_set.end()) {
-            m_set.insert(a);
-        } else {
-            a = *it;
-        }
-        lean_inc_ref(a);
+// `sarray` and `string`
+lean_object * sharecommon_quick_fn::visit_terminal(lean_object * a) {
+    auto it = m_set.find(a);
+    if (it == m_set.end()) {
+        m_set.insert(a);
+    } else {
+        a = *it;
+    }
+    lean_inc_ref(a);
+    return a;
+}
+
+lean_object * sharecommon_quick_fn::visit_array(lean_object * a) {
+    lean_object * r = check_cache(a);
+    if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
+
+    size_t sz = array_size(a);
+    lean_array_object * new_a = (lean_array_object*)lean_alloc_array(sz, sz);
+    for (size_t i = 0; i < sz; i++) {
+        lean_array_set_core((lean_object*)new_a, i, visit(lean_array_get_core(a, i)));
+    }
+    return save(a, (lean_object*)new_a);
+}
+
+lean_object * sharecommon_quick_fn::visit_ctor(lean_object * a) {
+    lean_object * r = check_cache(a);
+    if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
+    unsigned num_objs      = lean_ctor_num_objs(a);
+    unsigned tag           = lean_ptr_tag(a);
+    unsigned sz            = lean_object_byte_size(a);
+    unsigned scalar_offset = sizeof(lean_object) + num_objs*sizeof(void*);
+    unsigned scalar_sz     = sz - scalar_offset;
+    lean_object * new_a    = lean_alloc_ctor(tag, num_objs, scalar_sz);
+    for (unsigned i = 0; i < num_objs; i++) {
+        lean_ctor_set(new_a, i, visit(lean_ctor_get(a, i)));
+    }
+    if (scalar_sz > 0) {
+        memcpy(reinterpret_cast<char*>(new_a) + scalar_offset, reinterpret_cast<char*>(a) + scalar_offset, scalar_sz);
+    }
+    return save(a, new_a);
+}
+
+/*
+**TODO:** We did not implement stack overflow detection.
+We claim it is not needed in the current uses of `shareCommon'`.
+If this becomes an issue, we can use the following approach to address the issue without
+affecting the performance.
+- Add an extra `depth` parameter.
+- In `operator()`, estimate the maximum depth based on the remaining stack space. See `check_stack`.
+- If the limit is reached, simply return `a`.
+*/
+lean_object * sharecommon_quick_fn::visit(lean_object * a) {
+    if (lean_is_scalar(a)) {
         return a;
     }
-
-    lean_object * visit_array(lean_object * a) {
-        lean_object * r = check_cache(a);
-        if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
-
-        size_t sz = array_size(a);
-        lean_array_object * new_a = (lean_array_object*)lean_alloc_array(sz, sz);
-        for (size_t i = 0; i < sz; i++) {
-            lean_array_set_core((lean_object*)new_a, i, visit(lean_array_get_core(a, i)));
-        }
-        return save(a, (lean_object*)new_a);
-    }
-
-    lean_object * visit_ctor(lean_object * a) {
-        lean_object * r = check_cache(a);
-        if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
-        unsigned num_objs      = lean_ctor_num_objs(a);
-        unsigned tag           = lean_ptr_tag(a);
-        unsigned sz            = lean_object_byte_size(a);
-        unsigned scalar_offset = sizeof(lean_object) + num_objs*sizeof(void*);
-        unsigned scalar_sz     = sz - scalar_offset;
-        lean_object * new_a    = lean_alloc_ctor(tag, num_objs, scalar_sz);
-        for (unsigned i = 0; i < num_objs; i++) {
-            lean_ctor_set(new_a, i, visit(lean_ctor_get(a, i)));
-        }
-        if (scalar_sz > 0) {
-            memcpy(reinterpret_cast<char*>(new_a) + scalar_offset, reinterpret_cast<char*>(a) + scalar_offset, scalar_sz);
-        }
-        return save(a, new_a);
-    }
-
-public:
-
+    switch (lean_ptr_tag(a)) {
     /*
-    **TODO:** We did not implement stack overflow detection.
-    We claim it is not needed in the current uses of `shareCommon'`.
-    If this becomes an issue, we can use the following approach to address the issue without
-    affecting the performance.
-    - Add an extra `depth` parameter.
-    - In `operator()`, estimate the maximum depth based on the remaining stack space. See `check_stack`.
-    - If the limit is reached, simply return `a`.
+      Similarly to `sharecommon_fn`, we only maximally share arrays, scalar arrays, strings, and
+      constructor objects.
     */
-    lean_object * visit(lean_object * a) {
-        if (lean_is_scalar(a)) {
-            return a;
-        }
-        switch (lean_ptr_tag(a)) {
-        /*
-        Similarly to `sharecommon_fn`, we only maximally share arrays, scalar arrays, strings, and
-        constructor objects.
-        */
-        case LeanMPZ:             lean_inc_ref(a); return a;
-        case LeanClosure:         lean_inc_ref(a); return a;
-        case LeanThunk:           lean_inc_ref(a); return a;
-        case LeanTask:            lean_inc_ref(a); return a;
-        case LeanRef:             lean_inc_ref(a); return a;
-        case LeanExternal:        lean_inc_ref(a); return a;
-        case LeanReserved:        lean_inc_ref(a); return a;
-        case LeanScalarArray:     return visit_terminal(a);
-        case LeanString:          return visit_terminal(a);
-        case LeanArray:           return visit_array(a);
-        default:                  return visit_ctor(a);
-        }
+    case LeanMPZ:             lean_inc_ref(a); return a;
+    case LeanClosure:         lean_inc_ref(a); return a;
+    case LeanThunk:           lean_inc_ref(a); return a;
+    case LeanTask:            lean_inc_ref(a); return a;
+    case LeanRef:             lean_inc_ref(a); return a;
+    case LeanExternal:        lean_inc_ref(a); return a;
+    case LeanReserved:        lean_inc_ref(a); return a;
+    case LeanScalarArray:     return visit_terminal(a);
+    case LeanString:          return visit_terminal(a);
+    case LeanArray:           return visit_array(a);
+    default:                  return visit_ctor(a);
     }
-
-    lean_object * operator()(lean_object * a) {
-        return visit(a);
-    }
-};
+}
 
 // def ShareCommon.shareCommon' (a : A) : A := a
 extern "C" LEAN_EXPORT obj_res lean_sharecommon_quick(obj_arg a) {
     return sharecommon_quick_fn()(a);
 }
+
+lean_object * sharecommon_persistent_fn::operator()(lean_object * e) {
+    lean_object * r = check_cache(e);
+    if (r != nullptr)
+        return r;
+    m_saved.push_back(object_ref(e, true));
+    r = visit(e);
+    m_saved.push_back(object_ref(r, true));
+    return r;
+}
 };

src/runtime/sharecommon.h

@@ -0,0 +1,71 @@
+/*
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <vector>
+#include <unordered_map>
+#include <unordered_set>
+#include "runtime/object_ref.h"
+
+namespace lean {
+extern "C" LEAN_EXPORT uint8 lean_sharecommon_eq(b_obj_arg o1, b_obj_arg o2);
+extern "C" LEAN_EXPORT uint64_t lean_sharecommon_hash(b_obj_arg o);
+
+/*
+A faster version of `sharecommon_fn` which only uses a local state.
+It optimizes the number of RC operations, the strategy for caching results,
+and uses C++ hashmap.
+*/
+class sharecommon_quick_fn {
+protected:
+    struct set_hash {
+        std::size_t operator()(lean_object * o) const { return lean_sharecommon_hash(o); }
+    };
+    struct set_eq {
+        std::size_t operator()(lean_object * o1, lean_object * o2) const { return lean_sharecommon_eq(o1, o2); }
+    };
+
+    /*
+    We use `m_cache` to ensure we do **not** traverse a DAG as a tree.
+    We use pointer equality for this collection.
+    */
+    std::unordered_map<lean_object *, lean_object *> m_cache;
+    /* Set of maximally shared terms. AKA hash-consing table. */
+    std::unordered_set<lean_object *, set_hash, set_eq> m_set;
+    /*
+    If `true`, `check_cache` will also check `m_set`.
+    This is useful when the input term may contain terms that have already
+    been hashconsed.
+    */
+    bool m_check_set;
+
+    lean_object * check_cache(lean_object * a);
+    lean_object * save(lean_object * a, lean_object * new_a);
+    lean_object * visit_terminal(lean_object * a);
+    lean_object * visit_array(lean_object * a);
+    lean_object * visit_ctor(lean_object * a);
+    lean_object * visit(lean_object * a);
+public:
+    sharecommon_quick_fn(bool s = false):m_check_set(s) {}
+    void set_check_set(bool f) { m_check_set = f; }
+    lean_object * operator()(lean_object * a) {
+        return visit(a);
+    }
+};
+
+/*
+Similar to `sharecommon_quick_fn`, but we save the entry points and result values to ensure
+they are not deleted.
+*/
+class sharecommon_persistent_fn : private sharecommon_quick_fn {
+    std::vector<object_ref> m_saved;
+public:
+    sharecommon_persistent_fn(bool s = false):sharecommon_quick_fn(s) {}
+    void set_check_set(bool f) { m_check_set = f; }
+    lean_object * operator()(lean_object * e);
+};
+
+};

tests/lean/1007.lean.expected.out

@@ -8,4 +8,4 @@
 1007.lean:39:4-39:7: warning: declaration uses 'sorry'
 1007.lean:56:64-56:78: error: failed to synthesize
   IsLin fun x => sum fun i => norm x
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/1102.lean.expected.out

@@ -1,3 +1,3 @@
 1102.lean:22:35-22:49: error: failed to synthesize
   DVR 1
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/2040.lean.expected.out

@@ -1,12 +1,12 @@
 2040.lean:8:8-8:13: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 2040.lean:14:8-14:13: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 2040.lean:20:8-20:13: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 2040.lean:18:2-20:22: error: type mismatch
   trans (sorryAx (a = 37)) (sorryAx (37 = 2 ^ n))
 has type

tests/lean/2220.lean.expected.out

@@ -8,11 +8,11 @@
 @HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
 2220.lean:25:19-25:24: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 @HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
   (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
 2220.lean:26:12-26:17: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 @HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
   (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int

tests/lean/2273.lean.expected.out

@@ -1,3 +1,3 @@
 2273.lean:9:8-9:14: error: failed to synthesize
   P 37
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/297.lean.expected.out

@@ -3,4 +3,4 @@
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   Sort ?u
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/386.lean.expected.out

@@ -1,3 +1,3 @@
 386.lean:9:2-9:46: error: failed to synthesize
   Fintype ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/448.lean.expected.out

@@ -1,3 +1,3 @@
 448.lean:21:2-23:20: error: failed to synthesize
   MonadExceptOf IO.Error M
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/attrCmd.lean.expected.out

@@ -1,3 +1,3 @@
 attrCmd.lean:6:0-6:6: error: failed to synthesize
   Pure M
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/calcErrors.lean.expected.out

@@ -12,7 +12,7 @@ calcErrors.lean:24:8-24:11: error: invalid 'calc' step, relation expected
   p a
 calcErrors.lean:31:8-31:13: error: invalid 'calc' step, failed to synthesize `Trans` instance
   Trans p p ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 calcErrors.lean:41:7-41:12: error: invalid 'calc' step, left-hand-side is
   γ : Sort u_1
 previous right-hand-side is

tests/lean/defInst.lean.expected.out

@@ -1,7 +1,7 @@
 [4, 5, 6]
 defInst.lean:8:26-8:32: error: failed to synthesize
   BEq Foo
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 fun x y => sorryAx (?m x y) true : (x y : Foo) → ?m x y
 [4, 5, 6]
 fun x y => x == y : Foo → Foo → Bool

tests/lean/defaultInstance.lean.expected.out

@@ -1,5 +1,5 @@
 defaultInstance.lean:20:20-20:23: error: failed to synthesize
   Foo Bool (?m x)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 defaultInstance.lean:22:35-22:38: error: typeclass instance problem is stuck, it is often due to metavariables
   Foo Bool (?m x)

tests/lean/eagerUnfoldingIssue.lean.expected.out

@@ -1,6 +1,6 @@
 eagerUnfoldingIssue.lean:6:2-6:17: error: failed to synthesize
   MonadLog (StateM Nat)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 eagerUnfoldingIssue.lean:12:2-12:17: error: failed to synthesize
   MonadLog (StateM Nat)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/eraseInsts.lean.expected.out

@@ -1,3 +1,3 @@
 eraseInsts.lean:12:22-12:27: error: failed to synthesize
   HAdd Foo Foo ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/forErrors.lean.expected.out

@@ -1,3 +1,3 @@
 forErrors.lean:3:29-3:30: error: failed to synthesize
   ToStream α ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/kernelMVarBug.lean.expected.out

@@ -1,3 +1,3 @@
 kernelMVarBug.lean:5:15-5:20: error: failed to synthesize
   HAdd α α α
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/macroStack.lean.expected.out

@@ -11,7 +11,7 @@ while expanding
 macroStack.lean:11:9-11:15: error: invalid use of `(<- ...)`, must be nested inside a 'do' expression
 macroStack.lean:17:0-17:6: error: failed to synthesize
   HAdd Nat String ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 with resulting expansion
   binop% HAdd.hAdd✝ (x + x✝) x✝¹
 while expanding

tests/lean/macroSwizzle.lean.expected.out

@@ -1,6 +1,6 @@
 macroSwizzle.lean:4:7-4:23: error: failed to synthesize
   HAdd Bool String ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 macroSwizzle.lean:6:7-6:10: error: application type mismatch
   Nat.succ "x"
 argument

tests/lean/openScoped.lean.expected.out

@@ -1,7 +1,7 @@
 openScoped.lean:1:7-1:14: error: unknown identifier 'epsilon'
 openScoped.lean:4:2-4:24: error: failed to synthesize
   Decidable (f = g)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 Classical.epsilon.{u} {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
 openScoped.lean:15:7-15:14: error: unknown identifier 'epsilon'
 openScoped.lean:20:7-20:14: error: unknown identifier 'epsilon'

tests/lean/prvCtor.lean.expected.out

@@ -7,7 +7,7 @@ prvCtor.lean:27:7-27:8: error: unknown identifier 'a'
 prvCtor.lean:29:25-29:27: error: overloaded, errors 
   failed to synthesize
     EmptyCollection (Name "hello")
-  use `set_option diagnostics true` to get diagnostic information
+  Additional diagnostic information may be available using the `set_option diagnostics true` command.
   
   invalid {...} notation, constructor for `Name` is marked as private
 prvCtor.lean:31:25-31:34: error: invalid ⟨...⟩ notation, constructor for `Name` is marked as private

tests/lean/run/1163.lean

@@ -16,7 +16,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   Bool
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 def x : Bool := 0
@@ -29,7 +29,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   Bool
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 theorem result4 : False := by -- Does not generate a `sorry` warning because there is an error

tests/lean/run/3313.lean

@@ -41,7 +41,6 @@ info: [type_class] max synth pending failures (maxSynthPendingDepth: 1), use `se
 ---
 error: failed to synthesize
   HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R)))
-use `set_option diagnostics true` to get diagnostic information
 -/
 #guard_msgs in
 set_option diagnostics true in

tests/lean/run/345.lean

@@ -6,7 +6,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Sort _
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 axiom bla : 1
@@ -17,7 +17,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Sort _
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 structure Foo where
@@ -29,7 +29,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Sort _
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 inductive Bla (x : 1) : Type

tests/lean/run/3554.lean

@@ -5,8 +5,12 @@ def foo : Nat → Nat
 set_option debug.moduleNameAtTimeout false
 /--
 error: (deterministic) timeout, maximum number of heartbeats (100) has been reached
-use `set_option maxHeartbeats <num>` to set the limit
-use `set_option diagnostics true` to get diagnostic information
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout, maximum number of heartbeats (100) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 set_option maxHeartbeats 100 in

tests/lean/run/3996.lean

@@ -17,7 +17,7 @@ instance instB10000 : B 10000 where
 /--
 error: failed to synthesize
   A
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #synth A -- should fail quickly

tests/lean/run/4203.lean

@@ -14,7 +14,7 @@ def IsGood [DecidableEq dOut] [DecidableEq dOut₂] (Λ : Mappish dIn dOut) (Λ
 /--
 error: failed to synthesize
   Fintype v
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 def MappishOrder [DecidableEq dIn] : Preorder

tests/lean/run/4365.lean

@@ -37,7 +37,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   String
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #check (1 : String)
@@ -48,7 +48,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Bool
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #check (1 : Bool)
@@ -59,7 +59,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Bool → Nat
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #check (1 : Bool → Nat)
@@ -70,7 +70,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   String
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 def foo : String :=

tests/lean/run/by_cases.lean

@@ -13,7 +13,7 @@ example (p : Prop) : True := by
 /--
 error: failed to synthesize
   Decidable p
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 example (p : Prop) : True := by

tests/lean/run/diagnosticsMsgOptional.lean

@@ -0,0 +1,20 @@
+/-!
+# Mentioning `set_option diagnostics true` depends on it not already being set
+-/
+
+/--
+error: failed to synthesize
+  Coe Nat Int
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+#synth Coe Nat Int
+
+set_option diagnostics true
+
+/--
+error: failed to synthesize
+  Coe Nat Int
+-/
+#guard_msgs in
+#synth Coe Nat Int

tests/lean/run/guard_msgs.lean

@@ -51,7 +51,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `22` cannot be used in a context where the expected type is
   α
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs(error) in
 example : α := 22
@@ -107,7 +107,7 @@ Lax whitespace
 /--
 error: failed to synthesize
   DecidableEq (Nat → Nat)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs (whitespace := lax) in
 #synth DecidableEq (Nat → Nat)
@@ -115,7 +115,7 @@ use `set_option diagnostics true` to get diagnostic information
 /--
 error: failed to synthesize
   DecidableEq (Nat → Nat)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs (whitespace := lax) in
 #synth DecidableEq (Nat → Nat)

tests/lean/run/isDefEqProjIssue.lean

@@ -52,8 +52,36 @@ where
 
 /--
 error: (deterministic) timeout at `whnf`, maximum number of heartbeats (400) has been reached
-use `set_option maxHeartbeats <num>` to set the limit
-use `set_option diagnostics true` to get diagnostic information
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout at `elaborator`, maximum number of heartbeats (400) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout at `elaborator`, maximum number of heartbeats (400) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout at `whnf`, maximum number of heartbeats (400) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 set_option backward.isDefEq.lazyWhnfCore false in

tests/lean/run/simprocNat.lean

@@ -1,5 +1,13 @@
 variable (a b : Nat)
 
+/- bitwise operation tests -/
+
+#check_simp (3 : Nat) &&& (1 : Nat) ~> 1
+#check_simp (3 : Nat) ^^^ (1 : Nat) ~> 2
+#check_simp (2 : Nat) ||| (1 : Nat) ~> 3
+#check_simp (3 : Nat) <<< (2 : Nat) ~> 12
+#check_simp (3 : Nat) >>> (1 : Nat) ~> 1
+
 /- subtract diff tests -/
 
 #check_simp (1000 : Nat) - 400 ~> 600

tests/lean/sanitychecks.lean.expected.out

@@ -9,7 +9,7 @@ sanitychecks.lean:4:8-4:32: error: 'partial' theorems are not allowed, 'partial'
 sanitychecks.lean:7:7-7:31: error: 'unsafe' theorems are not allowed
 sanitychecks.lean:10:0-10:23: error: failed to synthesize
   Inhabited False
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 sanitychecks.lean:18:12-18:20: error: invalid use of 'partial', 'Foo.unsound3' is not a function
   False
 sanitychecks.lean:20:0-20:54: error: failed to compile partial definition 'Foo.unsound4', failed to show that type is inhabited and non empty

tests/lean/scopedLocalInsts.lean.expected.out

@@ -1,12 +1,12 @@
 scopedLocalInsts.lean:12:6-12:39: error: failed to synthesize
   ToString A
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 "A.mk 10 20"
 scopedLocalInsts.lean:21:6-21:39: error: failed to synthesize
   ToString A
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 "{ x := 10, y := 20 }"
 scopedLocalInsts.lean:32:6-32:39: error: failed to synthesize
   ToString A
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 "A.mk 10 20"

tests/lean/semicolonOrLinebreak.lean.expected.out

@@ -7,4 +7,4 @@ term has type
   Nat
 semicolonOrLinebreak.lean:20:2-20:9: error: failed to synthesize
   Singleton ?m Point
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/setLit.lean.expected.out

@@ -1,12 +1,12 @@
 setLit.lean:22:19-22:21: error: overloaded, errors 
   failed to synthesize
     EmptyCollection String
-  use `set_option diagnostics true` to get diagnostic information
+  Additional diagnostic information may be available using the `set_option diagnostics true` command.
   
   fields missing: 'data'
 setLit.lean:24:31-24:38: error: overloaded, errors 
   failed to synthesize
     Singleton Nat String
-  use `set_option diagnostics true` to get diagnostic information
+  Additional diagnostic information may be available using the `set_option diagnostics true` command.
   
   24:33 'val' is not a field of structure 'String'

tests/lean/tcloop.lean.expected.out

@@ -1,6 +1,3 @@
-tcloop.lean:14:2-14:15: error: failed to synthesize
-  B Nat
-(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached
-use `set_option synthInstance.maxHeartbeats <num>` to set the limit
-use `set_option diagnostics true` to get diagnostic information
-use `set_option diagnostics true` to get diagnostic information
+tcloop.lean:14:2-14:15: error: (deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached
+Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/typeOf.lean.expected.out

@@ -1,9 +1,9 @@
 typeOf.lean:11:22-11:25: error: failed to synthesize
   HAdd Nat Nat Bool
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 typeOf.lean:12:0-12:5: error: failed to synthesize
   HAdd Bool Nat Nat
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 typeOf.lean:20:56-20:62: error: invalid reassignment, term has type
   Bool : Type
 but is expected to have type

tests/pkg/import-case/.gitignore

@@ -0,0 +1 @@
+/.lake

tests/pkg/import-case/ImportCase.lean

@@ -0,0 +1,2 @@
+-- should *not* be accepted on any platform
+import ImportCase.basic

tests/pkg/import-case/ImportCase/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

tests/pkg/import-case/lakefile.toml

@@ -0,0 +1,5 @@
+name = "«import-case»"
+defaultTargets = ["ImportCase"]
+
+[[lean_lib]]
+name = "ImportCase"

tests/pkg/import-case/test.sh

@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+rm -rf .lake/build
+(lake build 2>&1 && exit 1 || true) | grep --color -F 'module source file not found'