feat: the global syntax linter

[adomani]

The globalSyntax linter emits a warning on pairs of consecutive commands with no overall effect.
For instance, the linter would flag

namespace X
end X

and similarly for consecutive pairs of open or section and end.

---

• depends on: feat: global syntax linter #34019, with just the linter implementation
• depends on: [Merged by Bors] - chore: remove self-cancelling pairs #34021, with the linter-driven corrections

[adomani]

The default value should eventually be false. This linter should only run in CI and possibly on a schedule.

[Ruben-VandeVelde]

Is it expensive? I'd actually like this to be always on and in core

[adomani]

I have not benchmarked it, but I think that it is probably quite cheap.

The main issue is that it is incompatible with file edits. Linters can only reliably act on a single command at a time, so any linter that acts based on more than one command is exploiting a hack, like this one. The hack in this case is the IO.Ref that the linter uses.

[adomani]

My earlier comment stands: I don't think that syntax linters can reliably lint more than one command. However, I have in mind a different implementation of this linter that may be slightly more robust to file edits, but would inevitably require restarting a file to get reliable results.

[github-actions]

PR summary ca7d6f198f

Import changes exceeding 2%

%	File
+4.35%	Mathlib.Init

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Init	46	48	+2 (+4.35%)
Mathlib.Algebra.Ring.Units	176	178	+2 (+1.14%)
Mathlib.Data.ENNReal.Basic	669	671	+2 (+0.30%)
Mathlib.Data.Matrix.Basic	842	844	+2 (+0.24%)
Mathlib.Topology.Algebra.IsUniformGroup.Defs	982	984	+2 (+0.20%)
Mathlib.Analysis.Normed.Order.Basic	1035	1037	+2 (+0.19%)
Mathlib.Tactic	2901	2903	+2 (+0.07%)

Import changes for all files

Files	Import difference
There are 7440 files with changed transitive imports taking up over 319500 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ RangesToKinds
+ RangesToKinds.insert
+ cancellingPairs
+ globalSyntaxLinter
+ startersEnders
+ substringOfRange
+ toggle

You can run this locally as follows

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/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).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat: global syntax linter #34019
• [Merged by Bors] - chore: remove self-cancelling pairs #34021
  By Dependent Issues (🤖). Happy coding!

[grunweg]

#34047 deprecates this module

[adomani]

By the way, let me also point out that I would like to have tests for this linter, but the current implementation does not allow #guard_msgs.