[Merged by Bors] - chore(scripts): require all scripts to be documented in the README #14539

grunweg · 2024-07-08T20:48:45Z

This is valuable so

contributors can discover existing useful tools,
existing knowledge is documented and not lost
it (hopefully) inspires to re-consider if all each script is useful/why we have it. Having a bounded number of entry-points to CI is useful to have.

This is implemented as a new check, piggy-backing the lint_style executable.

To make CI pass, this PR adds a README file to scripts, containing stub descriptions for the current files. Future PRs should fill this out.

grunweg · 2024-07-08T20:49:22Z

@semorrison You may be interested in this one: obviously, it's not ready to land yet.

github-actions · 2024-07-08T20:49:24Z

PR summary fbd5774b08

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ allScriptsDocumented

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>

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

In detail, this PR - moves the executable bit check into the .yml files, instead of the shell script - adds a `--fix` flag to `lint-style`, for fixing style errors (when possible) - moves calling `lint-style.py` into `lake exe lint-style`, and - switches the CI workflow to call `lake exe lint-style` instead, and removes `lint-style.sh` Ideally, `lint-style.py` will be completely rewritten in Lean soon, so this calling of an external process is only temporary. Helps with #14539.

kim-em · 2024-10-25T00:37:49Z

Apologies this rotted. I just merged master, hopefully it works.

I like this! Please merge if you are too, otherwise we can discuss what remains to be done.

bors d+

mathlib-bors · 2024-10-25T00:37:51Z

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

… them can come later.

scripts/README.md

grunweg · 2024-10-30T10:17:00Z

Thank you for documenting most entries! I just took a pass over the ones I know, and formatted the file consistently. This is just missing an entry on ~four scripts used to generate the PR summary comment. Help on these is still welcome - though in my opinion, this is already useful.

From my point of view, this can be merged. @bryangingechen I saw you self-assigned this. If I don't hear objections from you, I will merge this in a day (or so).

adomani · 2024-10-30T10:58:47Z

I pushed a possible categorization of the remaining scripts with some details. Let me know if this is good! A lot of these files also have individual docs, so the combination of the generic dispatch and the specific information is probably good enough.

scripts/README.md

grunweg · 2024-10-30T11:02:10Z

Thanks for adding the last missing docs! I like the changes and just pushed a last tweak. I consider this really really ready now.

kim-em · 2024-10-30T23:31:31Z

Nice! Thank @grunweg for making this happen, and @adomani and @jcommelin for contributing documentation. I feel much better about our scripts/ directory now!

Next up, rewrite all the python ones in lean. :-)

bors merge

…14539) This is valuable so - contributors can discover existing useful tools, - existing knowledge is documented and not lost - it (hopefully) inspires to re-consider if all each script is useful/why we have it. Having a [bounded number of entry-points](https://matklad.github.io/2023/12/31/O(1)-build-file.html) to CI is useful to have. This is implemented as a new check, piggy-backing the `lint_style` executable. To make CI pass, this PR adds a README file to `scripts`, containing stub descriptions for the current files. Future PRs should fill this out. Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Michael Rothgang <[email protected]> Co-authored-by: Damiano Testa <[email protected]>

mathlib-bors · 2024-10-30T23:32:30Z

Build failed:

Lint style

kim-em · 2024-10-30T23:42:57Z

Haha, it caught a new one that has arrived on master!

…d-scripts

kim-em · 2024-10-30T23:46:34Z

bors merge

…14539) This is valuable so - contributors can discover existing useful tools, - existing knowledge is documented and not lost - it (hopefully) inspires to re-consider if all each script is useful/why we have it. Having a [bounded number of entry-points](https://matklad.github.io/2023/12/31/O(1)-build-file.html) to CI is useful to have. This is implemented as a new check, piggy-backing the `lint_style` executable. To make CI pass, this PR adds a README file to `scripts`, containing stub descriptions for the current files. Future PRs should fill this out. Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Michael Rothgang <[email protected]> Co-authored-by: Damiano Testa <[email protected]>

mathlib-bors · 2024-10-30T23:47:30Z

Build failed:

Lint style

kim-em · 2024-10-30T23:57:32Z

bors merge

…14539) This is valuable so - contributors can discover existing useful tools, - existing knowledge is documented and not lost - it (hopefully) inspires to re-consider if all each script is useful/why we have it. Having a [bounded number of entry-points](https://matklad.github.io/2023/12/31/O(1)-build-file.html) to CI is useful to have. This is implemented as a new check, piggy-backing the `lint_style` executable. To make CI pass, this PR adds a README file to `scripts`, containing stub descriptions for the current files. Future PRs should fill this out. Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Michael Rothgang <[email protected]> Co-authored-by: Damiano Testa <[email protected]>

mathlib-bors · 2024-10-31T00:31:46Z

Pull request successfully merged into master.

Build succeeded:

grunweg · 2024-10-31T08:03:28Z

Next up, rewrite all the python ones in lean. :-)

@kim-em I do have some in-progress PRs regarding this; review welcome :-)

feat: rewrite the trailing whitespace linter in Lean #16334 and feat: rewrite the linter for spaces before semicolons in Lean #16532 (depending on the former) rewrite two more style linters from Python in Lean
feat: rewrite the duplicateImports linter #17555 rewrites a text-based linter as a syntax linter instead
[Merged by Bors] - feat: remove the text-based linters for module docstring, copyright and author lines #17556 removes Python linters which have been rewritten as syntax linters
chore: import the header linter in all files imported in Mathlib.Init #18275 and feat: check that every file imports Mathlib.Init #18281 rewrite init_creation.sh as a text-based Lean linter

grunweg added WIP Work in progress t-linter Linter labels Jul 8, 2024

wip: require all scripts to be documented

ee8a6aa

grunweg force-pushed the MR-lint-undocumented-scripts branch from f332ff6 to ee8a6aa Compare July 9, 2024 07:00

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 13, 2024

grunweg mentioned this pull request Jul 28, 2024

[Merged by Bors] - chore: remove fix-comments.py #15242

Closed

grunweg mentioned this pull request Aug 15, 2024

[Merged by Bors] - feat: remove lint-style.sh #15051

Closed

grunweg mentioned this pull request Sep 7, 2024

[Merged by Bors] - chore: remove scripts/fix-by-linebreaks.sh #16563

Closed

kim-em added 2 commits October 25, 2024 11:33

rename to match master

7abe395

merge master

73ee84e

github-actions bot added the delegated label Oct 25, 2024

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 25, 2024

grunweg added 9 commits October 27, 2024 14:38

Actually run the check: now it fails, of course.

cdaa88a

chore: add stub README

842f09d

Tweak further

5c6b5d6

Small fixes

bc5647a

TEMP

27b54ec

Fix filtering logic: operate on filenames only

5b56b6f

Add stub entries for the scripts, at least classify them. Documenting…

23b6c98

… them can come later.

Merge branch 'master' into MR-lint-undocumented-scripts

5fbc98f

Untemp

1925b25

grunweg removed the WIP Work in progress label Oct 27, 2024

jcommelin reviewed Oct 29, 2024

View reviewed changes

scripts/README.md Outdated Show resolved Hide resolved

kim-em and others added 3 commits October 30, 2024 13:11

work on the README

750a059

Some more tweaks and items.

3e4f35a

Tweak.

4c8e176

empty todo

92711a2

grunweg commented Oct 30, 2024

View reviewed changes

scripts/README.md Outdated Show resolved Hide resolved

scripts/README.md Outdated Show resolved Hide resolved

Tiny nits

f016492

github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 30, 2024

kim-em added 2 commits October 31, 2024 10:44

Merge remote-tracking branch 'origin/master' into MR-lint-undocumente…

915c07c

…d-scripts

document unused_in_pole.sh

c584328

don't put target in the backticks

fbd5774

kim-em mentioned this pull request Oct 30, 2024

[Merged by Bors] - feat: add deprecation script #18150

Closed

mathlib-bors bot changed the title ~~chore(scripts): require all scripts to be documented in the README~~ [Merged by Bors] - chore(scripts): require all scripts to be documented in the README Oct 31, 2024

mathlib-bors bot closed this Oct 31, 2024

mathlib-bors bot deleted the MR-lint-undocumented-scripts branch October 31, 2024 00:31

bryangingechen mentioned this pull request Oct 31, 2024

feat: add Dockerfiles for lean and mathlib #15936

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(scripts): require all scripts to be documented in the README #14539

[Merged by Bors] - chore(scripts): require all scripts to be documented in the README #14539

grunweg commented Jul 8, 2024 •

edited

Loading

grunweg commented Jul 8, 2024 •

edited

Loading

github-actions bot commented Jul 8, 2024 •

edited

Loading

kim-em commented Oct 25, 2024

mathlib-bors bot commented Oct 25, 2024

grunweg commented Oct 30, 2024

adomani commented Oct 30, 2024

grunweg commented Oct 30, 2024

kim-em commented Oct 30, 2024

mathlib-bors bot commented Oct 30, 2024

kim-em commented Oct 30, 2024

kim-em commented Oct 30, 2024

mathlib-bors bot commented Oct 30, 2024

kim-em commented Oct 30, 2024

mathlib-bors bot commented Oct 31, 2024

grunweg commented Oct 31, 2024

[Merged by Bors] - chore(scripts): require all scripts to be documented in the README #14539

[Merged by Bors] - chore(scripts): require all scripts to be documented in the README #14539

Conversation

grunweg commented Jul 8, 2024 • edited Loading

grunweg commented Jul 8, 2024 • edited Loading

github-actions bot commented Jul 8, 2024 • edited Loading

PR summary fbd5774b08

Import changes for modified files

Declarations diff

kim-em commented Oct 25, 2024

mathlib-bors bot commented Oct 25, 2024

grunweg commented Oct 30, 2024

adomani commented Oct 30, 2024

grunweg commented Oct 30, 2024

kim-em commented Oct 30, 2024

mathlib-bors bot commented Oct 30, 2024

kim-em commented Oct 30, 2024

kim-em commented Oct 30, 2024

mathlib-bors bot commented Oct 30, 2024

kim-em commented Oct 30, 2024

mathlib-bors bot commented Oct 31, 2024

grunweg commented Oct 31, 2024

grunweg commented Jul 8, 2024 •

edited

Loading

grunweg commented Jul 8, 2024 •

edited

Loading

github-actions bot commented Jul 8, 2024 •

edited

Loading