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 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>

.github/workflows/build.yml

@@ -97,9 +97,11 @@ jobs:
 
       - name: lint
         run: |
-          ./scripts/mk_all.sh -t
-          lean src/lint_mathlib.lean
+          ./scripts/mk_all.sh
+          lean --run scripts/lint_mathlib.lean
+          mv nolints.txt scripts/nolints.txt
           ./scripts/rm_all.sh
+          git diff
 
       - name: leanchecker
         run: |

.gitignore

@@ -4,6 +4,4 @@
 _cache
 __pycache__
 all.lean
-lint_mathlib.lean
-nolints.lean
 *.depend

scripts/lint_mathlib.lean

@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2020 Robert Y. Lewis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Robert Y. Lewis, Gabriel Ebner
+-/
+
+import tactic.lint system.io  -- these are required
+import all   -- then import everything, to parse the library for failing linters
+
+/-!
+# lint_mathlib
+
+Script that runs the linters listed in `mathlib_linters` on all of mathlib.
+As a side effect, the file `nolints.txt` is generated in the current
+directory. This script needs to be run in the root directory of mathlib.
+
+It assumes that files generated by `mk_all.sh` are present.
+
+This is used by the CI script for mathlib.
+
+Usage: `lean --run scripts/lint_mathlib.lean`
+-/
+
+open native
+
+/--
+Returns the contents of the `nolints.txt` file.
+-/
+meta def mk_nolint_file (env : environment) (mathlib_path_len : ℕ)
+  (results : list (name × linter × rb_map name string)) : format := do
+let failed_decls_by_file := rb_lmap.of_list (do
+  (linter_name, _, decls) ← results,
+  (decl_name, _) ← decls.to_list,
+  let file_name := (env.decl_olean decl_name).get_or_else "",
+  pure (file_name.popn mathlib_path_len, decl_name.to_string, linter_name.last)),
+format.intercalate format.line $
+"import .all" ::
+"run_cmd tactic.skip" :: do
+(file_name, decls) ← failed_decls_by_file.to_list.reverse,
+"" :: ("-- " ++ file_name) :: do
+(decl, linters) ← (rb_lmap.of_list decls).to_list.reverse,
+pure $ "apply_nolint " ++ decl ++ " " ++ " ".intercalate linters
+
+/--
+Parses the list of lines of the `nolints.txt` into an `rb_lmap` from linters to declarations.
+-/
+meta def parse_nolints (lines : list string) : rb_lmap name name :=
+rb_lmap.of_list $ do
+line ← lines,
+guard $ line.front = 'a',
+_ :: decl :: linters ← pure $ line.split (= ' ') | [],
+let decl := name.from_string decl,
+linter ← linters,
+pure (linter, decl)
+
+open io io.fs
+
+/--
+Reads the `nolints.txt`, and returns it as an `rb_lmap` from linters to declarations.
+-/
+meta def read_nolints_file (fn := "scripts/nolints.txt") : io (rb_lmap name name) := do
+cont ← io.fs.read_file fn,
+pure $ parse_nolints $ cont.to_string.split (= '\n')
+
+meta instance coe_tactic_to_io {α} : has_coe (tactic α) (io α) :=
+⟨run_tactic⟩
+
+/--
+Writes a file with the given contents.
+-/
+meta def io.write_file (fn : string) (contents : string) : io unit := do
+h ← mk_file_handle fn mode.write,
+put_str h contents,
+close h
+
+/-- Runs when called with `lean --run` -/
+meta def main : io unit := do
+env ← tactic.get_env,
+decls ← lint_mathlib_decls,
+linters ← get_linters mathlib_linters,
+mathlib_path_len ← string.length <$> tactic.get_mathlib_dir,
+let non_auto_decls := decls.filter (λ d, ¬ d.is_auto_or_internal env),
+results₀ ← lint_core decls non_auto_decls linters,
+nolint_file ← read_nolints_file,
+let results := (do
+  (linter_name, linter, decls) ← results₀,
+  [(linter_name, linter, (nolint_file.find linter_name).foldl rb_map.erase decls)]),
+io.print $ to_string $ format_linter_results env results decls non_auto_decls
+  mathlib_path_len "in mathlib" tt tt,
+io.write_file "nolints.txt" $ to_string $ mk_nolint_file env mathlib_path_len results₀,
+if results.all (λ r, r.2.2.empty) then pure () else io.fail ""

scripts/mk_all.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 # Makes a file all.lean in all subfolders of src/ importing all files in that folder,
 # including subfolders.
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
@@ -13,28 +13,3 @@ do
   sed 's/$/\.all/; s/\.lean\.all//; s/^\.\//       \./; 1s/^      /import/' >> all.lean
   # Now modify this output so that Lean can parse it. Changes `./foo.lean` to `.foo` and `foodir` to `.foodir.all`. Also adds indentation, a comment and `import`. Write this to `all.lean`
 done
-
-nolint=0
-while getopts 't' opt; do
-  case $opt in
-    t) nolint=1 ;;
-    *) echo 'Error in command line parsing' >&2
-       exit 1
-  esac
-done
-
-cd $DIR/../src/
-if [ "$nolint" -eq 1 ]; then
-  cp ../scripts/nolints.txt ./nolints.lean
-  cat <<EOT > lint_mathlib.lean
-import .nolints
-EOT
-else
-  cat <<EOT > lint_mathlib.lean
-import all
-EOT
-fi
-
-cat <<EOT >> lint_mathlib.lean
-#eval lint_mathlib_ci
-EOT

scripts/rm_all.sh

@@ -1,9 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 # Removes all files named all.lean in the src/ directory
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 find $DIR/../src/ -name 'all.lean' -delete -o -name 'all.olean' -delete
-# Removes src/lint_mathlib.lean, which is also created by `mk_all.sh`
-rm $DIR/../src/lint_mathlib.lean
-if test -f "$DIR/../src/nolints.lean"; then
-  rm $DIR/../src/nolints.lean
-fi

scripts/update_nolints.sh

@@ -3,11 +3,6 @@ DEPLOY_NIGHTLY_GITHUB_USER=leanprover-community-bot
 set -e
 set -x
 
-cd scripts
-./mk_all.sh
-lean --run mk_nolint.lean
-./rm_all.sh
-
-git add nolints.txt
+git add scripts/nolints.txt
 git commit -m "chore(scripts): update nolints.txt" || true
 git push origin-bot HEAD:master || true

src/logic/basic.lean

@@ -26,6 +26,7 @@ section miscellany
   `if p ∧ q then ... else ...` will not evaluate the decidability of `q` if `p` is false. -/
 attribute [inline] and.decidable or.decidable decidable.false xor.decidable iff.decidable
   decidable.true implies.decidable not.decidable ne.decidable
+  bool.decidable_eq decidable.to_bool
 
 variables {α : Type*} {β : Type*}
 

src/logic/function.lean

@@ -41,6 +41,8 @@ lemma comp_apply {α : Sort u} {β : Sort v} {φ : Sort w} (f : β → φ) (g :
 lemma injective.ne (hf : function.injective f) {a₁ a₂ : α} : a₁ ≠ a₂ → f a₁ ≠ f a₂ :=
 mt (assume h, hf h)
 
+/-- If the co-domain `β` of an injective function `f : α → β` has decidable equality, then
+the domain `α` also has decidable equality. -/
 def injective.decidable_eq [decidable_eq β] (I : injective f) : decidable_eq α
 | a b := decidable_of_iff _ I.eq_iff
 

src/meta/expr.lean

@@ -128,11 +128,22 @@ meta def add_prime : name → name
 | (name.mk_string s p) := name.mk_string (s ++ "'") p
 | n := (name.mk_string "x'" n)
 
+/--
+Returns the last non-numerical component of a name, or `"[anonymous]"` otherwise.
+-/
 def last_string : name → string
 | anonymous        := "[anonymous]"
 | (mk_string s _)  := s
 | (mk_numeral _ n) := last_string n
 
+/--
+Constructs a (non-simple) name from a string.
+
+Example: ``name.from_string "foo.bar" = `foo.bar``
+-/
+meta def from_string (s : string) : name :=
+from_components $ s.split (= '.')
+
 end name
 
 namespace level
@@ -642,6 +653,12 @@ e.is_constructor d.to_name ∨
   "rec", "rec_on", "no_confusion", "no_confusion_type", "sizeof", "ibelow", "has_sizeof_inst"]) ∨
 d.to_name.has_prefix (λ nm, e.is_ginductive' nm)
 
+/--
+Returns true iff `d` is an automatically-generated or internal declaration.
+-/
+meta def is_auto_or_internal (env : environment) (d : declaration) : bool :=
+d.to_name.is_internal || d.is_auto_generated env
+
 /-- Returns the list of universe levels of a declaration. -/
 meta def univ_levels (d : declaration) : list level :=
 d.univ_params.map level.param