Commit 2026-09-01 18:09 a30e7576

perf(Tactic/Linter/Header): different implementation for header linter (#40347) This PR tries a different implementation strategy for the header linter: identify whether we're linting the first command by parsing the file header quickly, seeing where the final position for the parse lands, and seeing if the current command's start position (stored in the CommandElabM context) matches that position. Then, check if the first command is a module doc (or an exempted command) just by looking at the current syntax's kind. While this does still parse the imports on every command, it does less parsing than the previous implementation. This reduces interpretation wall-clock by over 10% (at least on the radar machines). This also changes the behavior slightly:

• adds backticks in messages instead of quotes
• now allows set_option ... in before the module docstring There's still room for improvement: in the future we could try to figure out an interactive-safe cache for the end position of the header (somewhat tricky) and update the string functions to use the new string slice API. (The first part might be easier after some upcoming linting framework changes.) My guess for why this seems to improve the performance in apparently unrelated metrics is that it reduces pressure on the async computations overall, but to be honest, I'm not sure.