[Merged by Bors] - feat: warn on deprecated declarations in scripts/check-yaml

[thorimur]

This PR updates scripts/check-yaml.lean to warn on deprecated declarations.

It also cleans up some code: initSearchPath does exactly what the removed code plus CoreM.withImportModules does (and as far as I can see we no longer need CoreM). Also modulizes and removes the dependence on Mathlib.

---

• depends on: [Merged by Bors] - chore: update deprecated declarations in *.yamls #38312

[github-actions]

PR summary 188cb08f82

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

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

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

---

No changes to technical debt.

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

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - chore: update deprecated declarations in *.yamls #38312
  By Dependent Issues (🤖). Happy coding!

[grunweg]

Thanks, this is great to have and much cleaner! I'm not an expert on the initSearchPath change (and would appreciate a second pair of eyes on it); the rest is straightforward and much nicer.
maintainer merge?

[github-actions]

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

[adomani]

Thanks, this looks great!

Would it be possible to add a test for this code? Maybe by extending the databases list to contain a test that exercises the various deprecated/missing possibilities?

Scripts that are not in Mathlib have a tendency of breaking and go unnoticed...

[adomani]

Whether or not adding a test is feasible, I'll leave the choice to you!

bors d+

[mathlib-bors]

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

[thorimur]

Would it be possible to add a test for this code? Maybe by extending the databases list to contain a test that exercises the various deprecated/missing possibilities?

Scripts that are not in Mathlib have a tendency of breaking and go unnoticed...

I'd love to add a test, but it is more than a little awkward...we'd have to adjust the python script to output a new json file, I think (or permanently include a json somewhere?).

It's taking me a little bit to figure out what the right way to test this is, so maybe let's merge this so that no more deprecations creep in in the meantime, then PR the test separately if we can figure it out!

[thorimur]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step

[grunweg]

Here's an idea about testing: you could

• add a test-only .json file, referencing a deprecated item
• check the exact output, and
• that's it.

I even tend towards "use an actual deprecated item", and adding a detailed comment in the test what it's testing. Every six months, the test will have to be updated to use a new deprecated item. This is not great, but I'd say it's good enough.

Actually, thinking about it more: you could have a test file defining a test-only deprecated item, and use that for the test...