feat(.travis.yml): add linting to test stage (#1606)

leanprover-community · Oct 30, 2019 · d43f7f9 · d43f7f9
1 parent aadfde6
commit d43f7f9
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/.travis.yml b/.travis.yml
@@ -37,6 +37,7 @@ install:
   - if [ $RESULT -eq 0 ]; then git checkout -f HEAD ; fi
   - git clean -d -f -q
   - ./purge_olean.sh
+  - bash scripts/rm_all.sh || true
   - rm mathlib.txt || true
   - export LEAN_VERSION=lean-`lean --run scripts/lean_version.lean`
 
@@ -78,6 +79,9 @@ jobs:
         - travis_long "leanpkg test"
         - lean --recursive --export=mathlib.txt src/
         - travis_long "leanchecker mathlib.txt"
+        - bash scripts/mk_all.sh
+        - travis_long "lean src/lint_mathlib.lean"
+        - bash scripts/rm_all.sh
         - sh scripts/deploy_nightly.sh
 
     - stage: Test

diff --git a/scripts/mk_all.sh b/scripts/mk_all.sh
@@ -20,5 +20,5 @@ import all
 
 open nat -- need to do something before running a command
 
-#lint_mathlib
+#lint_mathlib- only def_lemma dup_namespace
 EOT