mathlib3
refactor(scripts/mk_nolint): produce nolints.txt file during linting
#2194
Merged
Overview
Commits
16
Changes
View On GitHub

refactor(scripts/mk_nolint): produce nolints.txt file during linting #2194

mergify merged 16 commits into master from parlint
gebner
gebner Factor out code to determine automatically-generated declarations.
eeea36fd
gebner Mark bool.decidable_eq and decidable.to_bool as [inline]
75000b29
gebner Execute linters in parallel.
1f37c93e
gebner Add lint_mathlib.lean script.
b903c4fa
gebner Switch CI to new lint_mathlib.lean script.
6599729a
gebner Make linter fail.
8b509c58
gebner Revert "Make linter fail."
fa46d8f7
gebner Remove one line from nolints.txt
1d7bd741
gebner Change shebang in rm_all.sh to be nixos-compatible
2e861986
gebner
gebner
gebner Disable parallel checking.
be113a25
gebner gebner changed the title refactor(scripts/mk_nolint): lint in parallel and produce nolints.txt file during linting refactor(scripts/mk_nolint): produce nolints.txt file during linting 6 years ago
gebner
gebner Make linter fail.
8f5ec620
gebner Revert "Make linter fail."
fd4f5d08
cipher1024 cipher1024 requested a review from robertylewis robertylewis 6 years ago
gebner
gebner
gebner commented on 2020-03-20
robertylewis
robertylewis commented on 2020-03-20
gebner Move is_auto_decl to meta/expr.lean
635674df
gebner Remove list.mmap_async
693d653d
gebner Factor out name.from_string
6ed9a2e1
robertylewis
robertylewis approved these changes on 2020-03-21
robertylewis robertylewis added ready-to-merge
mergify[bot] Merge branch 'master' into parlint
b2f2a807
mergify mergify merged 0bd8b94d into master 6 years ago
bryangingechen bryangingechen deleted the parlint branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum