mathlib3
refactor(scripts/mk_nolint): produce nolints.txt file during linting
#2194
Merged
Overview
Commits
16
Changes
View On GitHub
Commits
  • Factor out code to determine automatically-generated declarations.
    gebner committed 6 years ago
  • Mark bool.decidable_eq and decidable.to_bool as [inline]
    gebner committed 6 years ago
  • Execute linters in parallel.
    gebner committed 6 years ago
  • Add lint_mathlib.lean script.
    gebner committed 6 years ago
  • Switch CI to new lint_mathlib.lean script.
    gebner committed 6 years ago
  • Make linter fail.
    gebner committed 6 years ago
  • Revert "Make linter fail."
    gebner committed 6 years ago
  • Remove one line from nolints.txt
    gebner committed 6 years ago
  • Change shebang in rm_all.sh to be nixos-compatible
    gebner committed 6 years ago
  • Disable parallel checking.
    gebner committed 6 years ago
  • Make linter fail.
    gebner committed 6 years ago
  • Revert "Make linter fail."
    gebner committed 6 years ago
  • Move is_auto_decl to meta/expr.lean
    gebner committed 6 years ago
  • Remove list.mmap_async
    gebner committed 6 years ago
  • Factor out name.from_string
    gebner committed 6 years ago
  • Merge branch 'master' into parlint
    mergify[bot] committed 6 years ago
FAQ Terms Privacy Refunds Impressum
Loading