chore: update to nightly-2025-06-19

Manual/BasicTypes/BitVec.lean

@@ -297,13 +297,13 @@ These operations treat bitvectors as sequences of bits, rather than as encodings
 
 {docstring BitVec.getMsbD}
 
-{docstring BitVec.getMsb'}
+{docstring BitVec.getMsb}
 
 {docstring BitVec.getMsb?}
 
 {docstring BitVec.getLsbD}
 
-{docstring BitVec.getLsb'}
+{docstring BitVec.getLsb}
 
 {docstring BitVec.getLsb?}
 

Manual/BasicTypes/Maps/TreeMap.lean

@@ -109,10 +109,6 @@ The declarations in this section should be imported using `import Std.TreeMap`.
 
 {docstring Std.TreeMap.getEntryLTD}
 
-{docstring Std.TreeMap.getGE}
-
-{docstring Std.TreeMap.getGT}
-
 {docstring Std.TreeMap.getKeyGE}
 
 {docstring Std.TreeMap.getKeyGE!}
@@ -145,10 +141,6 @@ The declarations in this section should be imported using `import Std.TreeMap`.
 
 {docstring Std.TreeMap.getKeyLTD}
 
-{docstring Std.TreeMap.getLE}
-
-{docstring Std.TreeMap.getLT}
-
 {docstring Std.TreeMap.keyAtIdx}
 
 {docstring Std.TreeMap.keyAtIdx!}

Manual/BasicTypes/Maps/TreeSet.lean

@@ -56,24 +56,32 @@ tag := "TreeSet"
 
 {docstring Std.TreeSet.atIdxD}
 
+{docstring Std.TreeSet.getGE}
+
 {docstring Std.TreeSet.getGE!}
 
 {docstring Std.TreeSet.getGE?}
 
 {docstring Std.TreeSet.getGED}
 
+{docstring Std.TreeSet.getGT}
+
 {docstring Std.TreeSet.getGT!}
 
 {docstring Std.TreeSet.getGT?}
 
 {docstring Std.TreeSet.getGTD}
 
+{docstring Std.TreeSet.getLE}
+
 {docstring Std.TreeSet.getLE!}
 
 {docstring Std.TreeSet.getLE?}
 
 {docstring Std.TreeSet.getLED}
 
+{docstring Std.TreeSet.getLT}
+
 {docstring Std.TreeSet.getLT!}
 
 {docstring Std.TreeSet.getLT?}

Manual/BuildTools/Lake.lean

@@ -350,9 +350,10 @@ Executables have a single `exe` facet that consists of the executable binary.
 ```lean (show := false)
 -- Always keep this in sync with the description below. It ensures that the list is complete.
 /--
-info: #[`module.bc, `module.bc.o, `module.c, `module.c.o, `module.c.o.export, `module.c.o.noexport, `module.deps,
-  `module.dynlib, `module.ilean, `module.imports, `module.leanArts, `module.o, `module.o.export, `module.o.noexport,
-  `module.olean, `module.precompileImports, `module.transImports]
+info: #[`module.allImports, `module.bc, `module.bc.o, `module.c, `module.c.o, `module.c.o.export, `module.c.o.noexport,
+  `module.deps, `module.dynlib, `module.header, `module.ilean, `module.imports, `module.leanArts, `module.o,
+  `module.o.export, `module.o.noexport, `module.olean, `module.olean.private, `module.olean.server,
+  `module.precompileImports, `module.setup, `module.src, `module.transImports]
 -/
 #guard_msgs in
 #eval Lake.initModuleFacetConfigs.toList.toArray.map (·.1) |>.qsort (·.toString < ·.toString)
@@ -363,19 +364,27 @@ The facets available for modules are:
 
 : `leanArts` (default)
 
- The module's Lean artifacts (`*.olean`, `*.ilean`, `*.c` files)
+ The module's Lean artifacts (`*.olean`, `*.ilean`, `*.c` files).
+
+: `src`
+
+  The module's Lean source file.
 
 : `deps`
 
   The module's dependencies (e.g., imports or shared libraries).
 
 : `olean`
 
- The module's {tech}[`.olean` file]
+ The module's {tech}[`.olean` file]. {TODO}[Once module system lands fully, add docs for `olean.private` and `olean.server`]
 
 : `ilean`
 
- The module's `.ilean` file, which is metadata used by the Lean language server
+ The module's `.ilean` file, which is metadata used by the Lean language server.
+
+: `header`
+
+  The parsed module header of the module's source file.
 
 : `imports`
 
@@ -389,13 +398,22 @@ The facets available for modules are:
 
   The transitive imports of the Lean module, as {tech}[`.olean` files].
 
+: `allImports`
+
+  Both the immediate and transitive imports of the Lean module.
+
+: `setup`
+
+  All of a module's dependencies: transitive local imports and shared libraries to be loaded with `--load-dynlib`.
+  Returns the list of shared libraries to load along with their search path.
+
 : `c`
 
- The C file produced by the Lean compiler
+ The C file produced by the Lean compiler.
 
 : `bc`
 
- LLVM bitcode file, produced by the Lean compiler
+ LLVM bitcode file, produced by the Lean compiler.
 
 : `c.o`
 
@@ -411,15 +429,15 @@ The facets available for modules are:
 
 : `bc.o`
 
- The compiled object file, produced from the LLVM bitcode file
+ The compiled object file, produced from the LLVM bitcode file.
 
 : `o`
 
- The compiled object file for the configured backend
+ The compiled object file for the configured backend.
 
 : `dynlib`
 
-  A shared library (e.g., for the Lean option `--load-dynlib`){TODO}[Document Lean command line options, and cross-reference from here]
+  A shared library (e.g., for the Lean option `--load-dynlib`){TODO}[Document Lean command line options, and cross-reference from here].
 
 :::
 

Manual/Elaboration.lean

@@ -185,7 +185,7 @@ example (b : B) : ⟨b.1, b.2⟩ = b := rfl
 error: type mismatch
   rfl
 has type
-  ?m.854 = ?m.854 : Prop
+  ?m.858 = ?m.858 : Prop
 but is expected to have type
   e1 = e2 : Prop
 -/

Manual/Interaction.lean

@@ -362,7 +362,7 @@ def intersperse (x : α) : List α → List α
 ```
 ```leanOutput intersperse_eqns
 equations:
-theorem intersperse.eq_1.{u_1} : ∀ {α : Type u_1} (x y z : α) (zs : List α),
+@[defeq] theorem intersperse.eq_1.{u_1} : ∀ {α : Type u_1} (x y z : α) (zs : List α),
   intersperse x (y :: z :: zs) = y :: x :: intersperse x (z :: zs)
 theorem intersperse.eq_2.{u_1} : ∀ {α : Type u_1} (x : α) (x_1 : List α),
   (∀ (y z : α) (zs : List α), x_1 = y :: z :: zs → False) → intersperse x x_1 = x_1

Manual/Meta/LakeToml.lean

@@ -470,7 +470,7 @@ def asTable (humanName : String) (n : Name) (skip : List Name := []) : DocElabM
                 else if type.isConstOf ``Lake.BuildType then some (.oneOf buildTypes)
                 else if type.isConstOf ``Lake.StdVer then some .version
                 else if type.isConstOf ``Lake.StrPat then some (.other ``Lake.StrPat "string pattern" none)
-                else if type.isAppOfArity ``Array 1 && (type.getArg! 0).isConstOf ``Lake.LeanOption then some (.array (.other ``Lake.LeanOption "Lean option" none))
+                else if type.isAppOfArity ``Array 1 && (type.getArg! 0).isConstOf ``Lean.LeanOption then some (.array (.other ``Lean.LeanOption "Lean option" none))
                 else if type.isAppOfArity ``Array 1 && (type.getArg! 0).isConstOf ``String then some (.array .string)
                 else if type.isAppOfArity ``Array 1 && (type.getArg! 0).isConstOf ``Name then some (.array .string)
                 else if type.isAppOfArity ``Array 1 && (type.getArg! 0).isConstOf ``System.FilePath then some (.array .path)

Manual/Tactics/Custom.lean

@@ -132,120 +132,3 @@ Multiple {keywordOf Lean.Parser.Command.macro_rules}`macro_rules` declarations a
 Backtracking is at the granularity of {keywordOf Lean.Parser.Command.macro_rules}`macro_rules` declarations, not their individual cases.
 :::
 ::::
-
-
-# The Tactic Monad
-%%%
-tag := "tactic-monad"
-draft := true
-%%%
-
-::: planned 67
- * Relationship to {name}`Lean.Elab.Term.TermElabM`, {name}`Lean.Meta.MetaM`
- * Overview of available effects
- * Checkpointing
-:::
-
-{docstring Lean.Elab.Tactic.Tactic}
-
-{docstring Lean.Elab.Tactic.TacticM}
-
-{docstring Lean.Elab.Tactic.run}
-
-{docstring Lean.Elab.Tactic.runTermElab}
-
-## Control
-
-{docstring Lean.Elab.Tactic.tryTactic}
-
-{docstring Lean.Elab.Tactic.tryTactic?}
-
-## Expressions
-
-{docstring Lean.Elab.Tactic.ensureHasNoMVars}
-
-{docstring Lean.Elab.Tactic.getFVarId}
-
-{docstring Lean.Elab.Tactic.getFVarIds}
-
-{docstring Lean.Elab.Tactic.sortMVarIdsByIndex}
-
-{docstring Lean.Elab.Tactic.sortMVarIdArrayByIndex}
-
-## Source Locations
-
-{docstring Lean.Elab.Tactic.withLocation}
-
-## Goals
-
-{docstring Lean.Elab.Tactic.getGoals}
-
-{docstring Lean.Elab.Tactic.setGoals}
-
-{docstring Lean.Elab.Tactic.getMainGoal}
-
-{docstring Lean.Elab.Tactic.getMainTag}
-
-{docstring Lean.Elab.Tactic.closeMainGoal}
-
-{docstring Lean.Elab.Tactic.focus}
-
-{docstring Lean.Elab.Tactic.tagUntaggedGoals}
-
-{docstring Lean.Elab.Tactic.getUnsolvedGoals}
-
-{docstring Lean.Elab.Tactic.pruneSolvedGoals}
-
-{docstring Lean.Elab.Tactic.appendGoals}
-
-{docstring Lean.Elab.Tactic.closeMainGoalUsing}
-
-## Term Elaboration
-
-{docstring Lean.Elab.Tactic.elabTerm}
-
-{docstring Lean.Elab.Tactic.elabTermEnsuringType}
-
-{docstring Lean.Elab.Tactic.elabTermWithHoles}
-
-
-## Low-Level Operations
-
-These operations are primarily used as part of the implementation of {name}`TacticM` or of particular tactics.
-It's rare that they are useful when implementing new tactics.
-
-### Monad Class Implementations
-
-These operations are exposed through standard Lean monad type classes.
-
-{docstring Lean.Elab.Tactic.tryCatch}
-
-{docstring Lean.Elab.Tactic.liftMetaMAtMain}
-
-{docstring Lean.Elab.Tactic.getMainModule}
-
-{docstring Lean.Elab.Tactic.orElse}
-
-### Macro Expansion
-
-{docstring Lean.Elab.Tactic.getCurrMacroScope}
-
-{docstring Lean.Elab.Tactic.adaptExpander}
-
-### Simplifier
-
-{docstring Lean.Elab.Tactic.elabSimpArgs}
-
-{docstring Lean.Elab.Tactic.elabSimpConfig}
-
-{docstring Lean.Elab.Tactic.elabSimpConfigCtxCore}
-
-{docstring Lean.Elab.Tactic.dsimpLocation'}
-
-{docstring Lean.Elab.Tactic.elabDSimpConfigCore}
-
-### Attributes
-
-{docstring Lean.Elab.Tactic.tacticElabAttribute}
-
-{docstring Lean.Elab.Tactic.mkTacticAttribute}

Manual/Terms.lean

@@ -1321,9 +1321,9 @@ partial instance : OfNat Blah n where
 -- This shows that the partial instance was not unfolded
 /--
 error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
-  motive (instOfNatBlah_1.f 0) : Sort ?u.909
+  motive (instOfNatBlah_1.f 0) : Sort ?u.910
 but is expected to have type
-  motive n✝ : Sort ?u.909
+  motive n✝ : Sort ?u.910
 -/
 #guard_msgs in
 def defg (n : Blah) : Bool :=
@@ -1332,9 +1332,9 @@ def defg (n : Blah) : Bool :=
 
 /--
 error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
-  motive (Float.ofScientific 25 true 1) : Sort ?u.953
+  motive (Float.ofScientific 25 true 1) : Sort ?u.954
 but is expected to have type
-  motive x✝ : Sort ?u.953
+  motive x✝ : Sort ?u.954
 -/
 #guard_msgs in
 def twoPointFive? : Float → Option Float
@@ -1391,7 +1391,7 @@ is not definitionally equal to the right-hand side
   3 = 5
 ⊢ 3 = 3 ∨ 3 = 5
 ---
-info: { val := 3, val2 := ?m.1757, ok := ⋯ } : OnlyThreeOrFive
+info: { val := 3, val2 := ?m.1765, ok := ⋯ } : OnlyThreeOrFive
 -/
 #guard_msgs in
 #check OnlyThreeOrFive.mk 3 ..

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "94472367e2ad3acae8fd8d46267a7ae991d5ee62",
+   "rev": "984933046ebda997f57d9b464d7647b61625dfd3",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8ba0ef10d178ab95a5d6fe3cfbd586c6ecef2717",
+   "rev": "b16338c5c66f57ef5510d4334eb6fa4e2c6c8cd8",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-06-05
+leanprover/lean4:nightly-2025-06-19