PR summary b3cf7a02d3

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

./scripts/technical-debt-metrics.sh pr_summary

Quick question @kim-em : I realized the private annotations were holdovers, since I'm not in a public section. In be160c5 I removed these, and made only the option declaration itself public, but I'm cargo culting there. Is this sensible?

EDIT: discussed it a bit with @grunweg; we agree it's sensible to have the option declaration itself as public API accessible to other metaprograms; still curious what you think.

I know from the discussion on Zulip that you did some extensive benchmarking, so maybe my suggestion is not really needed. However, I expect that most lemmas in mathlib should not even be eligible for this linter, since there is neither an active variable [DecidableWhatever ...] in scope, nor is there an explicit [DecidableWhatever ...] in the type signature.

This check simply requires accessing the currently available variables in the scope and traversing (part of) the syntax of the command. These look like substantially cheaper checks than traversing the infotrees and for most of the commands, these would be the only needed checks.

Would it make sense to implement them? Or are there already early exits in the linter that take something like this into account?

I know from the discussion on Zulip that you did some extensive benchmarking, so maybe my suggestion is not really needed. However, I expect that most lemmas in mathlib should not even be eligible for this linter, since there is neither an active variable [DecidableWhatever ...] in scope, nor is there an explicit [DecidableWhatever ...] in the type signature.

This check simply requires accessing the currently available variables in the scope and traversing (part of) the syntax of the command. These look like substantially cheaper checks than traversing the infotrees and for most of the commands, these would be the only needed checks.

Would it make sense to implement them? Or are there already early exits in the linter that take something like this into account?

No no, this is certainly very welcome! :) I haven't yet focused on performance optimizations in the infotree (or earlier!) part of the linter, but I certainly plan to in subsequent PRs, especially since this linter architecture will also handle Fintype, Encodable, etc. instances.

I think that an early exit of the kind you mention is a good idea! I'm trying to think of cases where it would early-exit when it shouldn't, but can't. I'd like to test this thoroughly to be sure there are no false negatives, so I will try it in that subsequent performance-oriented PR. :)

(Note: there are also some minor performance improvements we could make to the infotree search itself; collectNodesBottomUp does a bit too much work for our purposes, so I'll try that too.)

Okay, I think all comments are resolved (or promised to be resolved in future versions! 😁), and I think making the option declaration public is such a minor change that it's easy to fix later if it's wrong. So, I'm going to pull the trigger on this in an hour or so, barring any further comments. :)

bors r+

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build
• Post-Build Step