From ee8a6aa3afbe1e01070ee0fc39081baf66d6e279 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 8 Jul 2024 22:45:18 +0200 Subject: [PATCH 01/18] wip: require all scripts to be documented --- scripts/lint_style.lean | 31 ++++++++++++++++++++++++++++--- 1 file changed, 28 insertions(+), 3 deletions(-) diff --git a/scripts/lint_style.lean b/scripts/lint_style.lean index 42c5e3b4e1cc9..6aee75d906d94 100644 --- a/scripts/lint_style.lean +++ b/scripts/lint_style.lean @@ -16,19 +16,44 @@ The linters themselves are defined in `Mathlib.Tactic.Linter.TextBased`. open Cli +open System.FilePath + +/-- Verifies that every file in the `scripts` directory is documented in `scripts/README.md`. -/ +def checkScriptsDocumented : IO Bool := do + -- Retrieve all scripts (except for the `bench` directory). + let allScripts ← (walkDir "scripts" fun p ↦ pure (p.components.getD 1 "" != "bench")) + let allScripts := (allScripts.erase "bench").erase "README.md" + -- TODO: drop some false positives + -- nolint.json and noshake.json are data files; as are style-exceptions.txt and nolints-style.txt + -- these *could* be explicitly allows, or documented as well (perhaps the latter?) + -- Check if the README text contains each file enclosed in backticks. + let readme : String ← IO.FS.readFile (System.mkFilePath ["scripts", "README.md"]) + IO.println s!"found {allScripts.size} scripts: {",".intercalate (allScripts.map (·.toString)).toList}" + -- These are data files for linter exceptions: don't complain about these *for now*. + let dataFiles := #["nolints.json", "noshake.json", "style-exceptions.txt", "nolints-style.txt"] + let undocumented := allScripts.filter fun script ↦ + !readme.containsSubstr s!"`{script}`" && !dataFiles.contains script.toString + if undocumented.size > 0 then + IO.println s!"error: found {undocumented.size} undocumented scripts:\ + please describe the scripts\n\ + {String.intercalate "," (undocumented.map (·.fileName.get!)).toList}\n\ + in 'scripts/README.md'" + return undocumented.size > 0 + /-- Implementation of the `lint_style` command line program. -/ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do let errorStyle := match (args.hasFlag "github", args.hasFlag "update") with | (true, _) => ErrorFormat.github | (false, true) => ErrorFormat.exceptionsFile | (false, false) => ErrorFormat.humanReadable - let mut numberErrorFiles : UInt32 := 0 + let mut numberErrors : UInt32 := 0 for s in ["Archive.lean", "Counterexamples.lean", "Mathlib.lean"] do let n ← lintAllFiles (System.mkFilePath [s]) errorStyle - numberErrorFiles := numberErrorFiles + n + numberErrors := numberErrors + n + if ← checkScriptsDocumented then numberErrors := numberErrors + 1 -- Make sure to return an exit code of at most 125, so this return value can be used further -- in shell scripts. - return min numberErrorFiles 125 + return min numberErrors 125 /-- Setting up command line options and help text for `lake exe lint_style`. -/ -- so far, no help options or so: perhaps that is fine? From 7abe395747120383b3f6de8d5c569f1bb8740a28 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 25 Oct 2024 11:33:03 +1100 Subject: [PATCH 02/18] rename to match master --- scripts/{lint_style.lean => lint-style.lean} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename scripts/{lint_style.lean => lint-style.lean} (100%) diff --git a/scripts/lint_style.lean b/scripts/lint-style.lean similarity index 100% rename from scripts/lint_style.lean rename to scripts/lint-style.lean From cdaa88a2c7b1bad1fa9788b127133f17d09deb46 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 27 Oct 2024 14:37:13 +0100 Subject: [PATCH 03/18] Actually run the check: now it fails, of course. --- scripts/lint-style.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index 09355fc3cfd0a..6e9bd097ebde0 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -12,6 +12,8 @@ import Cli.Basic This files defines the `lint-style` executable which runs all text-based style linters. The linters themselves are defined in `Mathlib.Tactic.Linter.TextBased`. + +In addition, this checks that every file in `scripts` is documented in its top-level README. -/ open Cli Mathlib.Linter.TextBased @@ -50,15 +52,16 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do let mut allModules := #[] for s in ["Archive.lean", "Counterexamples.lean", "Mathlib.lean"] do allModules := allModules.append ((← IO.FS.lines s).map (·.stripPrefix "import ")) - -- note: since we manually add "Batteries" to "Mathlib.lean", we remove it here manually + -- Note: since we manually add "Batteries" to "Mathlib.lean", we remove it here manually. allModules := allModules.erase "Batteries" - let numberError ← lintModules allModules style fix + let mut numberErrors := ← lintModules allModules style fix + if !(← checkScriptsDocumented) then numberErrors := numberErrors + 1 -- If run with the `--fix` argument, return a zero exit code. -- Otherwise, make sure to return an exit code of at most 125, -- so this return value can be used further in shell scripts. if args.hasFlag "fix" then return 0 - else return min numberError 125 + else return min numberErrors 125 /-- Setting up command line options and help text for `lake exe lint-style`. -/ -- so far, no help options or so: perhaps that is fine? From 842f09d5037923965577c07278e8edb1569c9a9f Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 27 Oct 2024 14:40:32 +0100 Subject: [PATCH 04/18] chore: add stub README --- scripts/README.md | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 scripts/README.md diff --git a/scripts/README.md b/scripts/README.md new file mode 100644 index 0000000000000..16881cce0d5e8 --- /dev/null +++ b/scripts/README.md @@ -0,0 +1,8 @@ +## Miscellaneous scripts for working on mathlib + +This directory contains miscellaneous scripts that are useful for working on or with mathlib. +When adding a new script, please make sure to document it here, so other readers have a chance +to learn about it as well! + +**Current scripts and their purpose.** +- From 5c6b5d6a2653737fde93585e203b170911d4c8e5 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 27 Oct 2024 14:42:21 +0100 Subject: [PATCH 05/18] Tweak further --- scripts/lint-style.lean | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index 6e9bd097ebde0..47bf3de16d0fa 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -25,9 +25,6 @@ def checkScriptsDocumented : IO Bool := do -- Retrieve all scripts (except for the `bench` directory). let allScripts ← (walkDir "scripts" fun p ↦ pure (p.components.getD 1 "" != "bench")) let allScripts := (allScripts.erase "bench").erase "README.md" - -- TODO: drop some false positives - -- nolint.json and noshake.json are data files; as are style-exceptions.txt and nolints-style.txt - -- these *could* be explicitly allows, or documented as well (perhaps the latter?) -- Check if the README text contains each file enclosed in backticks. let readme : String ← IO.FS.readFile (System.mkFilePath ["scripts", "README.md"]) IO.println s!"found {allScripts.size} scripts: {",".intercalate (allScripts.map (·.toString)).toList}" @@ -36,10 +33,9 @@ def checkScriptsDocumented : IO Bool := do let undocumented := allScripts.filter fun script ↦ !readme.containsSubstr s!"`{script}`" && !dataFiles.contains script.toString if undocumented.size > 0 then - IO.println s!"error: found {undocumented.size} undocumented scripts:\ - please describe the scripts\n\ - {String.intercalate "," (undocumented.map (·.fileName.get!)).toList}\n\ - in 'scripts/README.md'" + IO.println s!"error: found {undocumented.size} undocumented scripts: \ + please describe the scripts in 'scripts/README.md'\n\ + {String.intercalate "," (undocumented.map (·.fileName.get!)).toList}" return undocumented.size > 0 /-- Implementation of the `lint-style` command line program. -/ From bc5647a359ca215d5303de643c09bc95a5ce343a Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 27 Oct 2024 14:44:04 +0100 Subject: [PATCH 06/18] Small fixes --- scripts/lint-style.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index 47bf3de16d0fa..dcaf92ee2e8b8 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -24,7 +24,7 @@ open System.FilePath def checkScriptsDocumented : IO Bool := do -- Retrieve all scripts (except for the `bench` directory). let allScripts ← (walkDir "scripts" fun p ↦ pure (p.components.getD 1 "" != "bench")) - let allScripts := (allScripts.erase "bench").erase "README.md" + let allScripts := (allScripts.erase "scripts/bench").erase "scripts/README.md" -- Check if the README text contains each file enclosed in backticks. let readme : String ← IO.FS.readFile (System.mkFilePath ["scripts", "README.md"]) IO.println s!"found {allScripts.size} scripts: {",".intercalate (allScripts.map (·.toString)).toList}" From 27b54ecddc7fa7ac5a8f72bf90bd26dad7833f4f Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 27 Oct 2024 14:44:09 +0100 Subject: [PATCH 07/18] TEMP --- scripts/lint-style.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index dcaf92ee2e8b8..a699a82908269 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -50,7 +50,7 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do allModules := allModules.append ((← IO.FS.lines s).map (·.stripPrefix "import ")) -- Note: since we manually add "Batteries" to "Mathlib.lean", we remove it here manually. allModules := allModules.erase "Batteries" - let mut numberErrors := ← lintModules allModules style fix + let mut numberErrors := 0 --← lintModules allModules style fix if !(← checkScriptsDocumented) then numberErrors := numberErrors + 1 -- If run with the `--fix` argument, return a zero exit code. -- Otherwise, make sure to return an exit code of at most 125, From 5b56b6f6167262957d91ed0f0201672c74474f87 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 27 Oct 2024 14:50:25 +0100 Subject: [PATCH 08/18] Fix filtering logic: operate on filenames only --- scripts/lint-style.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index a699a82908269..2712f8f860e31 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -24,18 +24,20 @@ open System.FilePath def checkScriptsDocumented : IO Bool := do -- Retrieve all scripts (except for the `bench` directory). let allScripts ← (walkDir "scripts" fun p ↦ pure (p.components.getD 1 "" != "bench")) - let allScripts := (allScripts.erase "scripts/bench").erase "scripts/README.md" + let allScripts := allScripts.erase ("scripts" / "bench")|>.erase ("scripts" / "README.md") -- Check if the README text contains each file enclosed in backticks. - let readme : String ← IO.FS.readFile (System.mkFilePath ["scripts", "README.md"]) + let readme : String ← IO.FS.readFile ("scripts" / "README.md") IO.println s!"found {allScripts.size} scripts: {",".intercalate (allScripts.map (·.toString)).toList}" -- These are data files for linter exceptions: don't complain about these *for now*. let dataFiles := #["nolints.json", "noshake.json", "style-exceptions.txt", "nolints-style.txt"] - let undocumented := allScripts.filter fun script ↦ - !readme.containsSubstr s!"`{script}`" && !dataFiles.contains script.toString + -- For now, there are no scripts in sub-directories that should be documented. + let fileNames := allScripts.map (·.fileName.get!) + let undocumented := fileNames.filter fun script ↦ + !readme.containsSubstr s!"`{script}`" && !dataFiles.contains script if undocumented.size > 0 then IO.println s!"error: found {undocumented.size} undocumented scripts: \ please describe the scripts in 'scripts/README.md'\n\ - {String.intercalate "," (undocumented.map (·.fileName.get!)).toList}" + {String.intercalate "," undocumented.toList}" return undocumented.size > 0 /-- Implementation of the `lint-style` command line program. -/ From 23b6c9824b89c8163258093e26d0442e0521c0b4 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 27 Oct 2024 15:00:20 +0100 Subject: [PATCH 09/18] Add stub entries for the scripts, at least classify them. Documenting them can come later. --- scripts/README.md | 33 ++++++++++++++++++++++++++++++++- scripts/lint-style.lean | 2 +- 2 files changed, 33 insertions(+), 2 deletions(-) diff --git a/scripts/README.md b/scripts/README.md index 16881cce0d5e8..495ffe3743adb 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -5,4 +5,35 @@ When adding a new script, please make sure to document it here, so other readers to learn about it as well! **Current scripts and their purpose.** -- +TODO: add real content for all these entries! + +Part of mathlib +- `polyrith_sage.py`, `polyrith_sage_helper.py` + +Part of CI workflow +- `mk_all.lean` +- `lint-style.py` and `lint-style.lean`, `print-style-errors.sh` +- `lint-bib.sh` +- `yaml_check.py`, `check-yaml.lean` + +Managing and tracking technical debt +- `update_nolints_CI.sh` (maintenance, runs once a week) +- `technical-debt-metrics.sh` +- `init_creation.sh` (supposed to be run manually; might be removed soon?) + +- `create-adaptation-pr.sh`, `lean-pr-testing-comments.sh` + +- `bench_summary.lean`, `autolabel.lean`, `get_tlabel.sh` + +- `install_debian.sh`, `install_macos.sh` + +- `declarations_diff.sh`, `count-trans-deps.py`, `import_trans_difference.sh`, `update_PR_comment.sh`; +`import-graph-report.py` + + +Data files with exclusions for style linters: all of these should tend to zero over time +- `nolints.json`: TODO document! +- `no_lints_prime_decls.txt`: TODO document this + +Other +- `fix_unused.py` diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index 2712f8f860e31..f7b1d1c762785 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -29,7 +29,7 @@ def checkScriptsDocumented : IO Bool := do let readme : String ← IO.FS.readFile ("scripts" / "README.md") IO.println s!"found {allScripts.size} scripts: {",".intercalate (allScripts.map (·.toString)).toList}" -- These are data files for linter exceptions: don't complain about these *for now*. - let dataFiles := #["nolints.json", "noshake.json", "style-exceptions.txt", "nolints-style.txt"] + let dataFiles := #["noshake.json", "nolints-style.txt"] -- For now, there are no scripts in sub-directories that should be documented. let fileNames := allScripts.map (·.fileName.get!) let undocumented := fileNames.filter fun script ↦ From 1925b25f6e5b58bb41dd3e8682a468d4827bee10 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 27 Oct 2024 15:01:32 +0100 Subject: [PATCH 10/18] Untemp --- scripts/lint-style.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index f7b1d1c762785..e0fc31de683a6 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -27,7 +27,6 @@ def checkScriptsDocumented : IO Bool := do let allScripts := allScripts.erase ("scripts" / "bench")|>.erase ("scripts" / "README.md") -- Check if the README text contains each file enclosed in backticks. let readme : String ← IO.FS.readFile ("scripts" / "README.md") - IO.println s!"found {allScripts.size} scripts: {",".intercalate (allScripts.map (·.toString)).toList}" -- These are data files for linter exceptions: don't complain about these *for now*. let dataFiles := #["noshake.json", "nolints-style.txt"] -- For now, there are no scripts in sub-directories that should be documented. @@ -52,7 +51,7 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do allModules := allModules.append ((← IO.FS.lines s).map (·.stripPrefix "import ")) -- Note: since we manually add "Batteries" to "Mathlib.lean", we remove it here manually. allModules := allModules.erase "Batteries" - let mut numberErrors := 0 --← lintModules allModules style fix + let mut numberErrors := ← lintModules allModules style fix if !(← checkScriptsDocumented) then numberErrors := numberErrors + 1 -- If run with the `--fix` argument, return a zero exit code. -- Otherwise, make sure to return an exit code of at most 125, From f2643c0de3178391836a119f69b5101704c5627b Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 27 Oct 2024 15:05:47 +0100 Subject: [PATCH 11/18] Fix and clarify the return value. --- scripts/lint-style.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index e0fc31de683a6..57c5a1b1cb122 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -20,8 +20,9 @@ open Cli Mathlib.Linter.TextBased open System.FilePath -/-- Verifies that every file in the `scripts` directory is documented in `scripts/README.md`. -/ -def checkScriptsDocumented : IO Bool := do +/-- Verifies that every file in the `scripts` directory is documented in `scripts/README.md`. +Return `True` if there are undocumented scripts, otherwise `False`. -/ +def allScriptsDocumented : IO Bool := do -- Retrieve all scripts (except for the `bench` directory). let allScripts ← (walkDir "scripts" fun p ↦ pure (p.components.getD 1 "" != "bench")) let allScripts := allScripts.erase ("scripts" / "bench")|>.erase ("scripts" / "README.md") @@ -37,7 +38,7 @@ def checkScriptsDocumented : IO Bool := do IO.println s!"error: found {undocumented.size} undocumented scripts: \ please describe the scripts in 'scripts/README.md'\n\ {String.intercalate "," undocumented.toList}" - return undocumented.size > 0 + return undocumented.size == 0 /-- Implementation of the `lint-style` command line program. -/ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do @@ -52,7 +53,7 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do -- Note: since we manually add "Batteries" to "Mathlib.lean", we remove it here manually. allModules := allModules.erase "Batteries" let mut numberErrors := ← lintModules allModules style fix - if !(← checkScriptsDocumented) then numberErrors := numberErrors + 1 + if !(← allScriptsDocumented) then numberErrors := numberErrors + 1 -- If run with the `--fix` argument, return a zero exit code. -- Otherwise, make sure to return an exit code of at most 125, -- so this return value can be used further in shell scripts. From 750a05982d822e29d6d1f1c4aa60a7cf27513836 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 30 Oct 2024 13:11:31 +1100 Subject: [PATCH 12/18] work on the README --- scripts/README.md | 60 +++++++++++++++++++++++++++++++++---------- scripts/fix_unused.py | 3 +++ 2 files changed, 49 insertions(+), 14 deletions(-) diff --git a/scripts/README.md b/scripts/README.md index 495ffe3743adb..60ab59f09ac35 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -7,33 +7,65 @@ to learn about it as well! **Current scripts and their purpose.** TODO: add real content for all these entries! -Part of mathlib -- `polyrith_sage.py`, `polyrith_sage_helper.py` +Installation scripts +- `install_debian.sh`, `install_macos.sh` + Install scripts referenced from the leanprover community install pages. + https://leanprover-community.github.io/install/debian.html + https://leanprover-community.github.io/install/macos.html + If these web pages are deprecated or removed, we should remove these scripts. -Part of CI workflow +CI workflow - `mk_all.lean` + run via `lake exe mk_all`, regenerates `Mathlib.lean` - `lint-style.py` and `lint-style.lean`, `print-style-errors.sh` + style linters, written in Python and Lean. - `lint-bib.sh` + normalize the BibTeX file `docs/references.bib` using `bibtool`. - `yaml_check.py`, `check-yaml.lean` - -Managing and tracking technical debt + Sanity checks for `undergrad.yaml`, `overview.yaml`, and `100.yaml`. +- `lean-pr-testing-comments.sh` + Generate comments and labels on a Lean or Batteries PR after CI has finished on a + `*-pr-testing-NNNN` branch. - `update_nolints_CI.sh` (maintenance, runs once a week) -- `technical-debt-metrics.sh` -- `init_creation.sh` (supposed to be run manually; might be removed soon?) +- `bench_summary.lean` + Convert data retrieved from the speed-center into a shorter, more accessible format, + and post a comment with this summary on github. +- `declarations_diff.sh` + Attempts to find which declarations have been removed and which have been added in the current PR + with respect to `master`, and posts a comment on github with the result. -- `create-adaptation-pr.sh`, `lean-pr-testing-comments.sh` +Managing nightly-testing and bump branches +- `create-adaptation-pr.sh` implements some of the steps in the workflow described at + https://leanprover-community.github.io/contribute/tags_and_branches.html#mathlib-nightly-and-bump-branches + Specifically, it will: + - merge `master` into `bump/v4.x.y` + - create a new branch from `bump/v4.x.y`, called `bump/nightly-YYYY-MM-DD` + - merge `nightly-testing` into the new branch + - open a PR to merge the new branch back into `bump/v4.x.y` + - announce the PR on zulip + - finally, merge the new branch back into `nightly-testing`, if conflict resolution was required. -- `bench_summary.lean`, `autolabel.lean`, `get_tlabel.sh` + If there are merge conflicts, it pauses and asks for help from the human driver. -- `install_debian.sh`, `install_macos.sh` - -- `declarations_diff.sh`, `count-trans-deps.py`, `import_trans_difference.sh`, `update_PR_comment.sh`; -`import-graph-report.py` +Managing and tracking technical debt +- `technical-debt-metrics.sh` +- `init_creation.sh` (supposed to be run manually; might be removed soon?) +Mathlib tactics +- `polyrith_sage.py`, `polyrith_sage_helper.py` are required for `polyrith` + to communication with the Sage server. Data files with exclusions for style linters: all of these should tend to zero over time - `nolints.json`: TODO document! - `no_lints_prime_decls.txt`: TODO document this -Other +Tool for manual maintenance - `fix_unused.py` + Bulk processing of unused variable warnings, replacing them with `_`. + +Other / uncategorized +- `autolabel.lean`, `get_tlabel.sh` +- `count-trans-deps.py` +- `import_trans_difference.sh` +- `update_PR_comment.sh` +- `import-graph-report.py` diff --git a/scripts/fix_unused.py b/scripts/fix_unused.py index 9bc5679bfdf57..9475d07bf9a89 100755 --- a/scripts/fix_unused.py +++ b/scripts/fix_unused.py @@ -2,6 +2,9 @@ # https://chatgpt.com/share/66f4e420-66bc-8001-8349-ce3cfb4f23c3 # Usage: lake build | scripts/fix_unused.py + +# Bulk processing of unused variable warnings, replacing them with `_`. + import re import sys From 3e4f35a78b35d7173243822ad580b97f27f7614a Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 30 Oct 2024 11:12:07 +0100 Subject: [PATCH 13/18] Some more tweaks and items. --- scripts/README.md | 52 +++++++++++++++++++++++++++++------------------ 1 file changed, 32 insertions(+), 20 deletions(-) diff --git a/scripts/README.md b/scripts/README.md index 60ab59f09ac35..08481e57f05d4 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -1,24 +1,26 @@ -## Miscellaneous scripts for working on mathlib +# Miscellaneous scripts for working on mathlib This directory contains miscellaneous scripts that are useful for working on or with mathlib. When adding a new script, please make sure to document it here, so other readers have a chance to learn about it as well! -**Current scripts and their purpose.** -TODO: add real content for all these entries! -Installation scripts +## Current scripts and their purpose + +**Installation scripts** - `install_debian.sh`, `install_macos.sh` - Install scripts referenced from the leanprover community install pages. + Installation scripts referenced from the leanprover community install pages. https://leanprover-community.github.io/install/debian.html https://leanprover-community.github.io/install/macos.html If these web pages are deprecated or removed, we should remove these scripts. -CI workflow +**CI workflow** - `mk_all.lean` - run via `lake exe mk_all`, regenerates `Mathlib.lean` -- `lint-style.py` and `lint-style.lean`, `print-style-errors.sh` - style linters, written in Python and Lean. + run via `lake exe mk_all`, regenerates the import-only files + `Mathlib.lean`, `Mathlib/Tactic.lean`, `Archive.lean` and `Counterexamples.lean` +- `lint-style.lean`, `lint-style.py`, `print-style-errors.sh` + style linters, written in Python and Lean. Run via `lake exe lint-style`. + Medium-term, the latter two scripts should be rewritten and incorporated in `lint-style.lean`. - `lint-bib.sh` normalize the BibTeX file `docs/references.bib` using `bibtool`. - `yaml_check.py`, `check-yaml.lean` @@ -26,15 +28,16 @@ CI workflow - `lean-pr-testing-comments.sh` Generate comments and labels on a Lean or Batteries PR after CI has finished on a `*-pr-testing-NNNN` branch. -- `update_nolints_CI.sh` (maintenance, runs once a week) +- `update_nolints_CI.sh` + Update the `nolints.json` file to remove unneeded entries. Automatically run once a week. - `bench_summary.lean` - Convert data retrieved from the speed-center into a shorter, more accessible format, + Convert data retrieved from the speed center into a shorter, more accessible format, and post a comment with this summary on github. - `declarations_diff.sh` Attempts to find which declarations have been removed and which have been added in the current PR with respect to `master`, and posts a comment on github with the result. -Managing nightly-testing and bump branches +**Managing nightly-testing and bump branches** - `create-adaptation-pr.sh` implements some of the steps in the workflow described at https://leanprover-community.github.io/contribute/tags_and_branches.html#mathlib-nightly-and-bump-branches Specifically, it will: @@ -47,23 +50,32 @@ Managing nightly-testing and bump branches If there are merge conflicts, it pauses and asks for help from the human driver. -Managing and tracking technical debt +**Managing and tracking technical debt** - `technical-debt-metrics.sh` -- `init_creation.sh` (supposed to be run manually; might be removed soon?) + Prints information on certain kind of technical debt in Mathlib. + This output is automatically posted to zulip once a week. +- `init_creation.sh` + makes sure that every file in Mathlib transitively imports `Mathlib.init` + This may be removed soon, and replaced by a different mechanism. -Mathlib tactics +**Mathlib tactics** - `polyrith_sage.py`, `polyrith_sage_helper.py` are required for `polyrith` to communication with the Sage server. -Data files with exclusions for style linters: all of these should tend to zero over time -- `nolints.json`: TODO document! -- `no_lints_prime_decls.txt`: TODO document this +**Data files with linter exceptions** +- `nolints.json` contains exceptions for all `env_linter`s in mathlib. + For permanent and deliberate exceptions, add a `@[nolint lintername]` in the .lean file instead. +- `no_lints_prime_decls.txt` + contains temporary exceptions for the `docPrime` linter + +Both of these files should tend to zero over time; +please do not add new entries to these files. PRs removing (the need for) entries are welcome. -Tool for manual maintenance +**Tool for manual maintenance** - `fix_unused.py` Bulk processing of unused variable warnings, replacing them with `_`. -Other / uncategorized +**Other / uncategorized**: TODO add documentation for them! - `autolabel.lean`, `get_tlabel.sh` - `count-trans-deps.py` - `import_trans_difference.sh` From 4c8e176d399bbb058509468d584701810ffd5bc9 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 30 Oct 2024 11:14:26 +0100 Subject: [PATCH 14/18] Tweak. --- scripts/lint-style.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index 57c5a1b1cb122..953800e9826f3 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -35,8 +35,8 @@ def allScriptsDocumented : IO Bool := do let undocumented := fileNames.filter fun script ↦ !readme.containsSubstr s!"`{script}`" && !dataFiles.contains script if undocumented.size > 0 then - IO.println s!"error: found {undocumented.size} undocumented scripts: \ - please describe the scripts in 'scripts/README.md'\n\ + IO.println s!"error: found {undocumented.size} undocumented script(s): \ + please describe the script(s) in 'scripts/README.md'\n \ {String.intercalate "," undocumented.toList}" return undocumented.size == 0 @@ -52,7 +52,7 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do allModules := allModules.append ((← IO.FS.lines s).map (·.stripPrefix "import ")) -- Note: since we manually add "Batteries" to "Mathlib.lean", we remove it here manually. allModules := allModules.erase "Batteries" - let mut numberErrors := ← lintModules allModules style fix + let mut numberErrors ← lintModules allModules style fix if !(← allScriptsDocumented) then numberErrors := numberErrors + 1 -- If run with the `--fix` argument, return a zero exit code. -- Otherwise, make sure to return an exit code of at most 125, From 92711a2c9f37786f68f4ba34687b29a5cc8ca565 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Wed, 30 Oct 2024 10:57:33 +0000 Subject: [PATCH 15/18] empty todo --- scripts/README.md | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/scripts/README.md b/scripts/README.md index 08481e57f05d4..edf35619c0253 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -36,6 +36,8 @@ to learn about it as well! - `declarations_diff.sh` Attempts to find which declarations have been removed and which have been added in the current PR with respect to `master`, and posts a comment on github with the result. +- `autolabel.lean` is the Lean script in charge of automatically adding a `t-`label on eligible PRs. + Autolabelling is inferred by which directories the current PR modifies. **Managing nightly-testing and bump branches** - `create-adaptation-pr.sh` implements some of the steps in the workflow described at @@ -75,9 +77,11 @@ please do not add new entries to these files. PRs removing (the need for) entrie - `fix_unused.py` Bulk processing of unused variable warnings, replacing them with `_`. -**Other / uncategorized**: TODO add documentation for them! -- `autolabel.lean`, `get_tlabel.sh` -- `count-trans-deps.py` -- `import_trans_difference.sh` -- `update_PR_comment.sh` -- `import-graph-report.py` +**API surrounding CI** +- `update_PR_comment.sh` is a script that edits an existing message (or creates a new one). + It is used by the `PR_summary` workflow to maintain an up-to-date report with a searchble history. +- `get_tlabel.sh` extracts the `t-`label that a PR has (assuming that there is exactly one). + It is used by the `maintainer_merge` family of workflows to dispatch `maintainer merge` requests + to the appropriate topic. +- `count-trans-deps.py`, `import-graph-report.py` and `import_trans_difference.sh` produce various + summaries of changes in transitive imports that the `PR_summary` message incorporates. From f0164928c32df485d9fdc43ebd35aa104f1f9153 Mon Sep 17 00:00:00 2001 From: grunweg Date: Wed, 30 Oct 2024 12:01:18 +0100 Subject: [PATCH 16/18] Tiny nits --- scripts/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/README.md b/scripts/README.md index edf35619c0253..125bac1235fb3 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -79,9 +79,9 @@ please do not add new entries to these files. PRs removing (the need for) entrie **API surrounding CI** - `update_PR_comment.sh` is a script that edits an existing message (or creates a new one). - It is used by the `PR_summary` workflow to maintain an up-to-date report with a searchble history. + It is used by the `PR_summary` workflow to maintain an up-to-date report with a searchable history. - `get_tlabel.sh` extracts the `t-`label that a PR has (assuming that there is exactly one). It is used by the `maintainer_merge` family of workflows to dispatch `maintainer merge` requests - to the appropriate topic. + to the appropriate topic on zulip. - `count-trans-deps.py`, `import-graph-report.py` and `import_trans_difference.sh` produce various summaries of changes in transitive imports that the `PR_summary` message incorporates. From c5843283034f08638eb399acafa7b5c63082bada Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 31 Oct 2024 10:46:19 +1100 Subject: [PATCH 17/18] document unused_in_pole.sh --- scripts/README.md | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/scripts/README.md b/scripts/README.md index 125bac1235fb3..45feac9d332ec 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -14,6 +14,17 @@ to learn about it as well! https://leanprover-community.github.io/install/macos.html If these web pages are deprecated or removed, we should remove these scripts. +**Tool for manual maintenance** +- `fix_unused.py` + Bulk processing of unused variable warnings, replacing them with `_`. + +**Analyzing Mathlib's import structure** +- `unused_in_pole.sh ` calls `lake exe pole --loc --to ` to compute the longest + pole to a given target module (defaults to `Mathlib`), and then feeds this into + `lake exe unused` to analyze transitively unused imports. + Generates `unused.md` containing a markdown table showing the unused imports, + and suggests `lake exe graph` commands to visualize the largest "rectangles" of unused imports. + **CI workflow** - `mk_all.lean` run via `lake exe mk_all`, regenerates the import-only files @@ -73,10 +84,6 @@ to learn about it as well! Both of these files should tend to zero over time; please do not add new entries to these files. PRs removing (the need for) entries are welcome. -**Tool for manual maintenance** -- `fix_unused.py` - Bulk processing of unused variable warnings, replacing them with `_`. - **API surrounding CI** - `update_PR_comment.sh` is a script that edits an existing message (or creates a new one). It is used by the `PR_summary` workflow to maintain an up-to-date report with a searchable history. From fbd5774b08d0a0fa6e0168df91c5e81463f4ce6e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 31 Oct 2024 10:55:52 +1100 Subject: [PATCH 18/18] don't put target in the backticks --- scripts/README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/scripts/README.md b/scripts/README.md index 45feac9d332ec..33a295aa934b5 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -19,8 +19,9 @@ to learn about it as well! Bulk processing of unused variable warnings, replacing them with `_`. **Analyzing Mathlib's import structure** -- `unused_in_pole.sh ` calls `lake exe pole --loc --to ` to compute the longest - pole to a given target module (defaults to `Mathlib`), and then feeds this into +- `unused_in_pole.sh` (followed by an optional ``, defaulting to `Mathlib`) + calls `lake exe pole --loc --to ` to compute the longest + pole to a given target module, and then feeds this into `lake exe unused` to analyze transitively unused imports. Generates `unused.md` containing a markdown table showing the unused imports, and suggests `lake exe graph` commands to visualize the largest "rectangles" of unused imports.