This repository was archived by the owner on Jul 24, 2024. It is now read-only.
refactor(scripts/mk_nolint): produce nolints.txt file during linting#2194
Merged
Conversation
This reverts commit 8b509c5.
Member
Author
|
See #2170 (comment) for more motivation. |
Member
Author
|
So apparently lean segfaults now... And I can't debug it because CI doesn't upload oleans for branches that have been updated since. (Ok, I know just have to wait but I'm impatient.) |
gebner
changed the title
Member
Author
|
So the parallelization code triggers a Lean bug: leanprover-community/lean#151 I've removed that part. Now the PR only combines the |
This reverts commit 8f5ec62.
Member
Author
|
CI fails as expected when there's a linting error: https://github.com/leanprover-community/mathlib/runs/520528765 The The only thing that could fail after merging to master is the |
gebner
commented
Mar 20, 2020
Member
robertylewis
left a comment
robertylewis
left a comment
There was a problem hiding this comment.
Thanks for doing this! Looks generally good to me. We can add the parallel part back in if/when the Lean bug gets fixed.
robertylewis
approved these changes
Mar 21, 2020
robertylewis
added
the
ready-to-merge
cipher1024
pushed a commit
that referenced
this pull request
Apr 20, 2020
…2194) * Factor out code to determine automatically-generated declarations. * Mark bool.decidable_eq and decidable.to_bool as [inline] * Execute linters in parallel. * Add lint_mathlib.lean script. * Switch CI to new lint_mathlib.lean script. * Make linter fail. * Revert "Make linter fail." This reverts commit 8b509c5. * Remove one line from nolints.txt * Change shebang in rm_all.sh to be nixos-compatible * Disable parallel checking. * Make linter fail. * Revert "Make linter fail." This reverts commit 8f5ec62. * Move is_auto_decl to meta/expr.lean * Remove list.mmap_async * Factor out name.from_string Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
butterthebuddha
pushed a commit
to butterthebuddha/mathlib
that referenced
this pull request
May 15, 2020
…eanprover-community#2194) * Factor out code to determine automatically-generated declarations. * Mark bool.decidable_eq and decidable.to_bool as [inline] * Execute linters in parallel. * Add lint_mathlib.lean script. * Switch CI to new lint_mathlib.lean script. * Make linter fail. * Revert "Make linter fail." This reverts commit 8b509c5. * Remove one line from nolints.txt * Change shebang in rm_all.sh to be nixos-compatible * Disable parallel checking. * Make linter fail. * Revert "Make linter fail." This reverts commit 8f5ec62. * Move is_auto_decl to meta/expr.lean * Remove list.mmap_async * Factor out name.from_string Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
butterthebuddha
pushed a commit
to butterthebuddha/mathlib
that referenced
this pull request
May 16, 2020
…eanprover-community#2194) * Factor out code to determine automatically-generated declarations. * Mark bool.decidable_eq and decidable.to_bool as [inline] * Execute linters in parallel. * Add lint_mathlib.lean script. * Switch CI to new lint_mathlib.lean script. * Make linter fail. * Revert "Make linter fail." This reverts commit 8b509c5. * Remove one line from nolints.txt * Change shebang in rm_all.sh to be nixos-compatible * Disable parallel checking. * Make linter fail. * Revert "Make linter fail." This reverts commit 8f5ec62. * Move is_auto_decl to meta/expr.lean * Remove list.mmap_async * Factor out name.from_string Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This changes linting in the following way:
Linters are executed in parallel. Unfortunately I don't think we can execute the linter for each declaration in parallel, because spawning tasks is a bit slow in Lean 3 (see comment inThere is a bug in Lean.list.mmap_async).nolints.txtfile is generated directly during the linting step.Before this PR, we ran the all the linters twice. Once to to produce the warnings and fail CI, and then to update the
nolints.txtfile. Therefore the linting steps in CI on the master branch take about 50 minutes. After this PR, we only run the linters one and furthermore in parallel as well. I hope that linting will now in total only take ~15 minutes or so.The last few commits in this PR test two things in the CI setup:
nolints.txtfile is updated correctly. This is the "Remove one line from nolints.txt" commit. The linting step runsgit diffto show the changes, so we can check this even on a PR build.The
git commitstep could still fail on master, so we need to keep an eye out for that eventuality.TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list