-
Notifications
You must be signed in to change notification settings - Fork 892
chore(Tactic/Linters): remove public section
#31803
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
Conversation
PR summary 082440f5b2Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| /-- Verifies that all modules in `modules` are named in `UpperCamelCase` | ||
| (except for explicitly discussed exceptions, which are hard-coded here). | ||
| Return the number of modules violating this. -/ | ||
| public -- only for MathlibTest/ModuleCase.lean |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
One might argue that this is useful public API (as evidenced by the unit tests). If so, I'll be happy to remove the comment.
| Source: https://learn.microsoft.com/en-gb/windows/win32/fileio/naming-a-file. | ||
| Return the number of module names violating this rule. -/ | ||
| public -- only for `MathlibTest/ForbiddenModuleNames` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As above
public sectionpublic section
|
!bench |
|
(Just in case, I would be a bit surprised to see any effect.) |
|
Benchmark results for 97e228b against 6a54a80 are in! @grunweg |
|
Here are the benchmark results for commit 97e228b. |
2 files, Instructions +1.0⬝10⁹
|
should MathlibTest also allow the module system instead?
97e228b to
109460f
Compare
|
This PR/issue depends on:
|
Mostly as a learning exercise for me to understand the module system better.