build(travis): interrupt the built at the first error message

.travis.yml

@@ -34,11 +34,11 @@ jobs:
   include:
     - stage: Pre-build-1
       script:
-        - travis_long "timeout 2400 leanpkg test" || true
+        - travis_long "timeout 2400 leanpkg test" | python scripts/detect_errors.py
 
     - stage: Pre-build-2
       script:
-        - travis_long "timeout 2400 leanpkg test" || true
+        - travis_long "timeout 2400 leanpkg test" | python scripts/detect_errors.py
 
     - stage: Test
       script:

scripts/detect_errors.py

@@ -0,0 +1,15 @@
+
+import sys
+
+try:
+    for line in sys.stdin:
+        sys.stdout.write(line)
+        if 'error' in line: raise sys.exit()
+except:
+    try:
+        for i in range(20):
+            line = sys.stdin.next()
+            if not line: break
+            sys.stdout.write(line)
+    finally:
+        sys.exit(-1)

src/tactic/interactive.lean

@@ -182,10 +182,10 @@ optional arguments:
         this tactic fails, the corresponding assumption will be rejected and
         the next one will be attempted.
 -/
-meta def apply_assumption
+meta def apply_assumptio
   (asms : tactic (list expr) := local_context)
   (tac : tactic unit := return ()) : tactic unit :=
-tactic.apply_assumption asms tac
+tactic.apply_assumptio asms tac
 
 open nat