fix: if nolint files change, do a full rebuild #19275
Conversation
PR summary f706345d1aImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 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 No changes to technical debt.You can run this locally as
|
eric-wieser
changed the title
|
Thanks! bors d+ |
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Before merging, we should locally test that changing the file causes |
|
You may need to re-add the removed lemma. For instance, you could cherry-pick 2858e09. |
|
That may also serve as a test that the rebuilding will happen. |
lakefile.lean
Outdated
| @[default_target] | ||
| lean_lib Mathlib where | ||
| leanOptions := mathlibLeanOptions | ||
| -- Mathlib also enforces these linter options, which are not active by default. | ||
| moreServerOptions := mathlibOnlyLinters | ||
| extraDepTargets := #[ |
There was a problem hiding this comment.
Optional: add a comment why this is here? (Perhaps this is sufficiently obvious... I'm not sure. Up to you.)
lakefile.lean
Outdated
| @@ -62,11 +62,21 @@ package mathlib where | |||
| ## Mathlib libraries | |||
| -/ | |||
|
|
|||
| target nolints_style (pkg) : System.FilePath := | |||
| inputTextFile <| pkg.dir / "scripts" / "nolints-style.txt" | |||
There was a problem hiding this comment.
In fact, you could probably remove this one, right? nolints-style.txt is only used for lake exe lint-style, which is run as a separate executable by CI. (This is not related to syntax linters and caching their results.)
Leaving this in for paranoia is fine with me --- how about adding a comment that this is not defence in depth, and currently not actually required?
There was a problem hiding this comment.
Yes, I can; I removed it and added a comment explaining a little more about why.
In principle someone could start calling the function that reads nolints-style.txt from another linter, then suddenly we would need this again.
Probably it would be best to refactor things such that the script reads the file, and passes the result into the library function, to make it clear that the library can't read the file at import-time; but that's out of scope for this PR.
There was a problem hiding this comment.
👍 Thanks!
I'm adding the lint-style refactoring to my list of things; expect a PR within 1-2 weeks. (Currently, some more urgent things have to be finished first. But this one should be very quick, once I start it.)
There was a problem hiding this comment.
In fact, I had some time earlier - #19384 implements this.
|
Also: does |
Btw, master is "fixed" now, without this commit. I am not completely sure about what happened there... |
|
Something funny may be going on with the cache: in #19322, the step that checked the cache failed and re-running the jobs rebuilt all of mathlib again, even though the upload step had apparently worked the first time around. |
|
Perhaps relevant is that the |
|
@adomani, I take it your comment above means this PR should not be merged? |
|
I like that CI will rebuild everything if the no_lint file is modified, but I want to make sure that this change will not create issues for Simply sorting the file could be enough? Or adding an extra line break somewhere. |
For consistency with the other nolints files. Suggested in #19275.
For consistency with the other nolints files. Suggested in #19275.
Otherwise CI will succeed when removing entries from the file, but fail later when someone changes something unrelated.