feat: add `endOf` linter

[adomani]

This linter emits a warning at the end of a file if there are unclosed namespaces or sections.

Unlike #14352, this PR does leaves outermost noncomputable sections open.

Zulip thread

---

Self-correcting script:

eval "$(
  lake build |
    grep -v "^\(✔ \[\|note: \|⚠ \[\|trace: \|Build completed\)" |
      sed -z "s=warning: \./\./\./\./\([^:]*\):[^']*'\([^']*\)'\n=\nprintf '\2\\n' >> \1\n\n\n=g" |
      sed -z "s=\n\n*=\n=g; s=\([^']\)\nend=\1\n\nend=g"
)"

[github-actions[bot]]

PR summary b600a781ce

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ endOfLinter + getLinterHash

You can run this locally as follows

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

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

[grunweg]

#14620 contains a few of these fixes. As discussed with adomani, let's land these fixes as a follow-up, and land the linter now.

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[kim-em]

What sort of linter is this? (syntax? environment? script?) I can't even find it amongst all the modified files. :-(

I think we need to split out the actual section closing updates from the PR that adds the linter.

[grunweg]

It's a syntax linter; it can be found in Mathlib/Tactic/Linter/Lint.lean.

[grunweg]

Created #14621 with just the newly added sections/namespaces.

[grunweg]

The fixes to the other files have landed; I have merged master. This PR now just contains the linter. I still think the implementation is good. maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[mathlib-bors[bot]]

Build failed (retrying...):

• Build

[mathlib-bors[bot]]

Build failed (retrying...):

• Build

[mattrobball]

bors r-

[mathlib-bors[bot]]

Canceled.

[mattrobball]

Wronskian violates the linter and just got in

[mattrobball]

bors delegate+

Please merge again when fixed

[mathlib-bors[bot]]

:v: adomani can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[adomani]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style