From 2bb57f7a259d5cb0e41e919f565952eb1a306b3f Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 21 May 2025 08:11:11 +0200 Subject: [PATCH] chore: bump to nightly-2025-05-20 --- Manual/Elaboration.lean | 2 +- Manual/Intro.lean | 4 +- Manual/Language/InductiveTypes.lean | 8 +- .../Language/InductiveTypes/Structures.lean | 4 +- Manual/Meta/Basic.lean | 108 ------------------ Manual/Meta/Syntax.lean | 4 +- Manual/Meta/Tactics.lean | 2 + Manual/NotationsMacros.lean | 4 +- Manual/NotationsMacros/SyntaxDef.lean | 31 ++--- Manual/RecursiveDefs/PartialFixpoint.lean | 2 +- Manual/Runtime.lean | 2 +- Manual/Terms.lean | 36 +++--- Manual/Types.lean | 4 +- lake-manifest.json | 6 +- lean-toolchain | 2 +- 15 files changed, 59 insertions(+), 160 deletions(-) diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean index 456cbce3..85a3af2a 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.736 = ?m.736 : Prop + ?m.744 = ?m.744 : Prop but is expected to have type e1 = e2 : Prop -/ diff --git a/Manual/Intro.lean b/Manual/Intro.lean index 381e7847..13290ee1 100644 --- a/Manual/Intro.lean +++ b/Manual/Intro.lean @@ -99,9 +99,9 @@ declaration uses 'sorry' Error messages are shown like this: ```leanOutput output (severity := error) -Application type mismatch: In the appplication +Application type mismatch: In the application Nat.succ "two" -the final argument +the argument "two" has type String : Type diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean index 085ad6de..ab9ca1a5 100644 --- a/Manual/Language/InductiveTypes.lean +++ b/Manual/Language/InductiveTypes.lean @@ -264,10 +264,14 @@ inductive Either' (α : Type u) (β : Type v) : Type (max u v) where | right : β → Either' α β ``` ```leanOutput Either' -inductive datatype parameter mismatch +Mismatched inductive type parameter in + Either' α β +The provided argument α -expected +is not definitionally equal to the expected parameter α✝ + +Note: The value of parameter 'α✝' must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary. ``` Placing the parameters after the colon results in parameters that can be instantiated by the constructors: diff --git a/Manual/Language/InductiveTypes/Structures.lean b/Manual/Language/InductiveTypes/Structures.lean index 9c36444d..20038b25 100644 --- a/Manual/Language/InductiveTypes/Structures.lean +++ b/Manual/Language/InductiveTypes/Structures.lean @@ -533,9 +533,9 @@ it is a type error to apply {name}`printEven` directly to {name}`two`: #check printEven two ``` ```leanOutput printTwo -Application type mismatch: In the appplication +Application type mismatch: In the application printEven two -the final argument +the argument two has type EvenPrime : Type diff --git a/Manual/Meta/Basic.lean b/Manual/Meta/Basic.lean index e6757f54..d06e1760 100644 --- a/Manual/Meta/Basic.lean +++ b/Manual/Meta/Basic.lean @@ -152,111 +152,3 @@ def commandWithoutAsync : (act : CommandElabM α) → CommandElabM α := def withoutAsync [Monad m] [MonadWithOptions m] : (act : m α) → m α := withOptions (Elab.async.set · false) - - -/-- -Consistently rewrite all substrings that look like automatic metavariables (e.g "?m.123") so -that they're ?m.1, ?m.2, etc. --/ -def normalizeMetavars (str : String) : String := Id.run do - let mut out := "" - let mut iter := str.iter - let mut gensymCounter := 1 - let mut nums : Std.HashMap String Nat := {} - -- States are: - -- * none - Not looking at a metavar - -- * 0 - Saw the ? - -- * 1 - Saw the m - -- * 2 - Saw the . - -- * 3 - Saw one or more digits - let mut state : Option (Fin 4 × String.Iterator) := none - while h : iter.hasNext do - let c := iter.curr' h - - match state with - | none => - if c == '?' then - state := some (0, iter) - else - out := out.push c - | some (0, i) => - state := if c == 'm' then some (1, i) else none - | some (1, i) => - state := if c == '.' then some (2, i) else none - | some (2, i) => - state := if c.isDigit then some (3, i) else none - | some (3, i) => - unless c.isDigit do - state := none - let mvarStr := i.extract iter - match nums[mvarStr]? with - | none => - nums := nums.insert mvarStr gensymCounter - out := out ++ s!"?m.{gensymCounter}" - gensymCounter := gensymCounter + 1 - | some s => out := out ++ s!"?m.{s}" - out := out.push c - - iter := iter.next - match state with - | some (3, i) => - let mvarStr := i.extract iter - match nums[mvarStr]? with - | none => - nums := nums.insert mvarStr gensymCounter - out := out ++ s!"?m.{gensymCounter}" - gensymCounter := gensymCounter + 1 - | some s => out := out ++ s!"?m.{s}" - | some (_, i) => - out := out ++ i.extract iter - | _ => pure () - - out - -/-- info: "List ?m.1" -/ -#guard_msgs in -#eval normalizeMetavars "List ?m.9783" - -/-- info: "List ?m.1 " -/ -#guard_msgs in -#eval normalizeMetavars "List ?m.9783 " - -/-- info: "x : ?m.1\nxs : List ?m.1\nelem : x ∈ xs\n⊢ xs.length > 0\n" -/ -#guard_msgs in -#eval normalizeMetavars - r##"x : ?m.1034 -xs : List ?m.1034 -elem : x ∈ xs -⊢ xs.length > 0 -"## - -/-- info: "x : ?m.1\nxs : List ?m.1\nelem : x ∈ xs\n⊢ xs.length > 0" -/ -#guard_msgs in -#eval normalizeMetavars - r##"x : ?m.1034 -xs : List ?m.1034 -elem : x ∈ xs -⊢ xs.length > 0"## - -/-- info: "x : ?m.1\nxs : List ?m.2\nelem : x ∈ xs\n⊢ xs.length > 0" -/ -#guard_msgs in -#eval normalizeMetavars - r##"x : ?m.1034 -xs : List ?m.10345 -elem : x ∈ xs -⊢ xs.length > 0"## - -/-- info: "x : ?m.1\nxs : List ?m.2\nelem : x ∈ xs\n⊢ xs.length > 0" -/ -#guard_msgs in -#eval normalizeMetavars - r##"x : ?m.1035 -xs : List ?m.1034 -elem : x ∈ xs -⊢ xs.length > 0"## - -#eval normalizeMetavars - r##"x : ?m.1035 -α : Type ?u.1234 -xs : List ?m.1034 -elem : x ∈ xs -⊢ xs.length > 0"## diff --git a/Manual/Meta/Syntax.lean b/Manual/Meta/Syntax.lean index 63a54a83..897c2430 100644 --- a/Manual/Meta/Syntax.lean +++ b/Manual/Meta/Syntax.lean @@ -830,7 +830,7 @@ where return bar ++ .nest 2 (← production which stx |>.run' {}) def testGetBnf (config : FreeSyntaxConfig) (isFirst : Bool) (stxs : List Syntax) : TermElabM String := do - let (tagged, _) ← getBnf config isFirst stxs |>.run {} {partContext := ⟨⟨default, default, default, default, default⟩, default⟩} + let (tagged, _) ← getBnf config isFirst stxs |>.run (← ``(Manual)) (.const ``Manual []) {} {partContext := ⟨⟨default, default, default, default, default⟩, default⟩} pure tagged.stripTags namespace Tests @@ -897,7 +897,7 @@ info: antiquot ::= ... end Tests -instance : MonadWithReaderOf Core.Context DocElabM := inferInstanceAs (MonadWithReaderOf Core.Context (ReaderT PartElabM.State (StateT DocElabM.State TermElabM))) +instance : MonadWithReaderOf Core.Context DocElabM := inferInstanceAs (MonadWithReaderOf Core.Context (ReaderT DocElabContext (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)))) def withOpenedNamespace (ns : Name) (act : DocElabM α) : DocElabM α := try diff --git a/Manual/Meta/Tactics.lean b/Manual/Meta/Tactics.lean index 34278bb7..275096db 100644 --- a/Manual/Meta/Tactics.lean +++ b/Manual/Meta/Tactics.lean @@ -11,6 +11,7 @@ import Verso.Code.Highlighted import Verso.Doc.ArgParse import Verso.Doc.Suggestion import SubVerso.Highlighting.Code +import SubVerso.Examples.Messages import VersoManual import Manual.Meta.Basic @@ -22,6 +23,7 @@ open Lean Elab Term Tactic open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets open Verso.Genre.Manual.InlineLean.Scopes (runWithOpenDecls runWithVariables) open SubVerso.Highlighting +open SubVerso.Examples.Messages structure TacticOutputConfig where «show» : Bool := true diff --git a/Manual/NotationsMacros.lean b/Manual/NotationsMacros.lean index d8529706..d3e378b2 100644 --- a/Manual/NotationsMacros.lean +++ b/Manual/NotationsMacros.lean @@ -273,9 +273,9 @@ example (cmd1 cmd2 : TSyntax `command) : MacroM (TSyntax `command) := `($cmd1 $c ``` The result is two type errors like the following: ```leanOutput cmdQuot -Application type mismatch: In the appplication +Application type mismatch: In the application cmd1.raw -the final argument +the argument cmd1 has type TSyntax `command : Type diff --git a/Manual/NotationsMacros/SyntaxDef.lean b/Manual/NotationsMacros/SyntaxDef.lean index 2202ebdf..2fcbece9 100644 --- a/Manual/NotationsMacros/SyntaxDef.lean +++ b/Manual/NotationsMacros/SyntaxDef.lean @@ -756,35 +756,36 @@ In particular, Indentation-sensitvity is specified by combining {name Lean.Parse :::example "Aligned Columns" This syntax for saving notes takes a bulleted list of items, each of which must be aligned at the same column. ```lean -syntax "note " ppLine withPosition((colEq "• " str ppLine)+) : term +syntax "note " ppLine withPosition((colEq "◦ " str ppLine)+) : term ``` There is no elaborator or macro associated with this syntax, but the following example is accepted by the parser: ```lean (error := true) (name := noteEx1) #check note - • "One" - • "Two" + ◦ "One" + ◦ "Two" ``` ```leanOutput noteEx1 -elaboration function for '«termNote__•__»' has not been implemented +elaboration function for '«termNote__◦__»' has not been implemented note - • "One" - • "Two" + ◦ "One" + ◦ "Two" + ``` The syntax does not require that the list is indented with respect to the opening token, which would require an extra `withPosition` and a `colGt`. ```lean (error := true) (name := noteEx15) #check note -• "One" -• "Two" +◦ "One" +◦ "Two" ``` ```leanOutput noteEx15 -elaboration function for '«termNote__•__»' has not been implemented +elaboration function for '«termNote__◦__»' has not been implemented note - • "One" - • "Two" + ◦ "One" + ◦ "Two" ``` @@ -792,8 +793,8 @@ The following examples are not syntactically valid because the columns of the bu ```syntaxError noteEx2 #check note - • "One" - • "Two" + ◦ "One" + ◦ "Two" ``` ```leanOutput noteEx2 :4:3-4:4: expected end of input @@ -802,8 +803,8 @@ The following examples are not syntactically valid because the columns of the bu ```syntaxError noteEx2 #check note - • "One" - • "Two" + ◦ "One" + ◦ "Two" ``` ```leanOutput noteEx2 :4:5-4:6: expected end of input diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean index 7880c338..60f7f02f 100644 --- a/Manual/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/RecursiveDefs/PartialFixpoint.lean @@ -175,7 +175,7 @@ The error message on the recursive call is: ```leanOutput nonTailPos Could not prove 'List.findIndex' to be monotone in its recursive calls: Cannot eliminate recursive call `List.findIndex ys p` enclosed in - let_fun r := ys✝.findIndex p; + have r := ys✝.findIndex p; if r = -1 then -1 else r + 1 ``` diff --git a/Manual/Runtime.lean b/Manual/Runtime.lean index df1f4f74..d1be5c0c 100644 --- a/Manual/Runtime.lean +++ b/Manual/Runtime.lean @@ -203,7 +203,7 @@ def process' (str : String) : String × String:= The IR for {lean}`process` includes no `inc` or `dec` instructions. If the incoming string `x_1` is a unique reference, then it is still a unique reference when passed to {name}`String.set`, which can then use in-place modification: -```leanOutput p1 +```leanOutput p1 (allowDiff := 5) [result] def process._closed_1 : obj := let x_1 : obj := ""; diff --git a/Manual/Terms.lean b/Manual/Terms.lean index 27a5378b..b49ec252 100644 --- a/Manual/Terms.lean +++ b/Manual/Terms.lean @@ -1284,7 +1284,7 @@ $x:ident@$h:ident:$e -- Check claims about patterns -- Literals -/-- error: invalid pattern, constructor or constant marked with '[match_pattern]' expected -/ +/-- error: Invalid pattern: Expected a constructor or constant marked with `[match_pattern]` -/ #guard_msgs in def foo (x : String) : String := match x with @@ -1301,7 +1301,7 @@ instance : OfNat Blah n where ofNat := ⟨n + 1⟩ /-- -error: missing cases: +error: Missing cases: (Blah.mk (Nat.succ (Nat.succ _))) (Blah.mk Nat.zero) -/ @@ -1320,10 +1320,10 @@ partial instance : OfNat Blah n where -- This shows that the partial instance was not unfolded /-- -error: dependent elimination failed, type mismatch when solving alternative with type - motive (instOfNatBlah_1.f 0) -but expected - motive n✝ +error: Dependent elimination failed: Type mismatch when solving this alternative: it has type + motive (instOfNatBlah_1.f 0) : Sort ?u.859 +but is expected to have type + motive n✝ : Sort ?u.859 -/ #guard_msgs in def defg (n : Blah) : Bool := @@ -1331,10 +1331,10 @@ def defg (n : Blah) : Bool := | 0 => true /-- -error: dependent elimination failed, type mismatch when solving alternative with type - motive (Float.ofScientific 25 true 1) -but expected - motive x✝ +error: Dependent elimination failed: Type mismatch when solving this alternative: it has type + motive (Float.ofScientific 25 true 1) : Sort ?u.902 +but is expected to have type + motive x✝ : Sort ?u.902 -/ #guard_msgs in def twoPointFive? : Float → Option Float @@ -1370,7 +1370,7 @@ def ggg : OnlyThreeOrFive → Nat | {val := n} => n /-- -error: missing cases: +error: Missing cases: (OnlyThreeOrFive.mk _ true _) -/ #guard_msgs in @@ -1391,7 +1391,7 @@ is not definitionally equal to the right-hand side 3 = 5 ⊢ 3 = 3 ∨ 3 = 5 --- -info: { val := 3, val2 := ?m.1613, ok := ⋯ } : OnlyThreeOrFive +info: { val := 3, val2 := ?m.1639, ok := ⋯ } : OnlyThreeOrFive -/ #guard_msgs in #check OnlyThreeOrFive.mk 3 .. @@ -1404,7 +1404,7 @@ set_option pp.mvars.anonymous false in /-- info: fun y => match - let_fun this := ⟨y * 3, ⋯⟩; + have this := ⟨y * 3, ⋯⟩; this with | ⟨x, z⟩ => match x, z with @@ -1559,8 +1559,8 @@ Attempting to match on a number and a proof that it is in fact {lean}`5` is an e | 5, rfl => "ok" ``` ```leanOutput noMotive -invalid match-expression, pattern contains metavariables - Eq.refl ?m.73 +Invalid match expression: This pattern contains metavariables: + Eq.refl ?m.76 ``` An explicit motive explains the relationship between the discriminants: ```lean (name := withMotive) @@ -1629,9 +1629,9 @@ def boolCases (b : Bool) ``` The error for the first case is typical of both: ```leanOutput boolCases1 -Application type mismatch: In the appplication +Application type mismatch: In the application ifTrue h -the final argument +the argument h has type b = true : Prop @@ -1689,7 +1689,7 @@ def nonzero (n : Nat) : Bool := ``` The error message on the pattern `1 + _` is: ```leanOutput nonPat -invalid patterns, `k` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching +Invalid pattern(s): `k` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching: .(Nat.add 1 k) ``` diff --git a/Manual/Types.lean b/Manual/Types.lean index 88da7d26..a359f218 100644 --- a/Manual/Types.lean +++ b/Manual/Types.lean @@ -117,9 +117,9 @@ example : LengthList String 5 := ("Wrong", "number", ()) ``` ```leanOutput wrongNum -Application type mismatch: In the appplication +Application type mismatch: In the application ("number", ()) -the final argument +the argument () has type Unit : Type diff --git a/lake-manifest.json b/lake-manifest.json index 7d2a575e..f1f5e705 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "ff98b5d62fa1ef5f533d56b342c0d1a3207d7ad1", + "rev": "40ce546e0e1416cedd4eef2fa5a51c7254b16a6b", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", @@ -21,11 +21,11 @@ "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/subverso.git", + {"url": "https://github.com/leanprover/subverso", "type": "git", "subDir": null, "scope": "", - "rev": "a8b267f7bd8c78703dee72cfd995a35895645d60", + "rev": "83a4aa2bf2fe7346357ba0c63202bba94664dd6f", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index eb3e24b7..ee1a35a7 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-05-12 +leanprover/lean4:nightly-2025-05-20