[Merged by Bors] - ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter #5330

bryangingechen · 2020-12-12T04:58:21Z

As requested on Zulip, the reserved notation linter checks for reserve or precedence at the start of a non-comment, non-string literal line in any file other than tactic.core.

The new set_option linter disallows set_option pp, set_option profiler and set_option trace at the start of a non-comment, non-string literal line.

I also noticed that the small_alpha_vrachy_check linter added in #4802 wasn't actually called, so I added it to the main lint function.

~~I haven't fixed the initial issues yet.~~

~~I'll add the set_option linter to fix #1608 soon.~~

bryangingechen · 2020-12-12T04:58:52Z

For convenience, here are the initial issues:

src/order/lattice.lean : line 25 : ERR_RNT : Reserved notation outside tactic.core
src/order/lattice.lean : line 26 : ERR_RNT : Reserved notation outside tactic.core
src/meta/expr.lean : line 164 : ERR_SAV : File contains the character ᾰ
src/meta/expr.lean : line 167 : ERR_SAV : File contains the character ᾰ
src/meta/expr.lean : line 170 : ERR_SAV : File contains the character ᾰ
src/meta/expr.lean : line 178 : ERR_SAV : File contains the character ᾰ
src/meta/expr.lean : line 184 : ERR_SAV : File contains the character ᾰ
src/meta/expr.lean : line 190 : ERR_SAV : File contains the character ᾰ
src/meta/expr.lean : line 194 : ERR_SAV : File contains the character ᾰ
src/meta/expr.lean : line 196 : ERR_SAV : File contains the character ᾰ
src/meta/expr.lean : line 203 : ERR_SAV : File contains the character ᾰ
src/tactic/fresh_names.lean : line 100 : ERR_RNT : Reserved notation outside tactic.core
src/tactic/lift.lean : line 133 : ERR_RNT : Reserved notation outside tactic.core
src/tactic/localized.lean : line 38 : ERR_RNT : Reserved notation outside tactic.core
src/tactic/rcases.lean : line 616 : ERR_RNT : Reserved notation outside tactic.core
src/tactic/where.lean : line 153 : ERR_RNT : Reserved notation outside tactic.core
src/tactic/lint/frontend.lean : line 49 : ERR_RNT : Reserved notation outside tactic.core
src/tactic/lint/frontend.lean : line 50 : ERR_RNT : Reserved notation outside tactic.core
src/tactic/lint/frontend.lean : line 51 : ERR_RNT : Reserved notation outside tactic.core
src/tactic/lint/frontend.lean : line 52 : ERR_RNT : Reserved notation outside tactic.core
src/tactic/simps.lean : line 36 : ERR_RNT : Reserved notation outside tactic.core
src/logic/relator.lean : line 11 : ERR_RNT : Reserved notation outside tactic.core
src/linear_algebra/basic.lean : line 59 : ERR_RNT : Reserved notation outside tactic.core

bryangingechen · 2020-12-12T05:48:14Z

Should I go ahead and move all the instances of reserved notation to some section of tactic.core?

I'll add the exceptions for the ᾰ check to copy-mod-doc-exceptions.txt.

jcommelin · 2020-12-12T06:21:17Z

Yup, sounds good

…n_style_linter

bryangingechen · 2020-12-12T07:27:31Z

scripts/copy-mod-doc-exceptions.txt

@@ -1164,10 +1155,11 @@ src/logic/function/basic.lean : line 324 : ERR_LIN : Line has more than 100 char
 src/logic/function/basic.lean : line 498 : ERR_LIN : Line has more than 100 characters
 src/logic/function/basic.lean : line 538 : ERR_LIN : Line has more than 100 characters
 src/logic/relation.lean : line 10 : ERR_MOD : Module docstring missing, or too late
+src/logic/relator.lean : line 12 : ERR_RNT : Reserved notation outside tactic.core


I left logic.relator alone since it doesn't have any imports.

bryangingechen · 2020-12-12T09:52:22Z

Setting to WIP; I'll add another style linter that addresses #1608.

…ctions

bryangingechen · 2020-12-12T22:37:12Z

scripts/lint-copy-mod-doc.py

+def skip_comments(enumerate_lines):
+    in_comment = False
+    for line_nr, line in enumerate_lines:
+        if "/-" in line:
+            in_comment = True
+        if "-/" in line:
+            in_comment = False
+            continue
+        if line == "\n" or in_comment:
+            continue
+        yield line_nr, line
+
+def skip_string(enumerate_lines):
+    in_string = False
+    in_comment = False
+    for line_nr, line in enumerate_lines:
+        # ignore comment markers inside string literals
+        if not in_string:
+            if "/-" in line:
+                in_comment = True
+            if "-/" in line:
+                in_comment = False
+        # ignore quotes inside comments
+        if not in_comment:
+            # crude heuristic: if the number of non-escaped quote signs is odd,
+            # we're starting / ending a string literal
+            if line.count("\"") - line.count("\\\"") % 2 == 1:
+                in_string = not in_string
+            # if there are quote signs in this line,
+            # a string literal probably begins and / or ends here,
+            # so we skip this line
+            if line.count("\"") > 0:
+                continue
+            if in_string:
+                continue
+        yield line_nr, line


I factored out some generator functions that attempt to skip over block comments and string literals. skip_string feels a bit complex, but it does reduce the number of false positives.

robertylewis

Thanks very much for implementing this! I didn't carefully read the script, but it looks good at a glance and seems to work. The heuristics you point out don't seem likely to cause problems.

Just one small comment.

bors d+

robertylewis · 2020-12-14T15:10:15Z

src/tactic/core.lean

@@ -2306,3 +2306,39 @@ Otherwise, it fails.
 meta def list.find_defeq (red : tactic.transparency) {v} (m : list (expr × v)) (e : expr) :
  tactic (expr × v) :=
 m.mfind $ λ ⟨e', val⟩, tactic.is_def_eq e e' red
+
+/-!


I think tactic.core is an odd place for this. A lot of the notations are for tactics, but not all. Would it be better in a dedicated file as high in the import hierarchy as we can get it? (Imported by tactic.core or logic.basic or whatever.)

Yeah, I think it does make more sense to have a dedicated file. How about tactic.notations, imported by tactic.core?

I settled on tactic.reserved_notation, and I added it to the imports of logic.basic and logic.relator.

I'll push the commit after today's nolints update.

bors · 2020-12-14T15:11:26Z

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

…n_style_linter

scripts/lint-copy-mod-doc.py

Co-authored-by: Johan Commelin <johan@commelin.net>

bryangingechen · 2020-12-15T17:16:37Z

OK, let's see how it goes 🤞
bors r+

…s, enable small_alpha_vrachy_check linter (#5330) [As requested on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/the.20word.20.22to.22/near/219370843), the reserved notation linter checks for `reserve` or `precedence` at the start of a non-comment, non-string literal line in any file other than `tactic.core`. The new set_option linter disallows `set_option pp`, `set_option profiler` and `set_option trace` at the start of a non-comment, non-string literal line. I also noticed that the `small_alpha_vrachy_check` linter added in #4802 wasn't actually called, so I added it to the main `lint` function.

bors · 2020-12-15T21:07:49Z

Pull request successfully merged into master.

Build succeeded:

ci(lint-copy-mod-doc.py): add reserved notation linter

dc1905b

bryangingechen added WIP Work in progress RFC Request for comment CI This issue or PR is about continuous integration labels Dec 12, 2020

bryangingechen requested review from gebner, digama0 and robertylewis December 12, 2020 04:58

bryangingechen added 3 commits December 12, 2020 02:00

Merge remote-tracking branch 'community/master' into reserved_notatio…

2e1faef

…n_style_linter

fix line numbers, skip comments

989232b

move notation, add exceptions

a7fb357

bryangingechen commented Dec 12, 2020

View reviewed changes

bryangingechen added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Dec 12, 2020

fix?

5799cbc

digama0 approved these changes Dec 12, 2020

View reviewed changes

bryangingechen changed the title ~~ci(lint-copy-mod-doc.py): add reserved notation linter~~ ci(lint-copy-mod-doc.py): add reserved notation linter, enable small_alpha_vrachy_check linter Dec 12, 2020

bryangingechen added the WIP Work in progress label Dec 12, 2020

bryangingechen changed the title ~~ci(lint-copy-mod-doc.py): add reserved notation linter, enable small_alpha_vrachy_check linter~~ ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter Dec 12, 2020

add set_option_check, factor out skip_comment and add skip_string fun…

d73dda6

…ctions

bryangingechen commented Dec 12, 2020

View reviewed changes

bryangingechen removed the WIP Work in progress label Dec 12, 2020

robertylewis approved these changes Dec 14, 2020

View reviewed changes

robertylewis added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 14, 2020

move notation to tactic/reserved_notation.lean

7b04447

bryangingechen added 3 commits December 14, 2020 22:55

Merge remote-tracking branch 'community/master' into reserved_notatio…

c5192bc

…n_style_linter

fix

95b31e2

lint tactic/core.lean again

5eee23b

jcommelin reviewed Dec 15, 2020

View reviewed changes

scripts/lint-copy-mod-doc.py Outdated Show resolved Hide resolved

Update scripts/lint-copy-mod-doc.py

fafeec3

Co-authored-by: Johan Commelin <johan@commelin.net>

bryangingechen added delegated The PR author may merge after reviewing final suggestions. and removed RFC Request for comment labels Dec 15, 2020

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 15, 2020

bors bot changed the title ~~ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter~~ [Merged by Bors] - ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter Dec 15, 2020

bors bot closed this Dec 15, 2020

bors bot deleted the reserved_notation_style_linter branch December 15, 2020 21:07

fpvandoorn mentioned this pull request May 11, 2022

catch leftover set_option commands #1608

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter #5330

[Merged by Bors] - ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter #5330

bryangingechen commented Dec 12, 2020 •

edited

bryangingechen commented Dec 12, 2020

bryangingechen commented Dec 12, 2020

jcommelin commented Dec 12, 2020

bryangingechen Dec 12, 2020

bryangingechen commented Dec 12, 2020

bryangingechen Dec 12, 2020

robertylewis left a comment

robertylewis Dec 14, 2020

bryangingechen Dec 14, 2020

bryangingechen Dec 15, 2020

bors bot commented Dec 14, 2020

bryangingechen commented Dec 15, 2020

bors bot commented Dec 15, 2020

[Merged by Bors] - ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter #5330

[Merged by Bors] - ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter #5330

Conversation

bryangingechen commented Dec 12, 2020 • edited

bryangingechen commented Dec 12, 2020

bryangingechen commented Dec 12, 2020

jcommelin commented Dec 12, 2020

bryangingechen Dec 12, 2020

Choose a reason for hiding this comment

bryangingechen commented Dec 12, 2020

bryangingechen Dec 12, 2020

Choose a reason for hiding this comment

robertylewis left a comment

Choose a reason for hiding this comment

robertylewis Dec 14, 2020

Choose a reason for hiding this comment

bryangingechen Dec 14, 2020

Choose a reason for hiding this comment

bryangingechen Dec 15, 2020

Choose a reason for hiding this comment

bors bot commented Dec 14, 2020

bryangingechen commented Dec 15, 2020

bors bot commented Dec 15, 2020

bryangingechen commented Dec 12, 2020 •

edited