From ca12e7fd0e36c51436bcdf5131503c9dd0083e9b Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 12 Apr 2024 04:59:20 +0200 Subject: [PATCH] feat: add `#guard_msgs` configuration syntax and update documentation Implementation for this configuration syntax will appear after a stage0 update. --- src/Init/Notation.lean | 91 +++++++++++++++++++++++++++++++----------- 1 file changed, 68 insertions(+), 23 deletions(-) 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)