[Merged by Bors] - fix: support more parsers in #help#12287
[Merged by Bors] - fix: support more parsers in #help#12287
#help#12287Conversation
|
AIUI, this is blocked on the author fixing the build failures - let me label it as such. |
| \n\ | ||
| \nTry this:\ | ||
| \nset_option trace.Meta.synthInstance true\ | ||
| \n#synth SlimCheck.Testable ({tgt'})" |
There was a problem hiding this comment.
The reason this is here is because fixing #help caused the set of hash commands used by lint_hash_commands to include #synth, which now causes a false positive on this line. I fixed it by indenting the string literal so it doesn't look like an actual #synth call.
There was a problem hiding this comment.
I think #13142 should fix this: the new Lean version of this linter ought to see this is a string literal.
There was a problem hiding this comment.
I just ran an experiment: #13230 shows that building mathlib succeeds (in particular, the syntax linter does not flag #synth), but the text-based one works.
I think that the #-command CI checks should be removed.
There was a problem hiding this comment.
I don't understand what you are trying to say. Prior to this commit, #help would not flag #synth as a hash command, which causes the text-based CI to produce false negatives for all #synth commands. After it, #synth is treated as a hash command, producing a false positive right here in a string literal. I think the string literal is better anyway with proper indentation. The new syntax linter does not use #help to begin with and just fires on all atoms starting with # (which has its own set of false negatives since it doesn't recurse into subexpressions correctly, basically reproducing the error fixed in this PR in a new implementation, in addition to the FN because it doesn't consider nested commands like set_option ... in #synth).
There was a problem hiding this comment.
What I was trying to say is that it is only the string-based, #help-dependent linter that flags this, not the more recent syntax linter. Hence, removing the older string-based linter would make this change on Slimcheck not needed. Of course, the change could still be desirable!
|
bors merge |
As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/missing.20doc.20of.20.60.23check_failure.60/near/434466058), the `#help` command is out of date with respect to the parsers that can be obscuring the search for the "first token", used to power the search-by-token-prefix form of the command `#help tactic "measur"`. The list below has been tested against everything in lean, and the only things that fail to find a first token now are those that actually don't have a token like the ident parser. Co-authored-by: Mario Carneiro <di.gama@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
#help#help
As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/missing.20doc.20of.20.60.23check_failure.60/near/434466058), the `#help` command is out of date with respect to the parsers that can be obscuring the search for the "first token", used to power the search-by-token-prefix form of the command `#help tactic "measur"`. The list below has been tested against everything in lean, and the only things that fail to find a first token now are those that actually don't have a token like the ident parser. Co-authored-by: Mario Carneiro <di.gama@gmail.com>
As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/missing.20doc.20of.20.60.23check_failure.60/near/434466058), the `#help` command is out of date with respect to the parsers that can be obscuring the search for the "first token", used to power the search-by-token-prefix form of the command `#help tactic "measur"`. The list below has been tested against everything in lean, and the only things that fail to find a first token now are those that actually don't have a token like the ident parser. Co-authored-by: Mario Carneiro <di.gama@gmail.com>
As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/missing.20doc.20of.20.60.23check_failure.60/near/434466058), the `#help` command is out of date with respect to the parsers that can be obscuring the search for the "first token", used to power the search-by-token-prefix form of the command `#help tactic "measur"`. The list below has been tested against everything in lean, and the only things that fail to find a first token now are those that actually don't have a token like the ident parser. Co-authored-by: Mario Carneiro <di.gama@gmail.com>
As reported on Zulip, the
#helpcommand is out of date with respect to the parsers that can be obscuring the search for the "first token", used to power the search-by-token-prefix form of the command#help tactic "measur". The list below has been tested against everything in lean, and the only things that fail to find a first token now are those that actually don't have a token like the ident parser.