From e87b31eb3ac80a63535b34a13f853cb9e39ef189 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Thu, 31 Oct 2024 10:51:39 +0100 Subject: [PATCH] update readme and docs --- scripts/README.md | 4 ++++ scripts/add_deprecations.sh | 18 ++++++++++++++++++ 2 files changed, 22 insertions(+) diff --git a/scripts/README.md b/scripts/README.md index 33a295aa934b5..28b7eadfcf9bf 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -17,6 +17,10 @@ to learn about it as well! **Tool for manual maintenance** - `fix_unused.py` Bulk processing of unused variable warnings, replacing them with `_`. +- `add_deprecations.sh` is a text-based script that automatically adds deprecation stateements. + It assumes that the only difference between master and the current status of the PR consists + of renames. More precisely, any change on a line that contains a declaration name + and is not a rename, will likely confuse the script. **Analyzing Mathlib's import structure** - `unused_in_pole.sh` (followed by an optional ``, defaulting to `Mathlib`) diff --git a/scripts/add_deprecations.sh b/scripts/add_deprecations.sh index 49c218a789642..340f1d38c6ff7 100644 --- a/scripts/add_deprecations.sh +++ b/scripts/add_deprecations.sh @@ -1,5 +1,23 @@ #! /bin/bash +: <<'BASH_MODULE_DOCS' + +The script contained in this file tries to automatically generate deprecations for declarations that were renamed in a PR. + +The script is entirely text-based, so it makes several simplifying assumptions and may be easily confused. + +# Assumptions + +The script works under the assumption that the only modifications between master and the current branch are renames of lemmas that should be deprecated. + +The script inspects the relevant git diff, extracts the old name and the new one and uses this information to insert deprecated aliases as needed. + +Most other differences may confuse the script, although there is some slack. + +Please, do not try to push the boundaries of the script, since it is quite simple-minded! + +BASH_MODULE_DOCS + if [ -z "${1}" ] then commit="$( git merge-base master "$( git rev-parse --abbrev-ref HEAD )" )"