feat: whitespace and message ordering configurations for #guard_msgs

RELEASES.md

@@ -61,6 +61,11 @@ v4.8.0 (development in progress)
   to enable pretty printing function applications using generalized field notation.
   Field notation can now be disabled function-by-function using the `@[pp_nodot]` attribute.
 
+* The `#guard_msgs` command now has options to change whitespace normalization and sensitivity to message ordering.
+  For example, `#guard_msgs (whitespace := lax) in cmd` collapses whitespace before checking messages,
+  and `#guard_msgs (ordering := sorted) in cmd` sorts the messages in lexicographic order before checking.
+  PR [#3883](https://github.com/leanprover/lean4/pull/3883).
+
 Breaking changes:
 
 * Automatically generated equational theorems are now named using suffix `.eq_<idx>` instead of `._eq_<idx>`, and `.def` instead of `._unfold`. Example:

src/Init/Notation.lean

@@ -552,15 +552,52 @@ except that it doesn't print an empty diagnostic.
 -/
 syntax (name := runMeta) "run_meta " doSeq : command
 
-/-- Element that can be part of a `#guard_msgs` specification. -/
-syntax guardMsgsSpecElt := &"drop"? (&"info" <|> &"warning" <|> &"error" <|> &"all")
+set_option linter.missingDocs false in
+syntax guardMsgsFilterSeverity := &"info" <|> &"warning" <|> &"error" <|> &"all"
 
-/-- Specification for `#guard_msgs` command. -/
+/--
+A message filter specification for `#guard_msgs`.
+- `info`, `warning`, `error`: capture messages with the given severity level.
+- `all`: capture all messages (the default).
+- `drop info`, `drop warning`, `drop error`: drop messages with the given severity level.
+- `drop all`: drop every message.
+These filters are processed in left-to-right order.
+-/
+syntax guardMsgsFilter := &"drop"? guardMsgsFilterSeverity
+
+set_option linter.missingDocs false in
+syntax guardMsgsWhitespaceArg := &"exact" <|> &"normalized" <|> &"lax"
+
+/--
+Whitespace handling for `#guard_msgs`:
+- `whitespace := exact` requires an exact whitespace match.
+- `whitespace := normalized` converts all newline characters to a space before matching
+  (the default). This allows breaking long lines.
+- `whitespace := lax` collapses whitespace to a single space before matching.
+In all cases, leading and trailing whitespace is trimmed before matching.
+-/
+syntax guardMsgsWhitespace := &"whitespace" " := " guardMsgsWhitespaceArg
+
+set_option linter.missingDocs false in
+syntax guardMsgsOrderingArg := &"exact" <|> &"sorted"
+
+/--
+Message ordering for `#guard_msgs`:
+- `ordering := exact` uses the exact ordering of the messages (the default).
+- `ordering := sorted` sorts the messages in lexicographic order.
+  This helps with testing commands that are non-deterministic in their ordering.
+-/
+syntax guardMsgsOrdering := &"ordering" " := " guardMsgsOrderingArg
+
+set_option linter.missingDocs false in
+syntax guardMsgsSpecElt := guardMsgsFilter <|> guardMsgsWhitespace <|> guardMsgsOrdering
+
+set_option linter.missingDocs false in
 syntax guardMsgsSpec := "(" guardMsgsSpecElt,* ")"
 
 /--
-`#guard_msgs` captures the messages generated by another command and checks that they
-match the contents of the docstring attached to the `#guard_msgs` command.
+`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd`
+and checks that they match the contents of the docstring.
 
 Basic example:
 ```lean
@@ -570,10 +607,10 @@ error: unknown identifier 'x'
 #guard_msgs in
 example : α := x
 ```
-This checks that there is such an error and then consumes the message entirely.
+This checks that there is such an error and then consumes the message.
 
-By default, the command intercepts all messages, but there is a way to specify which types
-of messages to consider. For example, we can select only warnings:
+By default, the command captures all messages, but the filter condition can be adjusted.
+For example, we can select only warnings:
 ```lean
 /--
 warning: declaration uses 'sorry'
@@ -586,29 +623,37 @@ or only errors
 #guard_msgs(error) in
 example : α := sorry
 ```
-In this last example, since the message is not intercepted there is a warning on `sorry`.
+In the previous example, since warnings are not captured there is a warning on `sorry`.
 We can drop the warning completely with
 ```lean
 #guard_msgs(error, drop warning) in
 example : α := sorry
 ```
 
-Syntax description:
+In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses:
 ```
-#guard_msgs (drop? info|warning|error|all,*)? in cmd
+#guard_msgs (configElt,*) in cmd
 ```
-
-If there is no specification, `#guard_msgs` intercepts all messages.
-Otherwise, if there is one, the specification is considered in left-to-right order, and the first
-that applies chooses the outcome of the message:
-- `info`, `warning`, `error`: intercept a message with the given severity level.
-- `all`: intercept any message (so `#guard_msgs in cmd` and `#guard_msgs (all) in cmd`
-  are equivalent).
-- `drop info`, `drop warning`, `drop error`: intercept a message with the given severity
-  level and then drop it. These messages are not checked.
-- `drop all`: intercept a message and drop it.
-
-For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and then drop
+By default, the configuration list is `(all, whitespace := normalized, ordering := exact)`.
+
+Message filters (processed in left-to-right order):
+- `info`, `warning`, `error`: capture messages with the given severity level.
+- `all`: capture all messages (the default).
+- `drop info`, `drop warning`, `drop error`: drop messages with the given severity level.
+- `drop all`: drop every message.
+
+Whitespace handling (after trimming leading and trailing whitespace):
+- `whitespace := exact` requires an exact whitespace match.
+- `whitespace := normalized` converts all newline characters to a space before matching
+  (the default). This allows breaking long lines.
+- `whitespace := lax` collapses whitespace to a single space before matching.
+
+Message ordering:
+- `ordering := exact` uses the exact ordering of the messages (the default).
+- `ordering := sorted` sorts the messages in lexicographic order.
+  This helps with testing commands that are non-deterministic in their ordering.
+
+For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and drop
 everything else.
 -/
 syntax (name := guardMsgsCmd)

src/Lean/Elab/GuardMsgs.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
 prelude
+import Lean.Elab.Notation
 import Lean.Server.CodeActions.Attr
 
 /-! `#guard_msgs` command for testing commands
@@ -40,31 +41,55 @@ inductive SpecResult
   /-- Do not capture the message. -/
   | passthrough
 
+/-- The method to use when normalizing whitespace, after trimming. -/
+inductive WhitespaceMode
+  /-- Exact equality. -/
+  | exact
+  /-- Equality after normalizing newlines into spaces. -/
+  | normalized
+  /-- Equality after collapsing whitespace into single spaces. -/
+  | lax
+
+/-- Method to use when combining multiple messages. -/
+inductive MessageOrdering
+  /-- Use the exact ordering of the produced messages. -/
+  | exact
+  /-- Sort the produced messages. -/
+  | sorted
+
 /-- Parses a `guardMsgsSpec`.
 - No specification: check everything.
 - With a specification: interpret the spec, and if nothing applies pass it through. -/
 def parseGuardMsgsSpec (spec? : Option (TSyntax ``guardMsgsSpec)) :
-    CommandElabM (Message → SpecResult) := do
-  if let some spec := spec? then
-    match spec with
-    | `(guardMsgsSpec| ($[$elts:guardMsgsSpecElt],*)) => do
-      let mut p : Message → SpecResult := fun _ => .passthrough
-      let pushP (s : MessageSeverity) (drop : Bool) (p : Message → SpecResult)
-          (msg : Message) : SpecResult :=
-        if msg.severity == s then if drop then .drop else .check
-        else p msg
-      for elt in elts.reverse do
-        match elt with
-        | `(guardMsgsSpecElt| $[drop%$drop?]? info)    => p := pushP .information drop?.isSome p
-        | `(guardMsgsSpecElt| $[drop%$drop?]? warning) => p := pushP .warning drop?.isSome p
-        | `(guardMsgsSpecElt| $[drop%$drop?]? error)   => p := pushP .error drop?.isSome p
-        | `(guardMsgsSpecElt| $[drop%$drop?]? all) =>
-          p := fun _ => if drop?.isSome then .drop else .check
-        | _ => throwErrorAt elt "Invalid #guard_msgs specification element"
-      return p
-    | _ => throwErrorAt spec "Invalid #guard_msgs specification"
-  else
-    return fun _ => .check
+    CommandElabM (WhitespaceMode × MessageOrdering × (Message → SpecResult)) := do
+  let elts ←
+    if let some spec := spec? then
+      match spec with
+      | `(guardMsgsSpec| ($[$elts:guardMsgsSpecElt],*)) => pure elts
+      | _ => throwUnsupportedSyntax
+    else
+      pure #[]
+  let mut whitespace : WhitespaceMode := .normalized
+  let mut ordering : MessageOrdering := .exact
+  let mut p? : Option (Message → SpecResult) := none
+  let pushP (s : MessageSeverity) (drop : Bool) (p? : Option (Message → SpecResult))
+      (msg : Message) : SpecResult :=
+    let p := p?.getD fun _ => .passthrough
+    if msg.severity == s then if drop then .drop else .check
+    else p msg
+  for elt in elts.reverse do
+    match elt with
+    | `(guardMsgsSpecElt| $[drop%$drop?]? info)     => p? := pushP .information drop?.isSome p?
+    | `(guardMsgsSpecElt| $[drop%$drop?]? warning)  => p? := pushP .warning drop?.isSome p?
+    | `(guardMsgsSpecElt| $[drop%$drop?]? error)    => p? := pushP .error drop?.isSome p?
+    | `(guardMsgsSpecElt| $[drop%$drop?]? all)      => p? := some fun _ => if drop?.isSome then .drop else .check
+    | `(guardMsgsSpecElt| whitespace := exact)      => whitespace := .exact
+    | `(guardMsgsSpecElt| whitespace := normalized) => whitespace := .normalized
+    | `(guardMsgsSpecElt| whitespace := lax)        => whitespace := .lax
+    | `(guardMsgsSpecElt| ordering := exact)        => ordering := .exact
+    | `(guardMsgsSpecElt| ordering := sorted)       => ordering := .sorted
+    | _ => throwUnsupportedSyntax
+  return (whitespace, ordering, p?.getD fun _ => .check)
 
 /-- An info tree node corresponding to a failed `#guard_msgs` invocation,
 used for code action support. -/
@@ -86,16 +111,27 @@ def removeTrailingWhitespaceMarker (s : String) : String :=
   s.replace "⏎\n" "\n"
 
 /--
-Strings are compared up to newlines, to allow users to break long lines.
+Applies a whitespace normalization mode.
+-/
+def WhitespaceMode.apply (mode : WhitespaceMode) (s : String) : String :=
+  match mode with
+  | .exact => s
+  | .normalized => s.replace "\n" " "
+  | .lax => String.intercalate " " <| (s.split Char.isWhitespace).filter (!·.isEmpty)
+
+/--
+Applies a message ordering mode.
 -/
-def equalUpToNewlines (exp res : String) : Bool :=
-  exp.replace "\n" " " == res.replace "\n" " "
+def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List String :=
+  match mode with
+  | .exact => msgs
+  | .sorted => msgs |>.toArray.qsort (· < ·) |>.toList
 
 @[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 ""
         |>.trim |> removeTrailingWhitespaceMarker
-    let specFn ← parseGuardMsgsSpec spec?
+    let (whitespace, ordering, specFn) ← parseGuardMsgsSpec spec?
     let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
     elabCommandTopLevel cmd
     let msgs := (← get).messages
@@ -106,8 +142,10 @@ def equalUpToNewlines (exp res : String) : Bool :=
       | .check       => toCheck := toCheck.add msg
       | .drop        => pure ()
       | .passthrough => toPassthrough := toPassthrough.add msg
-    let res := "---\n".intercalate (← toCheck.toList.mapM (messageToStringWithoutPos ·)) |>.trim
-    if equalUpToNewlines expected res then
+    let strings ← toCheck.toList.mapM (messageToStringWithoutPos ·)
+    let strings := ordering.apply strings
+    let res := "---\n".intercalate strings |>.trim
+    if whitespace.apply expected == whitespace.apply res then
       -- Passed. Only put toPassthrough messages back on the message log
       modify fun st => { st with messages := initMsgs ++ toPassthrough }
     else

stage0/src/stdlib_flags.h

@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);

tests/lean/run/guard_msgs.lean

@@ -95,3 +95,37 @@ bar
 -/
 #guard_msgs in
 run_meta Lean.logInfo "foo ⏎\nbar"
+
+/-!
+Lax whitespace
+-/
+
+/-- error: failed to synthesize DecidableEq (Nat → Nat) -/
+#guard_msgs (whitespace := lax) in
+#synth DecidableEq (Nat → Nat)
+
+/-- error: failed to synthesize
+
+DecidableEq (Nat → Nat) -/
+#guard_msgs (whitespace := lax) in
+#synth DecidableEq (Nat → Nat)
+
+/-!
+Sorting
+-/
+
+/--
+info: A
+---
+info: B
+-/
+#guard_msgs (ordering := sorted) in
+run_meta do Lean.logInfo "B"; Lean.logInfo "A"
+
+/--
+info: B
+---
+info: A
+-/
+#guard_msgs in
+run_meta do Lean.logInfo "B"; Lean.logInfo "A"