PR summary 775d95dac5

Import changes for modified files

No significant changes to the import graph

Declarations diff

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

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

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

Good idea! (Out of curiosity: were there any bugs in the past caught by this? Or is this just a precaution?)

As a follow-up, would you like to ensure this stays in sync with the lakefile, somehow - or is that an unimportant concern? Feel free to maintainer merge on my behalf once you thought about this.

Yes, it would be nice to stay in sync, but I coudn't think of an easy way to do this --- we don't want to simply scrape the manifest, because some dependencies (e.g. Cli and ImportGraph) are not used in Mathlib proper so may not have been built by the time the test runs.

I think that dependencies change slowly enough, and the test is not critical, that we can hope for the best here, at least for now.

Sounds reasonable - so let me
maintainer merge

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

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style