diff --git a/RELEASES.md b/RELEASES.md index 032e64665d29..a14bd3500f2d 100644 --- a/RELEASES.md +++ b/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_` instead of `._eq_`, and `.def` instead of `._unfold`. Example: diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 0c6923436984..353cdc8459af 100644 --- a/src/Init/Notation.lean +++ b/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) diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean index ecdca448c4ce..ddb84a292185 100644 --- a/src/Lean/Elab/GuardMsgs.lean +++ b/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 diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 0699845ba452..658ab0874e68 100644 --- a/stage0/src/stdlib_flags.h +++ b/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); diff --git a/tests/lean/run/guard_msgs.lean b/tests/lean/run/guard_msgs.lean index 2e4faa99dc59..dbae9fd3114c 100644 --- a/tests/lean/run/guard_msgs.lean +++ b/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"