feat: add #guard_panic command and substring option for #guard_msgs (#11908)
This PR adds two features to the message testing commands:
## `#guard_panic` command
A new `#guard_panic` command that succeeds if the nested command
produces a panic message. Unlike `#guard_msgs`, it does not check the
exact message content, only that a panic occurred.
This is useful for testing commands that are expected to panic, where
the exact panic message text may be volatile. It is particularly useful
when minimizing a panic discovered "in the wild", while ensuring the
panic behaviour is preserved.
## `substring := true` option for `#guard_msgs`
Adds a `substring := true` option to `#guard_msgs` that checks if the
docstring appears as a substring of the output (after whitespace
normalization), rather than requiring an exact match. This is useful
when you only care about part of the message.
Example:
```lean
/-- Unknown identifier -/
#guard_msgs (substring := true) in
example : α := x
```
## Refactoring
Also refactors `runAndCollectMessages` as a shared helper function used
by both `#guard_msgs` and `#guard_panic`.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This commit is contained in:
Kim Morrison
GitHub
parent
8154453bb5
commit
a6ed0d640d
3 changed files with 144 additions and 19 deletions
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue