mathlib

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

refactor(scripts/mk_nolint): produce nolints.txt file during linting (#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 8b509c5815d862d0d060eac407cf6d22d743f960. * 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 8f5ec62030ecaec93d01981b273c2a737d67eddf. * 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>