rename: `no_lost_declarations` to `decls_diff` and `short` as default option

[adomani]

This PR renames the no_lost_declarations script to decls_diff, to better describe the effect of the script. It was originally intended as a script to make sure that "moving" PRs did not leave out any declaration, but is now used as a measure of the diff in declarations between PRs and master.

The other change it does is to make the short option the default, as this is the most commonly used.

Old	New
./scripts/no_lost_declarations.sh short	./scripts/decls_diff.sh
./scripts/no_lost_declarations.sh	./scripts/decls_diff.sh long

Mostly, these changes are invisible, as this script is used almost exclusively by CI, but the intention is that the change conveys better what script does to a human.

---

[github-actions[bot]]

PR summary 01cceba7e3

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/declarations_diff.sh <optional_commit>

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

[grunweg]

Looks reasonable! What do you think about renaming to declarations_diff? (I find the latter more readable; if mostly CI runs this, one might as well use a readable name.) Feel free to maintainer merge on my behalf when you considered this.

[adomani]

Michael, thank you for the suggestion: I like it and I renamed the script to declarations_diff.

[grunweg]

Thanks! maintainer merge

[github-actions[bot]]

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

[mattrobball]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style