fix(Linter/UnusedTactic): don't use IO.Ref for extensibility

[JovanGerb]

This PR cleans up the unused tactic linter extensibility implementation. Previously, this was implemented using a PersistentEnvExtension and an IO.Ref. The problem with the IO.Ref is that it creates "spooky action at a distance": a command later in the file can affect what happens earlier in the file. Instead, we can allow both local and global modifications using a SimpleScopedEnvExtension.

Previously, the list of exceptions was unnaturally split into the two files. This PR makes it into just a single list.

Additionally:

• #allow_unused_tactic is deprecated in favour of allow_unused_tactic
• We put a namespace around the change? syntax, so that change? is not anymore a declared constant.

---

[github-actions]

PR summary a732f541f8

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Linter.UnusedTacticExtension	1	0	-1 (-100.00%)
Mathlib.Tactic.Linter.UnusedTactic	4	2	-2 (-50.00%)
Mathlib.Init	58	56	-2 (-3.45%)
Mathlib.Tactic.Change	59	57	-2 (-3.39%)
Mathlib.Tactic	2856	2854	-2 (-0.07%)

Import changes for all files

Files	Import difference
../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all
There are 8251 files with changed transitive imports taking up over 359941 characters: this is too many to display!
You can run this locally from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

---

Declarations diff (regex)

+ initialAllowedUnusedTactics

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit a732f541f8
Reference commit ac10dc7e9a

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

---

note: file Mathlib/Tactic/Linter/UnusedTacticExtension.lean was removed.
Please create a follow-up pull request adding a module deprecation. Thanks!

[JovanGerb]

@adomani, is there actually a use case for only locally adding a tactic as an allowed tactic? I would think that if a tactic is allowed to be unused, then this should also be so in imported files. In that case, we wouldn't need separate allow_unused_tactic and allow_unused_tactic! commands.

[adomani]

I do not have a strong reason, but, when I teach, I sometimes like to make the distinction that in some places done is not flagged, but when I am polishing the code, I would like it to be flagged.

I would say that for mathlib itself, there is no need for the distinction, but there are many consumers downstream of mathlib that it is probably a good idea to allow local and global silencing to be separate.