Zulip Chat Archive

Stream: mathlib4

Topic: auto-fix comments

Johan Commelin (Jan 20 2023 at 09:15):

Reid and I wrote a script that will interactively try to fix names in comments, using #align mappings:
https://github.com/leanprover-community/mathlib4/pull/1710

Johan Commelin (Jan 20 2023 at 09:18):

It is somewhat tested. The way we had in mind to use this is:

  • start your port with start_port.sh
  • manually fix errors (red stuff), including names of declarations and #align statements
  • run ./scripts/fix-lints.py FILENAME to fix a whole lot of warnings
  • run ./scripts/fix-comments.py FILENAME (this script) to fix names in comments
  • manually fix whatever remains to be done

Reid Barton (Jan 20 2023 at 09:42):

One caveat is that many lean 3 definitions from the core library are missing #aligns (unless they were added since yesterday), e.g. fin, group

Patrick Massot (Jan 20 2023 at 09:43):

I think you can add those anywhere in mathlib4

Johan Commelin (Jan 20 2023 at 12:32):

Another catch: the tool does not yet fix docstrings in @[to_additive "some additive docstring goes here"]

Reid Barton (Jan 20 2023 at 14:48):

Another caveat is that the tool doesn't guess what namespace the comments are supposed to be referring to

Johan Commelin (Jan 23 2023 at 15:08):

@ porters: this script has been merged

Johan Commelin (Jan 23 2023 at 15:08):

Please report any issues

Eric Wieser (Jan 23 2023 at 15:14):

Issue: I pushed a fix at the same time it was put on the queue, so actually, it hasn't been merged yet

Eric Wieser (Jan 23 2023 at 15:16):

(and now lake exe cache get is failing with network errors so bors refuses to merge it)

Yury G. Kudryashov (May 25 2023 at 21:13):

!4#4360 touches 326 files

Ruben Van de Velde (May 25 2023 at 21:36):

Just 6 comments

Last updated: Dec 20 2023 at 11:08 UTC