From 4b270b403bf06842fd2d48e71e3567563b5c72dd Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 11 Jun 2025 11:42:34 +0200 Subject: [PATCH 1/2] chore: update to nightly-2025-06-11 --- Manual/BasicTypes/Maps/TreeMap.lean | 8 -- Manual/BasicTypes/Maps/TreeSet.lean | 8 ++ Manual/BuildTools/Lake.lean | 40 +++++++--- Manual/Elaboration.lean | 2 +- Manual/Interaction.lean | 2 +- Manual/Meta/LakeToml.lean | 2 +- Manual/Tactics/Custom.lean | 117 ---------------------------- Manual/Terms.lean | 10 +-- lake-manifest.json | 4 +- lean-toolchain | 2 +- 10 files changed, 48 insertions(+), 147 deletions(-) diff --git a/Manual/BasicTypes/Maps/TreeMap.lean b/Manual/BasicTypes/Maps/TreeMap.lean index ac1fbfeb..18b2689d 100644 --- a/Manual/BasicTypes/Maps/TreeMap.lean +++ b/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!} diff --git a/Manual/BasicTypes/Maps/TreeSet.lean b/Manual/BasicTypes/Maps/TreeSet.lean index 7511f6ef..83ceab1c 100644 --- a/Manual/BasicTypes/Maps/TreeSet.lean +++ b/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?} diff --git a/Manual/BuildTools/Lake.lean b/Manual/BuildTools/Lake.lean index d3b72928..b58e70dd 100644 --- a/Manual/BuildTools/Lake.lean +++ b/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,7 +364,11 @@ 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` @@ -371,11 +376,15 @@ The facets available for modules are: : `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]. ::: diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean index 10de99a2..e91f8981 100644 --- a/Manual/Elaboration.lean +++ b/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 -/ diff --git a/Manual/Interaction.lean b/Manual/Interaction.lean index f83123ce..5871f74e 100644 --- a/Manual/Interaction.lean +++ b/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 diff --git a/Manual/Meta/LakeToml.lean b/Manual/Meta/LakeToml.lean index 5056aaf9..35c7fdb2 100644 --- a/Manual/Meta/LakeToml.lean +++ b/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) diff --git a/Manual/Tactics/Custom.lean b/Manual/Tactics/Custom.lean index dd082728..38b7df29 100644 --- a/Manual/Tactics/Custom.lean +++ b/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} diff --git a/Manual/Terms.lean b/Manual/Terms.lean index 1dcf348e..6630c2f1 100644 --- a/Manual/Terms.lean +++ b/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 .. diff --git a/lake-manifest.json b/lake-manifest.json index 9ed3df26..80aab530 100644 --- a/lake-manifest.json +++ b/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", diff --git a/lean-toolchain b/lean-toolchain index a8cce637..6c00a5bf 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-06-05 +leanprover/lean4:nightly-2025-06-11 From ca9cd3894b06375e9709b9d060085cc0d9472c16 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 20 Jun 2025 11:33:20 +1000 Subject: [PATCH 2/2] bump toolchain, and deprecation --- Manual/BasicTypes/BitVec.lean | 4 ++-- lean-toolchain | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Manual/BasicTypes/BitVec.lean b/Manual/BasicTypes/BitVec.lean index a6eba5a5..93af1445 100644 --- a/Manual/BasicTypes/BitVec.lean +++ b/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?} diff --git a/lean-toolchain b/lean-toolchain index 6c00a5bf..4389302b 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-06-11 +leanprover/lean4:nightly-2025-06-19