From 15e7991bf96166c8703b9fc98d97318e775c1faa Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 19 Dec 2025 16:50:57 +0100 Subject: [PATCH] chore: bump to latest Lean release (4.26.0) --- .../IndicesParametersUniverses.lean | 6 +- book/FPLean/Examples.lean | 101 +++++++----------- book/FPLean/Examples/Commands.lean | 18 +++- book/FPLean/Examples/Commands/ShLex.lean | 8 +- book/FPLean/Examples/OtherLanguages.lean | 14 +-- .../FunctorApplicativeMonad/Applicative.lean | 2 +- .../GettingToKnow/DatatypesPatterns.lean | 2 +- book/FPLean/GettingToKnow/Evaluating.lean | 2 +- book/FPLean/GettingToKnow/Polymorphism.lean | 14 +-- book/FPLean/HelloWorld/StepByStep.lean | 3 +- book/FPLean/Monads/Class.lean | 29 ++--- book/FPLean/Monads/IO.lean | 60 +++++------ .../ProgramsProofs/ArraysTermination.lean | 6 +- book/FPLean/TacticsInductionProofs.lean | 2 +- book/FPLean/TypeClasses/OutParams.lean | 10 +- book/lake-manifest.json | 16 ++- book/lakefile.lean | 31 ++++-- book/lean-toolchain | 2 +- book/verso-sources.json | 2 +- examples/ExampleSupport.lean | 6 +- examples/Examples/Classes.lean | 12 ++- .../DependentTypes/IndicesParameters.lean | 6 +- .../Examples/FunctorApplicativeMonad.lean | 4 +- examples/Examples/HelloWorld.lean | 13 ++- examples/Examples/Induction.lean | 2 +- examples/Examples/Intro.lean | 38 +++---- examples/Examples/Monads/Class.lean | 34 +++--- examples/Examples/Monads/IO.lean | 53 +++++---- examples/Examples/ProgramsProofs/Arrays.lean | 5 +- examples/lake-manifest.json | 2 +- examples/lakefile.lean | 5 + examples/lean-toolchain | 2 +- 32 files changed, 269 insertions(+), 241 deletions(-) diff --git a/book/FPLean/DependentTypes/IndicesParametersUniverses.lean b/book/FPLean/DependentTypes/IndicesParametersUniverses.lean index 2f53aa8..af8dffa 100644 --- a/book/FPLean/DependentTypes/IndicesParametersUniverses.lean +++ b/book/FPLean/DependentTypes/IndicesParametersUniverses.lean @@ -84,7 +84,7 @@ The provided argument 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. +Note: The value of parameter `α` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary. ``` Similarly, attempting to name an index results in an error: ```anchor WithNamedIndex @@ -100,7 +100,7 @@ The provided argument 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. +Note: The value of parameter `α` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary. ``` Using an appropriate universe level and placing the index after the colon results in a declaration that is acceptable: @@ -142,7 +142,7 @@ The provided argument is not definitionally equal to the expected parameter n -Note: The value of parameter 'n' must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary. +Note: The value of parameter `n` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary. ``` Using the {anchorName NatParam}`n` as suggested causes the declaration to be accepted: diff --git a/book/FPLean/Examples.lean b/book/FPLean/Examples.lean index 418add1..29fc84b 100644 --- a/book/FPLean/Examples.lean +++ b/book/FPLean/Examples.lean @@ -153,14 +153,11 @@ div.paragraph > .eval-steps:not(:last-child), div.paragraph > .eval-steps:not(:l "# -block_extension Block.leanEvalSteps (steps : Array Highlighted) where +block_extension Block.leanEvalSteps (steps : Array Highlighted) via withHighlighting where data := ToJson.toJson steps traverse _ _ _ := pure none toTeX := none - extraCss := [highlightingStyle, evalStepsStyle] - extraJs := [highlightingJs] - extraJsFiles := [{filename := "popper.js", contents := popper, sourceMap? := none}, {filename := "tippy.js", contents := tippy, sourceMap? := none}] - extraCssFiles := [("tippy-border.css", tippy.border.css)] + extraCss := [evalStepsStyle] toHtml := open Verso.Output.Html in some <| fun _ _ _ data _ => do @@ -253,7 +250,7 @@ private def getClass : MessageSeverity → String | .information => "information" | .warning => "warning" -block_extension Block.leanOutput (severity : MessageSeverity) (message : String) (summarize : Bool := false) where +block_extension Block.leanOutput (severity : MessageSeverity) (message : String) (summarize : Bool := false) via withHighlighting where data := ToJson.toJson (severity, message, summarize) traverse _ _ _ := do pure none @@ -261,10 +258,6 @@ block_extension Block.leanOutput (severity : MessageSeverity) (message : String) some <| fun _ go _ _ content => do pure <| .seq <| ← content.mapM fun b => do pure <| .seq #[← go b, .raw "\n"] - extraCss := [highlightingStyle] - extraJs := [highlightingJs] - extraJsFiles := [{filename := "popper.js", contents := popper, sourceMap? := none}, {filename := "tippy.js", contents := tippy, sourceMap? := none}] - extraCssFiles := [("tippy-border.css", tippy.border.css)] toHtml := open Verso.Output.Html in some <| fun _ _ _ data _ => do @@ -379,25 +372,30 @@ structure EvalStepContext extends CodeContext where instance [Monad m] [MonadOptions m] [MonadError m] [MonadLiftT CoreM m] : FromArgs EvalStepContext m where fromArgs := (fun x y => EvalStepContext.mk y x) <$> .positional' `step <*> fromArgs +private def replicateString (n : Nat) (c : Char) : String := + n.fold (init := "") fun _ _ s => s.push c + +private theorem replicateString_length {n c} : (replicateString n c).length = n := by + simp [replicateString] + induction n <;> simp [Nat.fold, *] + private def quoteCode (str : String) : String := Id.run do let str := if str.startsWith "`" || str.endsWith "`" then " " ++ str ++ " " else str let mut n := 1 let mut run := none - let mut iter := str.iter - while h : iter.hasNext do - let c := iter.curr' h - iter := iter.next + let mut iter := str.startPos + while h : iter ≠ str.endPos do + let c := iter.get h + iter := iter.next h if c == '`' then run := some (run.getD 0 + 1) else if let some k := run then if k > n then n := k run := none - let delim := String.mk (List.replicate n '`') + let delim := replicateString n '`' return delim ++ str ++ delim - - @[role_expander moduleEvalStep] def moduleEvalStep : RoleExpander | args, inls => do @@ -432,7 +430,7 @@ def moduleEvalStep : RoleExpander if let some step := steps[step.val]? then if let some code := code? then - _ ← ExpectString.expectString "step" code step.toString.trim + _ ← ExpectString.expectString "step" code step.toString.trimAscii.copy return #[← ``(Inline.other (Inline.lean $(quote step) {}) #[])] else let stepStr := step.toString @@ -462,17 +460,17 @@ private def editCodeBlock [Monad m] [MonadFileMap m] (stx : Syntax) (newContents let { start := {line := l1, ..}, .. } := txt.utf8RangeToLspRange rng let line1 := (txt.lineStart (l1 + 1)).extract txt.source (txt.lineStart (l1 + 2)) if line1.startsWith "```" then - return some s!"{delims}{line1.dropWhile (· == '`') |>.trim}\n{withNl newContents}{delims}" + return some s!"{delims}{line1.dropWhile (· == '`') |>.trimAscii.copy}\n{withNl newContents}{delims}" else return none where delims : String := Id.run do let mut n := 3 let mut run := none - let mut iter := newContents.iter - while h : iter.hasNext do - let c := iter.curr' h - iter := iter.next + let mut iter := newContents.startPos + while h : iter ≠ newContents.endPos do + let c := iter.get h + iter := iter.next h if c == '`' then run := some (run.getD 0 + 1) else if let some k := run then @@ -491,7 +489,7 @@ def moduleEvalStepBlock : CodeBlockExpander let steps := splitHighlighted (· == "===>") fragment if let some step := steps[step.val]? then - _ ← ExpectString.expectString "step" code (withNl step.toString.trim) + _ ← ExpectString.expectString "step" code (withNl step.toString.trimAscii.copy) return #[← ``(Block.other (Block.lean $(quote step) {}) #[])] else let ok := steps.mapIdx fun i s => ({suggestion := toString i, postInfo? := some s.toString}) @@ -532,7 +530,7 @@ def moduleEqSteps : CodeBlockExpander let steps := splitHighlighted (· ∈ ["={", "}="]) fragment let steps ← steps.mapM fun hl => do if let some ((.token ⟨.docComment, txt⟩), _) := hl.firstToken then - let txt := txt.trim |>.stripPrefix "/--" |>.stripSuffix "-/" |>.trim + let txt := txt.trimAscii |>.dropPrefix "/--" |>.dropSuffix "-/" |>.trimAscii |>.copy if let some ⟨#[.p txts]⟩ := MD4Lean.parse txt then let mut out : Array Term := #[] for txt in txts do @@ -711,7 +709,7 @@ def commandOut : RoleExpander let cmd ← oneCodeStr inls let output ← Commands.commandOut container cmd logSilentInfo output - return #[← ``(Inline.code $(quote output.trim))] + return #[← ``(Inline.code $(quote output.trimAscii.copy))] @[code_block_expander commandOut] def commandOutCodeBlock : CodeBlockExpander @@ -719,7 +717,7 @@ def commandOutCodeBlock : CodeBlockExpander let (container, command) ← ArgParse.run ((·, ·) <$> .positional `container .ident <*> .positional `command .strLit) args let output ← Commands.commandOut container command - _ ← ExpectString.expectString "command output" outStr (withNl output) (useLine := fun l => !l.trim.isEmpty) (preEq := String.trim) + _ ← ExpectString.expectString "command output" outStr (withNl output) (useLine := fun l => !l.trimAscii.isEmpty) (preEq := (·.trimAscii.copy)) logSilentInfo output return #[← ``(Block.code $(quote output))] @@ -778,20 +776,20 @@ def commands : CodeBlockExpander let mut quoted := false for line in specStr.splitOn "\n" do if line.startsWith "$$" then - commands := commands.push (.quote (line.drop 2 |>.trim)) + commands := commands.push (.quote (line.drop 2 |>.trimAscii |>.copy)) quoted := true else if line.startsWith "$" then - let line := line.drop 1 |>.trim + let line := line.drop 1 |>.trimAscii quoted := false if line.contains '#' then let cmd := line.takeWhile (· ≠ '#') - let rest := (line.drop (cmd.length + 1)).trim - commands := commands.push (.run cmd.trim (some rest)) + let rest := (line.drop (cmd.positions.count + 1)).trimAscii.copy + commands := commands.push (.run cmd.trimAscii.copy (some rest)) else - commands := commands.push (.run line none) + commands := commands.push (.run line.copy none) else if quoted then - commands := commands.push (.out line.trimRight) + commands := commands.push (.out line.trimAsciiEnd.copy) let mut out := #[] let mut outStr := "" for cmdSpec in commands do @@ -816,8 +814,8 @@ def commands : CodeBlockExpander | .out txt => out := out.push (txt, false) outStr := outStr ++ withNl txt - unless str.getString.trim == "" && outStr.trim == "" do - _ ← ExpectString.expectString "commands" str outStr (preEq := String.trim) + unless str.getString.trimAscii.isEmpty && outStr.trimAscii.isEmpty do + _ ← ExpectString.expectString "commands" str outStr (preEq := (·.trimAscii.copy)) if «show» then pure #[← ``(Block.other (Block.shellCommands $(quote out)) #[])] else pure #[] @@ -898,7 +896,7 @@ def moduleOutText : RoleExpander if let `(inline|role{ $_ $_* }[ $x ]) := (← getRef) then x.raw else str let suggs : Array Suggestion := strings.map fun msg => { - suggestion := quoteCode msg.trim + suggestion := quoteCode msg.trimAscii.copy } let h ← if suggs.isEmpty then pure m!"" @@ -917,7 +915,7 @@ def moduleOutText : RoleExpander mkNullNode #[tok1, tok2] else mkNullNode contents for (msg, _) in infos do - let msg := msg.toString.trim + let msg := msg.toString.trimAscii.copy Suggestion.saveSuggestion stx (quoteCode <| ExpectString.abbreviateString msg) (quoteCode msg) return #[← ``(sorryAx _ true)] @@ -927,17 +925,17 @@ where let str := if str.startsWith "`" || str.endsWith "`" then " " ++ str ++ " " else str let mut n := 1 let mut run := none - let mut iter := str.iter - while h : iter.hasNext do - let c := iter.curr' h - iter := iter.next + let mut iter := str.startPos + while h : iter ≠ str.endPos do + let c := iter.get h + iter := iter.next h if c == '`' then run := some (run.getD 0 + 1) else if let some k := run then if k > n then n := k run := none - let delim := String.mk (List.replicate n '`') + let delim := replicateString n '`' return delim ++ str ++ delim macro_rules @@ -953,22 +951,3 @@ macro_rules `(inline|role{%$rs moduleOutText MessageSeverity.error anchor:=$a $arg*}%$re [%$s $str* ]%$e) | `(inline|role{%$rs anchorWarningText $a:arg_val $arg*}%$re [%$s $str* ]%$e) => `(inline|role{%$rs moduleOutText MessageSeverity.warning anchor:=$a $arg*}%$re [%$s $str* ]%$e) - - -def hasSubstring (s pattern : String) : Bool := - if h : pattern.endPos.1 = 0 then false - else - have hPatt := Nat.zero_lt_of_ne_zero h - let rec loop (pos : String.Pos.Raw) := - if h : pos.byteIdx + pattern.endPos.byteIdx > s.endPos.byteIdx then - false - else - have := Nat.lt_of_lt_of_le (Nat.add_lt_add_left hPatt _) (Nat.ge_of_not_lt h) - if pos.substrEq s pattern 0 pattern.endPos.byteIdx then - have := Nat.sub_lt_sub_left this (Nat.add_lt_add_left hPatt _) - true - else - have := Nat.sub_lt_sub_left this (pos.byteIdx_lt_byteIdx_next s) - loop (pos.next s) - termination_by s.endPos.1 - pos.1 - loop 0 diff --git a/book/FPLean/Examples/Commands.lean b/book/FPLean/Examples/Commands.lean index 3ca78ad..71feec6 100644 --- a/book/FPLean/Examples/Commands.lean +++ b/book/FPLean/Examples/Commands.lean @@ -35,6 +35,18 @@ def requireContainer (container : Ident) : m Container := do private def localeVars : Array String := #["LANG", "LC_ALL"] +private def lakeVars : Array String := + #["ELAN_TOOLCHAIN", "LEAN_SYSROOT", "LEAN", "LAKE", "LAKE_HOME", "LEAN_PATH", "LAKE_CACHE_DIR", "LEAN_AR", "LEAN_CC", "DYLD_LIBRARY_PATH"] + +private def fixPath (path : String) := + System.SearchPath.parse path + |>.iter + |>.map (·.toString) + |>.filter (fun p => ((p.find? ".elan").isNone || (p.find? "toolchains").isNone)) + |>.toList + |> System.SearchPath.separator.toString.intercalate + + def command (container : Ident) (dir : System.FilePath) (command : StrLit) (viaShell := false) : m IO.Process.Output := do let c ← ensureContainer container unless dir.isRelative do @@ -49,13 +61,13 @@ def command (container : Ident) (dir : System.FilePath) (command : StrLit) (viaS cmd := cmd, args := args, cwd := dir, - env := #[("PATH", some (extraPath ++ path))] ++ localeVars.map (·, some "C.UTF-8") + env := #[("PATH", some (extraPath ++ fixPath path))] ++ lakeVars.map (·, none) ++ localeVars.map (·, some "C.UTF-8") } if out.exitCode != 0 then let stdout := m!"Stdout: {indentD out.stdout}" let stderr := m!"Stderr: {indentD out.stderr}" throwErrorAt command "Non-zero exit code from '{command.getString}' ({out.exitCode}).\n{indentD stdout}\n{indentD stderr}" - modifyEnv (containersExt.modifyState · (·.insert container.getId { c with outputs := c.outputs.insert command.getString.trim out.stdout })) + modifyEnv (containersExt.modifyState · (·.insert container.getId { c with outputs := c.outputs.insert command.getString.trimAscii.copy out.stdout })) return out where @@ -71,7 +83,7 @@ where def commandOut (container : Ident) (command : StrLit) : m String := do let c ← requireContainer container - if let some out := c.outputs[command.getString.trim]? then + if let some out := c.outputs[command.getString.trimAscii.copy]? then return out else throwErrorAt command "Output not found: {indentD command}" diff --git a/book/FPLean/Examples/Commands/ShLex.lean b/book/FPLean/Examples/Commands/ShLex.lean index 4bdcf4e..c5ca5d9 100644 --- a/book/FPLean/Examples/Commands/ShLex.lean +++ b/book/FPLean/Examples/Commands/ShLex.lean @@ -8,12 +8,12 @@ private inductive State where def shlex (cmd : String) : Except String (Array String) := do let mut state : State := .normal - let mut iter := cmd.iter + let mut iter := cmd.startPos let mut out : Array String := #[] let mut current : Option String := none - while h : iter.hasNext do - let c := iter.curr' h - iter := iter.next' h + while h : iter ≠ cmd.endPos do + let c := iter.get h + iter := iter.next h match state, c with | .normal, '\\' => state := .escaped state diff --git a/book/FPLean/Examples/OtherLanguages.lean b/book/FPLean/Examples/OtherLanguages.lean index a6b3c56..490ce4d 100644 --- a/book/FPLean/Examples/OtherLanguages.lean +++ b/book/FPLean/Examples/OtherLanguages.lean @@ -157,16 +157,16 @@ An anchor consists of a line that contains `ANCHOR:` or `ANCHOR_END:` followed b of the anchor. -/ def anchor? (line : String) : Except String (String × Bool) := do - let mut line := line.trim + let mut line := line.trimAscii line := line.dropWhile (· ≠ 'A') if line.startsWith "ANCHOR:" then - line := line.stripPrefix "ANCHOR:" - line := line.trimLeft - if line.isEmpty then throw "Expected name after `ANCHOR: `" else return (line, true) + line := line.dropPrefix "ANCHOR:" + line := line.trimAsciiStart + if line.isEmpty then throw "Expected name after `ANCHOR: `" else return (line.copy, true) else if line.startsWith "ANCHOR_END:" then - line := line.stripPrefix "ANCHOR_END:" - line := line.trimLeft - if line.isEmpty then throw "Expected name after `ANCHOR_END: `" else return (line, false) + line := line.dropPrefix "ANCHOR_END:" + line := line.trimAsciiStart + if line.isEmpty then throw "Expected name after `ANCHOR_END: `" else return (line.copy, false) else throw s!"Expected `ANCHOR:` or `ANCHOR_END:`, got {line}" private def stringAnchors (s : String) : Except String (String × HashMap String String) := do diff --git a/book/FPLean/FunctorApplicativeMonad/Applicative.lean b/book/FPLean/FunctorApplicativeMonad/Applicative.lean index 6d240c8..05d7293 100644 --- a/book/FPLean/FunctorApplicativeMonad/Applicative.lean +++ b/book/FPLean/FunctorApplicativeMonad/Applicative.lean @@ -126,7 +126,7 @@ There is a value with type {anchorName Pairpure2}`β` in scope (namely {anchorNa def Pair.pure (x : β) : Pair α β := Pair.mk _ x ``` ```anchorError Pairpure2 -don't know how to synthesize placeholder for argument 'first' +don't know how to synthesize placeholder for argument `first` context: β α : Type x : β diff --git a/book/FPLean/GettingToKnow/DatatypesPatterns.lean b/book/FPLean/GettingToKnow/DatatypesPatterns.lean index 8ece6c1..8d51ba0 100644 --- a/book/FPLean/GettingToKnow/DatatypesPatterns.lean +++ b/book/FPLean/GettingToKnow/DatatypesPatterns.lean @@ -301,7 +301,7 @@ Not considering parameter n of evenLoops: it is unchanged in the recursive calls no parameters suitable for structural recursion -well-founded recursion cannot be used, 'evenLoops' does not take any (non-fixed) arguments +well-founded recursion cannot be used, `evenLoops` does not take any (non-fixed) arguments ``` ::: diff --git a/book/FPLean/GettingToKnow/Evaluating.lean b/book/FPLean/GettingToKnow/Evaluating.lean index 169df31..2490e27 100644 --- a/book/FPLean/GettingToKnow/Evaluating.lean +++ b/book/FPLean/GettingToKnow/Evaluating.lean @@ -158,7 +158,7 @@ In particular, the example yields a quite long error message: ```anchorError stringAppendReprFunction -could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type +could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type String → String ``` diff --git a/book/FPLean/GettingToKnow/Polymorphism.lean b/book/FPLean/GettingToKnow/Polymorphism.lean index 800d7e6..c53392f 100644 --- a/book/FPLean/GettingToKnow/Polymorphism.lean +++ b/book/FPLean/GettingToKnow/Polymorphism.lean @@ -438,17 +438,17 @@ However, attempting to test it on the empty list leads to two errors: ``` ```anchorError headNoneBad -don't know how to synthesize implicit argument 'α' - @List.nil ?m.41782 +don't know how to synthesize implicit argument `α` + @List.nil ?m.3 context: -⊢ Type ?u.41779 +⊢ Type ?u.71462 ``` ```anchorError headNoneBad -don't know how to synthesize implicit argument 'α' - @_root_.List.head? ?m.41782 [] +don't know how to synthesize implicit argument `α` + @_root_.List.head? ?m.3 [] context: -⊢ Type ?u.41779 +⊢ Type ?u.71462 ``` ::: @@ -856,7 +856,7 @@ Evaluating it leads to an error: #eval allTools ``` ```anchorError evalAllTools -could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type +could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type List WoodSplittingTool ``` This is because Lean attempts to use code from a built-in table to display a list, but this code demands that display code for {anchorName WoodSplittingTool}`WoodSplittingTool` already exists. diff --git a/book/FPLean/HelloWorld/StepByStep.lean b/book/FPLean/HelloWorld/StepByStep.lean index 5018484..acd7429 100644 --- a/book/FPLean/HelloWorld/StepByStep.lean +++ b/book/FPLean/HelloWorld/StepByStep.lean @@ -261,7 +261,8 @@ def main : IO Unit := runActions from5 Running this program results in the following output: -```anchorInfo countdown5 (module := Examples.HelloWorld) +```commands countdownFromFive "" +$ countdown 5 4 3 diff --git a/book/FPLean/Monads/Class.lean b/book/FPLean/Monads/Class.lean index 46e2ff0..a5814a8 100644 --- a/book/FPLean/Monads/Class.lean +++ b/book/FPLean/Monads/Class.lean @@ -240,30 +240,19 @@ Because this reduces to {anchorTerm IdMore}`α → (α → β) → β`, the seco With the identity monad, {anchorName mapMId}`mapM` becomes equivalent to {anchorName Names (show:=map)}`Functor.map` To call it this way, however, Lean requires a hint that the intended monad is {anchorName mapMId}`Id`: ```anchor mapMId -#eval mapM (m := Id) (· + 1) [1, 2, 3, 4, 5] +def numbers := mapM (m := Id) (do return · + 1) [1, 2, 3, 4, 5] ``` -```anchorInfo mapMId -[2, 3, 4, 5, 6] -``` -Omitting the hint results in an error: -```anchor mapMIdNoHint -#eval mapM (· + 1) [1, 2, 3, 4, 5] -``` -```anchorError mapMIdNoHint -failed to synthesize - HAdd Nat Nat (?m.4 ?m.3) - -Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. -``` -In this error, the application of one metavariable to another indicates that Lean doesn't run the type-level computation backwards. -The return type of the function is expected to be the monad applied to some other type. -Similarly, using {anchorName mapMIdId}`mapM` with a function whose type doesn't provide any specific hints about which monad is to be used results in an “instance problem is stuck” message: +Using {anchorName mapMIdId}`mapM` in a context in which the type doesn't provide any specific hints about which monad is to be used results in an “instance problem is stuck” message: ```anchor mapMIdId -#eval mapM (fun (x : Nat) => x) [1, 2, 3, 4, 5] +def numbers := mapM (do return · + 1) [1, 2, 3, 4, 5] ``` ```anchorError mapMIdId -typeclass instance problem is stuck, it is often due to metavariables - Monad ?m.22785 +typeclass instance problem is stuck + Pure ?m.6 + +Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Pure` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass. + +Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck. ``` ::: diff --git a/book/FPLean/Monads/IO.lean b/book/FPLean/Monads/IO.lean index e05ca97..a870000 100644 --- a/book/FPLean/Monads/IO.lean +++ b/book/FPLean/Monads/IO.lean @@ -112,73 +112,67 @@ Peeling back another layer, {anchorName names}`EIO` is itself defined in terms o ``` ```anchorInfo printEIO def EIO : Type → Type → Type := -fun ε => EStateM ε IO.RealWorld +fun ε α => EST ε IO.RealWorld α ``` -The {anchorName printEStateM}`EStateM` monad includes both errors and state—it's a combination of {anchorName names}`Except` and {anchorName State (module := Examples.Monads)}`State`. -It is defined using another type, {anchorName printEStateMResult}`EStateM.Result`: +The {anchorName printEStateM}`EST` monad includes both errors and state—it's similar to a combination of {anchorName names}`Except` and {anchorName State (module := Examples.Monads)}`State`. +It is defined using another type, {anchorName printEStateMResult}`EST.Out`: ```anchor printEStateM -#print EStateM +#print EST ``` ```anchorInfo printEStateM -def EStateM.{u} : Type u → Type u → Type u → Type u := -fun ε σ α => σ → EStateM.Result ε σ α +def EST : Type → Type → Type → Type := +fun ε σ α => Void σ → EST.Out ε σ α ``` -In other words, a program with type {anchorTerm EStateMNames}`EStateM ε σ α` is a function that accepts an initial state of type {anchorName EStateMNames}`σ` and returns an {anchorTerm EStateMNames}`EStateM.Result ε σ α`. +In other words, a program with type {anchorTerm EStateMNames}`EST ε σ α` is a function that accepts an initial state of type {anchorName EStateMNames}`σ` and returns an {anchorTerm EStateMNames}`EST.Out ε σ α`. +The state is wrapped in the type {anchorName VoidSigma}`Void`, which is an internal primitive that causes a value to be erased from compiled code; {anchorTerm VoidSigma}`Void σ` has the same representation as {anchorName save (module:=Examples.Monads)}`Unit`. -{anchorName EStateMNames}`EStateM.Result` is very much like the definition of {anchorName names}`Except`, with one constructor that indicates a successful termination and one constructor that indicates an error: +{anchorName EStateMNames}`EST.Out` is very much like the definition of {anchorName names}`Except`, with one constructor that indicates a successful termination and one constructor that indicates an error: ```anchor printEStateMResult -#print EStateM.Result +#print EST.Out ``` ```anchorInfo printEStateMResult -inductive EStateM.Result.{u} : Type u → Type u → Type u → Type u +inductive EST.Out : Type → Type → Type → Type number of parameters: 3 constructors: -EStateM.Result.ok : {ε σ α : Type u} → α → σ → EStateM.Result ε σ α -EStateM.Result.error : {ε σ α : Type u} → ε → σ → EStateM.Result ε σ α +EST.Out.ok : {ε σ α : Type} → α → Void σ → EST.Out ε σ α +EST.Out.error : {ε σ α : Type} → ε → Void σ → EST.Out ε σ α ``` -Just like {anchorTerm Except (module:=Examples.Monads)}`Except ε α`, the {anchorName names (show := ok)}`EStateM.Result.ok` constructor includes a result of type {anchorName Except (module:=Examples.Monads)}`α`, and the {anchorName names (show := error)}`EStateM.Result.error` constructor includes an exception of type {anchorName Except (module:=Examples.Monads)}`ε`. +Just like {anchorTerm Except (module:=Examples.Monads)}`Except ε α`, the {anchorName names (show := ok)}`EST.Out.ok` constructor includes a result of type {anchorName Except (module:=Examples.Monads)}`α`, and the {anchorName names (show := error)}`EST.Out.error` constructor includes an exception of type {anchorName Except (module:=Examples.Monads)}`ε`. Unlike {anchorName names}`Except`, both constructors have an additional state field that includes the final state of the computation. -The {anchorName names}`Monad` instance for {anchorTerm names}`EStateM ε σ` requires {anchorName names}`pure` and {anchorName names}`bind`. -Just as with {anchorName State (module:=Examples.Monads)}`State`, the implementation of {anchorName names}`pure` for {anchorName names}`EStateM` accepts an initial state and returns it unchanged, and just as with {anchorName names}`Except`, it returns its argument in the {anchorName names (show := ok)}`EStateM.Result.ok` constructor: +The {anchorName names}`Monad` instance for {anchorTerm names}`EST ε σ` requires {anchorName names}`pure` and {anchorName names}`bind`. +Just as with {anchorName State (module:=Examples.Monads)}`State`, the implementation of {anchorName names}`pure` for {anchorName names}`EST` accepts an initial state and returns it unchanged, and just as with {anchorName names}`Except`, it returns its argument in the {anchorName names (show := ok)}`EST.Out.ok` constructor: ```anchor printEStateMpure -#print EStateM.pure +#print EST.pure ``` ```anchorInfo printEStateMpure -protected def EStateM.pure.{u} : {ε σ α : Type u} → α → EStateM ε σ α := -fun {ε σ α} a s => EStateM.Result.ok a s +protected def EST.pure : {α ε σ : Type} → α → EST ε σ α := +fun {α ε σ} a s => EST.Out.ok a s ``` -{kw}`protected` means that the full name {anchorName printEStateMpure}`EStateM.pure` is needed even if the {anchorName names}`EStateM` namespace has been opened. +{kw}`protected` means that the full name {anchorName printEStateMpure}`EST.pure` is needed even if the {anchorName names}`EST` namespace has been opened. -Similarly, {anchorName names}`bind` for {anchorName names}`EStateM` takes an initial state as an argument. +Similarly, {anchorName names}`bind` for {anchorName names}`EST` takes an initial state as an argument. It passes this initial state to its first action. Like {anchorName names}`bind` for {anchorName names}`Except`, it then checks whether the result is an error. If so, the error is returned unchanged and the second argument to {anchorName names}`bind` remains unused. If the result was a success, then the second argument is applied to both the returned value and to the resulting state. ```anchor printEStateMbind -#print EStateM.bind +#print EST.bind ``` ```anchorInfo printEStateMbind -protected def EStateM.bind.{u} : {ε σ α β : Type u} → EStateM ε σ α → (α → EStateM ε σ β) → EStateM ε σ β := +protected def EST.bind : {ε σ α β : Type} → EST ε σ α → (α → EST ε σ β) → EST ε σ β := fun {ε σ α β} x f s => match x s with - | EStateM.Result.ok a s => f a s - | EStateM.Result.error e s => EStateM.Result.error e s + | EST.Out.ok a s => f a s + | EST.Out.error e s => EST.Out.error e s ``` Putting all of this together, {anchorName names}`IO` is a monad that tracks state and errors at the same time. The collection of available errors is that given by the datatype {anchorName printIOError}`IO.Error`, which has constructors that describe many things that can go wrong in a program. -The state is a type that represents the real world, called {anchorTerm printRealWorld}`IO.RealWorld`. +The state is a type that represents the real world, called {anchorTerm RealWorld}`IO.RealWorld`. Each basic {anchorName names}`IO` action receives this real world and returns another one, paired either with an error or a result. In {anchorName names}`IO`, {anchorName names}`pure` returns the world unchanged, while {anchorName names}`bind` passes the modified world from one action into the next action. Because the entire universe doesn't fit in a computer's memory, the world being passed around is just a representation. So long as world tokens are not re-used, the representation is safe. -This means that world tokens do not need to contain any data at all: -```anchor printRealWorld -#print IO.RealWorld -``` -```anchorInfo printRealWorld -def IO.RealWorld : Type := -Unit -``` +The type {anchorTerm RealWorld}`IO.RealWorld` is a trivial primitive type that does not need any representation at all, because it is only used inside of {anchorName VoidSigma}`Void`. diff --git a/book/FPLean/ProgramsProofs/ArraysTermination.lean b/book/FPLean/ProgramsProofs/ArraysTermination.lean index 255046e..ec82889 100644 --- a/book/FPLean/ProgramsProofs/ArraysTermination.lean +++ b/book/FPLean/ProgramsProofs/ArraysTermination.lean @@ -384,7 +384,8 @@ def findHelper (arr : Array α) (p : α → Bool) else none ``` -Adding a question mark to {kw}`termination_by` (that is, using {kw}`termination_by?`) causes Lean to explicitly suggest the measure that it chose: +Adding a question mark to {kw}`termination_by` (that is, using {kw}`termination_by?`) causes Lean to explicitly suggest the measure that it chose. +Clicking {lit}`[apply]` replaces {kw}`termination_by?` with the suggested measure: ```anchor ArrayFindHelperSugg def findHelper (arr : Array α) (p : α → Bool) (i : Nat) : Option (Nat × α) := @@ -397,7 +398,8 @@ def findHelper (arr : Array α) (p : α → Bool) termination_by? ``` ```anchorInfo ArrayFindHelperSugg -Try this: termination_by arr.size - i +Try this: + [apply] termination_by arr.size - i ``` Not all termination arguments are as quite as simple as this one. diff --git a/book/FPLean/TacticsInductionProofs.lean b/book/FPLean/TacticsInductionProofs.lean index 4fb901f..bbdb632 100644 --- a/book/FPLean/TacticsInductionProofs.lean +++ b/book/FPLean/TacticsInductionProofs.lean @@ -129,7 +129,7 @@ theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by | succ n ih lots of names => skip ``` ```anchorError plusR_ind_zero_left_3 -Too many variable names provided at alternative 'succ': 5 provided, but 2 expected +Too many variable names provided at alternative `succ`: 5 provided, but 2 expected ``` Focusing on the base case, the {kw}`rfl` tactic works just as well inside of the {kw}`induction` tactic as it does in a recursive function: diff --git a/book/FPLean/TypeClasses/OutParams.lean b/book/FPLean/TypeClasses/OutParams.lean index 9bff7a7..a691729 100644 --- a/book/FPLean/TypeClasses/OutParams.lean +++ b/book/FPLean/TypeClasses/OutParams.lean @@ -82,10 +82,14 @@ When attempting to use these instances with {kw}`#eval`, an error occurs: #eval toString (HPlus.hPlus (3 : Pos) (5 : Nat)) ``` ```anchorError hPlusOops -typeclass instance problem is stuck, it is often due to metavariables - ToString ?m.14563 +typeclass instance problem is stuck + HPlus Pos Nat ?m.6 + +Note: Lean will not try to resolve this typeclass instance problem because the third type argument to `HPlus` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass. + +Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck. ``` -This happens because there is a metavariable in the type, and Lean has no way to solve it. +The message indicates that this happens because there is a metavariable in the type, and Lean has no way to solve it. ::: As discussed in {ref "polymorphism"}[the initial description of polymorphism], metavariables represent unknown parts of a program that could not be inferred. diff --git a/book/lake-manifest.json b/book/lake-manifest.json index 132d071..6ecf6ad 100644 --- a/book/lake-manifest.json +++ b/book/lake-manifest.json @@ -5,17 +5,27 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b1cdd66be1f055926796aa804fdc13c9e9ac17c6", + "rev": "ea44a4d919a4570055bf53171ea4d8a8919cde84", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, "scope": "", - "rev": "66aefec2852d3e229517694e642659f316576591", + "rev": "38ac5945d744903ffcc473ce1030223991b11cf6", "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +35,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "57f4e6c99a4132d54a2105dec21c2e3c2af98b15", + "rev": "eb77622e97e942ba2cfe02f60637705fc2d9481b", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/book/lakefile.lean b/book/lakefile.lean index 8b0c898..04ea8ea 100644 --- a/book/lakefile.lean +++ b/book/lakefile.lean @@ -15,11 +15,14 @@ require verso from git "https://github.com/leanprover/verso.git"@"main" private def examplePath : System.FilePath := "../examples" private def lakeVars := - #["LAKE", "LAKE_HOME", "LAKE_PKG_URL_MAP", - "LEAN_SYSROOT", "LEAN_AR", "LEAN_PATH", "LEAN_SRC_PATH", + #["LAKE", "LAKE_HOME", "LAKE_PKG_URL_MAP", "LAKE_CACHE_DIR", + "LEAN", "LEAN_SYSROOT", "LEAN_AR", "LEAN_PATH", "LEAN_SRC_PATH", "LEAN_GITHASH", "ELAN_TOOLCHAIN", "DYLD_LIBRARY_PATH", "LD_LIBRARY_PATH"] +private def fixPath (path : System.SearchPath) : String := + path |>.map (·.toString) |>.filter (!·.contains ".lake") |> System.SearchPath.separator.toString.intercalate + input_dir examples where path := examplePath text := true @@ -32,7 +35,11 @@ input_dir exampleBinaries where target buildExamples (pkg) : Unit := do let exs ← examples.fetch - let exBins ← examples.fetch + let exBins ← exampleBinaries.fetch + let toolchainFile := examplePath / "lean-toolchain" + let toolchain ← IO.FS.readFile toolchainFile + let toolchain := toolchain.trimAscii |>.dropPrefix "leanprover/lean4:" |>.dropPrefix "v" |>.copy + addPureTrace toolchain exBins.bindM fun binFiles => do for file in binFiles do if file.extension.isNone || file.extension.isEqSome System.FilePath.exeExtension then @@ -44,12 +51,20 @@ target buildExamples (pkg) : Unit := do list := list ++ s!"{file}\n" buildFileUnlessUpToDate' (pkg.buildDir / "examples-built") (text := true) do Lake.logInfo s!"Building examples in {examplePath}" - let out ← captureProc { - cmd := "lake", - args := #["build"], + let mut out := "" + let path := fixPath (← getSearchPath "PATH") + out := out ++ (← captureProc { + cmd := "elan", + args := #["run", "--install", toolchain, "lake", "build"], + cwd := examplePath, + env := lakeVars.map (·, none) ++ #[("PATH", some path)] + }) + out := out ++ (← captureProc { + cmd := "elan", + args := #["run", "--install", toolchain, "lake", "build", "subverso-extract-mod"], cwd := examplePath, - env := lakeVars.map (·, none) - } + env := lakeVars.map (·, none) ++ #[("PATH", some path)] + }) IO.FS.createDirAll pkg.buildDir IO.FS.writeFile (pkg.buildDir / "examples-built") (list ++ "--- Output ---\n" ++ out) diff --git a/book/lean-toolchain b/book/lean-toolchain index 137937a..bd19bde 100644 --- a/book/lean-toolchain +++ b/book/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.25.0-rc2 \ No newline at end of file +leanprover/lean4:v4.27.0-rc1 diff --git a/book/verso-sources.json b/book/verso-sources.json index 166c291..468d7f6 100644 --- a/book/verso-sources.json +++ b/book/verso-sources.json @@ -2,7 +2,7 @@ "version": 0, "sources": { "manual": { - "root": "https://lean-lang.org/doc/reference/4.23.0/", + "root": "https://lean-lang.org/doc/reference/4.26.0/", "updateFrequency": "manual", "shortName": "ref", "longName": "Lean Language Reference" diff --git a/examples/ExampleSupport.lean b/examples/ExampleSupport.lean index 415b670..c64bd3c 100644 --- a/examples/ExampleSupport.lean +++ b/examples/ExampleSupport.lean @@ -293,7 +293,7 @@ def elabCheckMsgs : CommandElab | `(command| $[$dc?:docComment]? #check_msgs%$tk $(spec?)? in $cmd) => do let expected : String := (← dc?.mapM (getDocStringText ·)).getD "" |>.trim |> removeTrailingWhitespaceMarker - let (whitespace, ordering, specFn) ← parseGuardMsgsSpec spec? + let {whitespace, ordering, filterFn, reportPositions := _} ← parseGuardMsgsSpec spec? let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} }) -- do not forward snapshot as we don't want messages assigned to it to leak outside withReader ({ · with snap? := none }) do @@ -307,7 +307,7 @@ def elabCheckMsgs : CommandElab let mut toCheck : MessageLog := .empty let mut toPassthrough : MessageLog := .empty for msg in msgs.toList do - match specFn msg with + match filterFn msg with | .check => toCheck := toCheck.add msg | .drop => pure () | .pass => toPassthrough := toPassthrough.add msg @@ -321,7 +321,7 @@ def elabCheckMsgs : CommandElab -- Failed. Put all the messages back on the message log and add an error modify fun st => { st with messages := initMsgs ++ msgs } let feedback := - let diff := Diff.diff (expected.split (· == '\n')).toArray (res.split (· == '\n')).toArray + let diff := Diff.diff (expected.splitToList (· == '\n')).toArray (res.splitToList (· == '\n')).toArray Diff.linesToString diff logErrorAt tk m!"❌️ Docstring on `#check_msgs` does not match generated message:\n\n{feedback}" diff --git a/examples/Examples/Classes.lean b/examples/Examples/Classes.lean index d4dd805..d11dd78 100644 --- a/examples/Examples/Classes.lean +++ b/examples/Examples/Classes.lean @@ -806,8 +806,12 @@ instance : HPlus Pos Nat Pos where -- ANCHOR_END: HPlusInstances /-- -error: typeclass instance problem is stuck, it is often due to metavariables - ToString ?m.14563 +error: typeclass instance problem is stuck + HPlus Pos Nat ?m.6 + +Note: Lean will not try to resolve this typeclass instance problem because the third type argument to `HPlus` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass. + +Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck. -/ #check_msgs in -- ANCHOR: hPlusOops @@ -1376,7 +1380,7 @@ example : Functor.map (· + 5) [1, 2, 3] = [6, 7, 8] := rfl -- ANCHOR_END: mapList -- ANCHOR: mapOption -example : Functor.map toString (some (List.cons 5 List.nil)) = some "[5]" := rfl +example : Functor.map toString (some (List.cons 5 List.nil)) = some "[5]" := by decide +native -- TODO verify text and perhaps replace -- ANCHOR_END: mapOption -- ANCHOR: mapListList @@ -1388,7 +1392,7 @@ example : (· + 5) <$> [1, 2, 3] = [6, 7, 8] := rfl -- ANCHOR_END: mapInfixList -- ANCHOR: mapInfixOption -example : toString <$> (some (List.cons 5 List.nil)) = some "[5]" := rfl +example : toString <$> (some (List.cons 5 List.nil)) = some "[5]" := by decide +native -- ANCHOR_END: mapInfixOption -- ANCHOR: mapInfixListList diff --git a/examples/Examples/DependentTypes/IndicesParameters.lean b/examples/Examples/DependentTypes/IndicesParameters.lean index 7079df4..9b45162 100644 --- a/examples/Examples/DependentTypes/IndicesParameters.lean +++ b/examples/Examples/DependentTypes/IndicesParameters.lean @@ -42,7 +42,7 @@ The provided argument 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. +Note: The value of parameter `α` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary. -/ #check_msgs in -- ANCHOR: WithParameterBeforeColonDifferentNames @@ -59,7 +59,7 @@ The provided argument 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. +Note: The value of parameter `α` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary. -/ #check_msgs in -- ANCHOR: WithNamedIndex @@ -99,7 +99,7 @@ The provided argument is not definitionally equal to the expected parameter n -Note: The value of parameter 'n' must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary. +Note: The value of parameter `n` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary. -/ #check_msgs in -- ANCHOR: NatParamFour diff --git a/examples/Examples/FunctorApplicativeMonad.lean b/examples/Examples/FunctorApplicativeMonad.lean index 94b8728..f8b7b31 100644 --- a/examples/Examples/FunctorApplicativeMonad.lean +++ b/examples/Examples/FunctorApplicativeMonad.lean @@ -470,8 +470,8 @@ def Pair.pure (x : β) : Pair α β := _ stop discarding -/-- error: -don't know how to synthesize placeholder for argument 'first' +/-- +error: don't know how to synthesize placeholder for argument `first` context: β α : Type x : β diff --git a/examples/Examples/HelloWorld.lean b/examples/Examples/HelloWorld.lean index 4c7fe80..c9291da 100644 --- a/examples/Examples/HelloWorld.lean +++ b/examples/Examples/HelloWorld.lean @@ -101,9 +101,18 @@ def runActions : List (IO Unit) → IO Unit def main : IO Unit := runActions from5 -- ANCHOR_END: main --- ANCHOR: countdown5 +/-- +info: 5 +4 +3 +2 +1 +Blast off! +-/ +#check_msgs in +-- ANCHOR: countdownFromFive #eval main --- ANCHOR_END: countdown5 +-- ANCHOR_END: countdownFromFive evaluation steps : IO Unit {{{ evalMain }}} -- ANCHOR: evalMain diff --git a/examples/Examples/Induction.lean b/examples/Examples/Induction.lean index be9d9ae..a1d596b 100644 --- a/examples/Examples/Induction.lean +++ b/examples/Examples/Induction.lean @@ -71,7 +71,7 @@ error: unsolved goals case zero ⊢ 0 = Nat.plusR 0 0 --- -error: Too many variable names provided at alternative 'succ': 5 provided, but 2 expected +error: Too many variable names provided at alternative `succ`: 5 provided, but 2 expected --- error: unsolved goals case succ diff --git a/examples/Examples/Intro.lean b/examples/Examples/Intro.lean index e13456c..3ae2dde 100644 --- a/examples/Examples/Intro.lean +++ b/examples/Examples/Intro.lean @@ -56,7 +56,7 @@ String.append "it is " "no" end evaluation steps /-- -error: could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type +error: could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type String → String -/ #check_msgs in @@ -909,8 +909,8 @@ false -- ANCHOR_END: _something_more -/-- error: -fail to show termination for +/-- +error: fail to show termination for evenLoops with errors failed to infer structural recursion: @@ -918,7 +918,7 @@ Not considering parameter n of evenLoops: it is unchanged in the recursive calls no parameters suitable for structural recursion -well-founded recursion cannot be used, 'evenLoops' does not take any (non-fixed) arguments +well-founded recursion cannot be used, `evenLoops` does not take any (non-fixed) arguments -/ #check_msgs in -- ANCHOR: evenLoops @@ -1442,15 +1442,15 @@ some 2 -- ANCHOR_END: headSome /-- -error: don't know how to synthesize implicit argument 'α' - @_root_.List.head? ?m.41386 [] +error: don't know how to synthesize implicit argument `α` + @_root_.List.head? ?m.3 [] context: -⊢ Type ?u.41383 +⊢ Type ?u.70597 --- -error: don't know how to synthesize implicit argument 'α' - @List.nil ?m.41386 +error: don't know how to synthesize implicit argument `α` + @List.nil ?m.3 context: -⊢ Type ?u.41383 +⊢ Type ?u.70597 -/ #check_msgs in -- ANCHOR: headNoneBad @@ -1458,15 +1458,15 @@ context: -- ANCHOR_END: headNoneBad /-- -error: don't know how to synthesize implicit argument 'α' - @_root_.List.head? ?m.41395 [] +error: don't know how to synthesize implicit argument `α` + @_root_.List.head? ?m.3 [] context: -⊢ Type ?u.41392 +⊢ Type ?u.70606 --- -error: don't know how to synthesize implicit argument 'α' - @List.nil ?m.41395 +error: don't know how to synthesize implicit argument `α` + @List.nil ?m.3 context: -⊢ Type ?u.41392 +⊢ Type ?u.70606 -/ #check_msgs in -- ANCHOR: headNoneBad2 @@ -1740,7 +1740,7 @@ def allTools : List WoodSplittingTool := [ -- ANCHOR_END: allTools /-- -error: could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type +error: could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type List WoodSplittingTool -/ #check_msgs in @@ -2069,7 +2069,7 @@ def halve : Nat → Nat example : Explicit.halve = halve := by funext x - fun_induction halve x <;> simp [halve, Explicit.halve, *] + fun_induction halve x <;> simp [Explicit.halve, *] namespace Oops /-- @@ -2275,7 +2275,7 @@ error: failed to synthesize Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. --- -info: toString "three fives is " ++ sorry ++ toString "" : String +info: toString "three fives is " ++ sorry : String -/ #check_msgs in -- ANCHOR: interpolationOops diff --git a/examples/Examples/Monads/Class.lean b/examples/Examples/Monads/Class.lean index 96de96f..3bceddb 100644 --- a/examples/Examples/Monads/Class.lean +++ b/examples/Examples/Monads/Class.lean @@ -269,36 +269,42 @@ def saveIfEven (i : Int) : WithLog Int Int := #eval mapM saveIfEven [1, 2, 3, 4, 5] -- ANCHOR_END: mapMsaveIfEven -/-- info: -[2, 3, 4, 5, 6] --/ +discarding #check_msgs in -- ANCHOR: mapMId -#eval mapM (m := Id) (· + 1) [1, 2, 3, 4, 5] +def numbers := mapM (m := Id) (do return · + 1) [1, 2, 3, 4, 5] -- ANCHOR_END: mapMId +stop discarding - - +discarding /-- -error: failed to synthesize - HAdd Nat Nat (?m.4 ?m.3) +error: typeclass instance problem is stuck + Pure ?m.6 -Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. +Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Pure` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass. + +Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck. -/ #check_msgs in -- ANCHOR: mapMIdNoHint -#eval mapM (· + 1) [1, 2, 3, 4, 5] +def numbers := mapM (do return · + 1) [1, 2, 3, 4, 5] -- ANCHOR_END: mapMIdNoHint +stop discarding +discarding +/-- +error: typeclass instance problem is stuck + Pure ?m.6 -/-- error: -typeclass instance problem is stuck, it is often due to metavariables - Monad ?m.4319 +Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Pure` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass. + +Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck. -/ #check_msgs in -- ANCHOR: mapMIdId -#eval mapM (fun (x : Nat) => x) [1, 2, 3, 4, 5] +def numbers := mapM (do return · + 1) [1, 2, 3, 4, 5] -- ANCHOR_END: mapMIdId +stop discarding end MyListStuff diff --git a/examples/Examples/Monads/IO.lean b/examples/Examples/Monads/IO.lean index fdbb6f0..de2213b 100644 --- a/examples/Examples/Monads/IO.lean +++ b/examples/Examples/Monads/IO.lean @@ -9,10 +9,10 @@ local instance : Monad IO where universe u example {ε} {α}:= EIO ε α -- ANCHOR: EStateMNames -example {ε} {α} {σ} := EStateM ε σ α → EStateM.Result ε σ α +example {ε} {α} {σ} := EST ε σ α → EST.Out ε σ α -- ANCHOR_END: EStateMNames -example := @EStateM.Result.ok -example := @EStateM.Result.error +example := @EST.Out.ok +example := @EST.Out.error example {α}:= BaseIO α example {ε} := Except ε example := Type u @@ -99,65 +99,62 @@ IO.Error.userError : String → IO.Error /-- info: def EIO : Type → Type → Type := -fun ε => EStateM ε IO.RealWorld +fun ε α => EST ε IO.RealWorld α -/ #check_msgs in -- ANCHOR: printEIO #print EIO -- ANCHOR_END: printEIO +-- ANCHOR: VoidSigma +example {σ} := Void σ +-- ANCHOR_END: VoidSigma + +-- ANCHOR: RealWorld +example := IO.RealWorld +-- ANCHOR_END: RealWorld /-- info: -def EStateM.{u} : Type u → Type u → Type u → Type u := -fun ε σ α => σ → EStateM.Result ε σ α +def EST : Type → Type → Type → Type := +fun ε σ α => Void σ → EST.Out ε σ α -/ #check_msgs in -- ANCHOR: printEStateM -#print EStateM +#print EST -- ANCHOR_END: printEStateM /-- info: -inductive EStateM.Result.{u} : Type u → Type u → Type u → Type u +inductive EST.Out : Type → Type → Type → Type number of parameters: 3 constructors: -EStateM.Result.ok : {ε σ α : Type u} → α → σ → EStateM.Result ε σ α -EStateM.Result.error : {ε σ α : Type u} → ε → σ → EStateM.Result ε σ α +EST.Out.ok : {ε σ α : Type} → α → Void σ → EST.Out ε σ α +EST.Out.error : {ε σ α : Type} → ε → Void σ → EST.Out ε σ α -/ #check_msgs in -- ANCHOR: printEStateMResult -#print EStateM.Result +#print EST.Out -- ANCHOR_END: printEStateMResult /-- info: -protected def EStateM.pure.{u} : {ε σ α : Type u} → α → EStateM ε σ α := -fun {ε σ α} a s => EStateM.Result.ok a s +protected def EST.pure : {α ε σ : Type} → α → EST ε σ α := +fun {α ε σ} a s => EST.Out.ok a s -/ #check_msgs in -- ANCHOR: printEStateMpure -#print EStateM.pure +#print EST.pure -- ANCHOR_END: printEStateMpure /-- info: -protected def EStateM.bind.{u} : {ε σ α β : Type u} → EStateM ε σ α → (α → EStateM ε σ β) → EStateM ε σ β := +protected def EST.bind : {ε σ α β : Type} → EST ε σ α → (α → EST ε σ β) → EST ε σ β := fun {ε σ α β} x f s => match x s with - | EStateM.Result.ok a s => f a s - | EStateM.Result.error e s => EStateM.Result.error e s + | EST.Out.ok a s => f a s + | EST.Out.error e s => EST.Out.error e s -/ #check_msgs in -- ANCHOR: printEStateMbind -#print EStateM.bind +#print EST.bind -- ANCHOR_END: printEStateMbind - - -/-- info: -def IO.RealWorld : Type := -Unit --/ -#check_msgs in --- ANCHOR: printRealWorld -#print IO.RealWorld --- ANCHOR_END: printRealWorld diff --git a/examples/Examples/ProgramsProofs/Arrays.lean b/examples/Examples/ProgramsProofs/Arrays.lean index 61ef60e..d1e9b5c 100644 --- a/examples/Examples/ProgramsProofs/Arrays.lean +++ b/examples/Examples/ProgramsProofs/Arrays.lean @@ -307,8 +307,9 @@ def Array.find (arr : Array α) (p : α → Bool) : -- ANCHOR_END: ArrayFind namespace Huh -/-- info: -Try this: termination_by arr.size - i +/-- +info: Try this: + [apply] termination_by arr.size - i -/ #check_msgs in -- ANCHOR: ArrayFindHelperSugg diff --git a/examples/lake-manifest.json b/examples/lake-manifest.json index 4a488fe..6379fb3 100644 --- a/examples/lake-manifest.json +++ b/examples/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "767f10408ca8abe29a15add2bf111eefdd9522b2", + "rev": "eb77622e97e942ba2cfe02f60637705fc2d9481b", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/examples/lakefile.lean b/examples/lakefile.lean index e417df9..54768f4 100644 --- a/examples/lakefile.lean +++ b/examples/lakefile.lean @@ -48,6 +48,11 @@ lean_exe examples { root := `Main } +@[default_target] +lean_exe countdown { + root := `Examples.HelloWorld +} + @[default_target] lean_lib DougLib where srcDir := "douglib" diff --git a/examples/lean-toolchain b/examples/lean-toolchain index f434439..4a5353b 100644 --- a/examples/lean-toolchain +++ b/examples/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.23.0 +leanprover/lean4:4.26.0