diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 1b5126a68a..ca6186ee3c 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -782,9 +782,16 @@ Position reporting for `#guard_msgs`: -/ syntax guardMsgsPositions := &"positions" " := " guardMsgsPositionsArg +/-- +Substring matching for `#guard_msgs`: +- `substring := true` checks that the docstring appears as a substring of the output. +- `substring := false` (the default) requires exact matching (modulo whitespace normalization). +-/ +syntax guardMsgsSubstring := &"substring" " := " (&"true" <|> &"false") + set_option linter.missingDocs false in syntax guardMsgsSpecElt := - guardMsgsFilter <|> guardMsgsWhitespace <|> guardMsgsOrdering <|> guardMsgsPositions + guardMsgsFilter <|> guardMsgsWhitespace <|> guardMsgsOrdering <|> guardMsgsPositions <|> guardMsgsSubstring set_option linter.missingDocs false in syntax guardMsgsSpec := "(" guardMsgsSpecElt,* ")" @@ -860,6 +867,11 @@ Position reporting: `#guard_msgs` appears. - `positions := false` does not report position info. +Substring matching: +- `substring := true` checks that the docstring appears as a substring of the output + (after whitespace normalization). This is useful when you only care about part of the message. +- `substring := false` (the default) requires exact matching (modulo whitespace normalization). + For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. @@ -873,6 +885,13 @@ The top-level command elaborator only runs the linters if `#guard_msgs` is not p syntax (name := guardMsgsCmd) (plainDocComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command +/-- +`#guard_panic in cmd` runs `cmd` and succeeds if the command produces a panic message. +This is useful for testing that a command panics without matching the exact (volatile) panic text. +-/ +syntax (name := guardPanicCmd) + "#guard_panic" " in" ppLine command : command + /-- Format and print the info trees for a given command. This is mostly useful for debugging info trees. diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean index 92c3ca20db..2d30fd9b83 100644 --- a/src/Lean/Elab/GuardMsgs.lean +++ b/src/Lean/Elab/GuardMsgs.lean @@ -11,10 +11,13 @@ public import Lean.Server.CodeActions.Attr public section -/-! `#guard_msgs` command for testing commands +/-! `#guard_msgs` and `#guard_panic` commands for testing commands -This module defines a command to test that another command produces the expected messages. -See the docstring on the `#guard_msgs` command. +This module defines commands to test that other commands produce expected messages: +- `#guard_msgs`: tests that a command produces exactly the expected messages +- `#guard_panic`: tests that a command produces a panic message (without checking the exact text) + +See the docstrings on the individual commands. -/ open Lean Parser.Tactic Elab Command @@ -88,6 +91,8 @@ structure GuardMsgsSpec where ordering : MessageOrdering := .exact /-- Whether to report position information. -/ reportPositions : Bool := false + /-- Whether to check for substring containment instead of exact match. -/ + substring : Bool := false def parseGuardMsgsFilterAction (action? : Option (TSyntax ``guardMsgsFilterAction)) : CommandElabM FilterSpec := do @@ -118,7 +123,7 @@ def parseGuardMsgsSpec (spec? : Option (TSyntax ``guardMsgsSpec)) : CommandElabM | `(guardMsgsSpec| ($[$elts:guardMsgsSpecElt],*)) => pure elts | _ => throwUnsupportedSyntax let defaultFilterFn := cfg.filterFn - let mut { whitespace, ordering, reportPositions .. } := cfg + let mut { whitespace, ordering, reportPositions, substring .. } := cfg let mut p? : Option (Message → FilterSpec) := none let pushP (action : FilterSpec) (msgP : Message → Bool) (p? : Option (Message → FilterSpec)) (msg : Message) : FilterSpec := @@ -136,9 +141,11 @@ def parseGuardMsgsSpec (spec? : Option (TSyntax ``guardMsgsSpec)) : CommandElabM | `(guardMsgsSpecElt| ordering := sorted) => ordering := .sorted | `(guardMsgsSpecElt| positions := true) => reportPositions := true | `(guardMsgsSpecElt| positions := false) => reportPositions := false + | `(guardMsgsSpecElt| substring := true) => substring := true + | `(guardMsgsSpecElt| substring := false) => substring := false | _ => throwUnsupportedSyntax let filterFn := p?.getD defaultFilterFn - return { filterFn, whitespace, ordering, reportPositions } + return { filterFn, whitespace, ordering, reportPositions, substring } /-- An info tree node corresponding to a failed `#guard_msgs` invocation, used for code action support. -/ @@ -176,22 +183,31 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S | .exact => msgs | .sorted => msgs |>.toArray.qsort (· < ·) |>.toList +/-- +Runs a command and collects all messages (sync and async) it produces. +Clears the snapshot tasks after collection. +Returns the collected messages. +-/ +def runAndCollectMessages (cmd : Syntax) : CommandElabM MessageLog := do + -- do not forward snapshot as we don't want messages assigned to it to leak outside + withReader ({ · with snap? := none }) do + -- The `#guard_msgs` command is special-cased in `elabCommandTopLevel` to ensure linters only run once. + elabCommandTopLevel cmd + -- collect sync and async messages + let msgs := (← get).messages ++ + (← get).snapshotTasks.foldl (· ++ ·.get.getAll.foldl (· ++ ·.diagnostics.msgLog) .empty) .empty + -- clear async messages as we don't want them to leak outside + modify ({ · with snapshotTasks := #[] }) + return msgs + @[builtin_command_elab Lean.guardMsgsCmd] def elabGuardMsgs : CommandElab | `(command| $[$dc?:docComment]? #guard_msgs%$tk $(spec?)? in $cmd) => do let expected : String := (← dc?.mapM (getDocStringText ·)).getD "" |>.trimAscii |>.copy |> removeTrailingWhitespaceMarker - let { whitespace, ordering, filterFn, reportPositions } ← parseGuardMsgsSpec spec? - -- do not forward snapshot as we don't want messages assigned to it to leak outside - withReader ({ · with snap? := none }) do - -- The `#guard_msgs` command is special-cased in `elabCommandTopLevel` to ensure linters only run once. - elabCommandTopLevel cmd - -- collect sync and async messages - let msgs := (← get).messages ++ - (← get).snapshotTasks.foldl (· ++ ·.get.getAll.foldl (· ++ ·.diagnostics.msgLog) {}) {} - -- clear async messages as we don't want them to leak outside - modify ({ · with snapshotTasks := #[] }) - let mut toCheck : MessageLog := .empty - let mut toPassthrough : MessageLog := .empty + let { whitespace, ordering, filterFn, reportPositions, substring } ← parseGuardMsgsSpec spec? + let msgs ← runAndCollectMessages cmd + let mut toCheck : MessageLog := MessageLog.empty + let mut toPassthrough : MessageLog := MessageLog.empty for msg in msgs.toList do if msg.isSilent then continue @@ -207,7 +223,13 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S let strings ← toCheck.toList.mapM (messageToString · reportPos?) let strings := ordering.apply strings let res := "---\n".intercalate strings |>.trimAscii |>.copy - if whitespace.apply expected == whitespace.apply res then + let passed := if substring then + -- Substring mode: check that expected appears within res (after whitespace normalization) + (whitespace.apply res).contains (whitespace.apply expected) + else + -- Exact mode: check equality (after whitespace normalization) + whitespace.apply expected == whitespace.apply res + if passed then -- Passed. Only put toPassthrough messages back on the message log modify fun st => { st with messages := toPassthrough } else @@ -257,4 +279,24 @@ def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do } }] +@[builtin_command_elab Lean.guardPanicCmd] def elabGuardPanic : CommandElab + | `(command| #guard_panic in $cmd) => do + let msgs ← runAndCollectMessages cmd + -- Check if any message contains "PANIC" + let mut foundPanic := false + for msg in msgs.toList do + if msg.isSilent then continue + let msgStr ← msg.data.toString + if msgStr.contains "PANIC" then + foundPanic := true + break + if foundPanic then + -- Success - clear the messages so they don't appear + modify fun st => { st with messages := MessageLog.empty } + else + -- Failed - put the messages back and add our error + modify fun st => { st with messages := msgs } + logError "Expected a PANIC but none was found" + | _ => throwUnsupportedSyntax + end Lean.Elab.Tactic.GuardMsgs diff --git a/tests/lean/run/guard_msgs.lean b/tests/lean/run/guard_msgs.lean index fa080a24c9..c0f46b2310 100644 --- a/tests/lean/run/guard_msgs.lean +++ b/tests/lean/run/guard_msgs.lean @@ -399,3 +399,67 @@ info: foo run_cmd logInfo m!"foo" end Positions + +section GuardPanic + +/-! Tests for #guard_panic -/ + +-- Test that #guard_panic succeeds when a panic occurs +#guard_panic in +run_cmd (panic! "test panic" : Lean.Elab.Command.CommandElabM Unit) + +-- Test that #guard_panic fails when no panic occurs +/-- +info: Nat : Type +--- +error: Expected a PANIC but none was found +-/ +#guard_msgs in +#guard_panic in +#check Nat + +-- Test that #guard_panic clears messages on success (no output expected) +#guard_msgs in +#guard_panic in +run_cmd (panic! "this message should not appear" : Lean.Elab.Command.CommandElabM Unit) + +end GuardPanic + +section Substring + +/-! Tests for substring matching -/ + +-- Test that substring mode matches when expected is a substring of actual +/-- Unknown identifier -/ +#guard_msgs (substring := true) in +example : α := x + +-- Test that substring mode works with whitespace normalization +/-- Unknown identifier -/ +#guard_msgs (substring := true, whitespace := lax) in +example : α := x + +-- Test that substring mode fails when expected is not a substring +/-- +error: Unknown identifier `x` +--- +error: ❌️ Docstring on `#guard_msgs` does not match generated message: + +error: Unknown identifier `x` +-/ +#guard_msgs in +/-- This text does not appear -/ +#guard_msgs (substring := true) in +example : α := x + +-- Test that substring mode can match a middle portion +/-- identifier -/ +#guard_msgs (substring := true) in +example : α := x + +-- Test explicit substring := false (should behave like default) +/-- error: Unknown identifier `x` -/ +#guard_msgs (substring := false) in +example : α := x + +end Substring