From b2b78eb2229a5a778112bd76ccd44dcf6084e8b2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 15 Jan 2021 15:44:32 +0100 Subject: [PATCH] test: use `printMessageEndPos` for leantests --- tests/lean/217.lean.expected.out | 4 +- tests/lean/StxQuot.lean.expected.out | 2 +- tests/lean/attrCmd.lean.expected.out | 2 +- .../autoBoundImplicits1.lean.expected.out | 20 +++++----- .../autoBoundImplicits2.lean.expected.out | 6 +-- tests/lean/autoPPExplicit.lean.expected.out | 2 +- ...utobound_and_macroscopes.lean.expected.out | 6 +-- tests/lean/auxDeclIssue.lean.expected.out | 6 +-- tests/lean/beginEndAsMacro.lean.expected.out | 2 +- tests/lean/classBadOutParam.lean.expected.out | 2 +- .../class_def_must_fail.lean.expected.out | 4 +- tests/lean/collectDepsIssue.lean.expected.out | 8 ++-- tests/lean/defaultInstance.lean.expected.out | 4 +- tests/lean/doErrorMsg.lean.expected.out | 10 ++--- tests/lean/doIssue.lean.expected.out | 6 +-- tests/lean/doNotation1.lean.expected.out | 28 ++++++------- tests/lean/doSeqRightIssue.lean.expected.out | 2 +- tests/lean/elseifDoErrorPos.lean.expected.out | 2 +- tests/lean/emptyc.lean.expected.out | 2 +- .../lean/envExtensionSealed.lean.expected.out | 2 +- tests/lean/evalWithMVar.lean.expected.out | 4 +- tests/lean/eval_except.lean.expected.out | 4 +- tests/lean/file_not_found.lean.expected.out | 6 +-- tests/lean/forErrors.lean.expected.out | 4 +- tests/lean/funExpected.lean.expected.out | 2 +- .../hidingInaccessibleNames.lean.expected.out | 16 ++++---- tests/lean/holeErrors.lean.expected.out | 28 ++++++------- tests/lean/holes.lean.expected.out | 20 +++++----- tests/lean/hygienicIntro.lean.expected.out | 4 +- tests/lean/inductionErrors.lean.expected.out | 40 +++++++++---------- tests/lean/inductive1.lean.expected.out | 36 ++++++++--------- tests/lean/invalidFieldName.lean.expected.out | 2 +- tests/lean/invalidNamedArgs.lean.expected.out | 4 +- tests/lean/letrec1.lean.expected.out | 8 ++-- tests/lean/letrecErrors.lean.expected.out | 6 +-- tests/lean/macroPrio.lean.expected.out | 2 +- tests/lean/macroStack.lean.expected.out | 8 ++-- tests/lean/match1.lean.expected.out | 6 +-- .../lean/matchErrorLocation.lean.expected.out | 2 +- tests/lean/matchErrorMsg.lean.expected.out | 2 +- tests/lean/moduleOf.lean.expected.out | 2 +- ...mutualWithNamespaceMacro.lean.expected.out | 2 +- tests/lean/mutualdef1.lean.expected.out | 6 +-- tests/lean/namedHoles.lean.expected.out | 6 +-- tests/lean/openExport.lean.expected.out | 4 +- tests/lean/parserPrio.lean.expected.out | 2 +- tests/lean/patvar.lean.expected.out | 8 ++-- .../phashmap_inst_coherence.lean.expected.out | 4 +- tests/lean/private.lean.expected.out | 6 +-- tests/lean/protected.lean.expected.out | 14 +++---- tests/lean/pureCoeIssue.lean.expected.out | 4 +- tests/lean/redundantAlt.lean.expected.out | 4 +- tests/lean/rewrite.lean.expected.out | 4 +- tests/lean/sanitychecks.lean.expected.out | 14 +++---- ...InstanceOutsideNamespace.lean.expected.out | 6 +-- tests/lean/scopedLocalInsts.lean.expected.out | 12 +++--- tests/lean/scopedMacros.lean.expected.out | 8 ++-- tests/lean/scopedTokens.lean.expected.out | 2 +- tests/lean/scopedunifhint.lean.expected.out | 10 ++--- tests/lean/shadow.lean.expected.out | 10 ++--- tests/lean/sorryWarning.lean.expected.out | 2 +- tests/lean/struct1.lean.expected.out | 28 ++++++------- tests/lean/structAutoBound.lean.expected.out | 4 +- tests/lean/structDefault.lean.expected.out | 2 +- tests/lean/structInstError.lean.expected.out | 2 +- tests/lean/substlet.lean.expected.out | 2 +- tests/lean/syntaxErrors.lean.expected.out | 4 +- tests/lean/test_single.sh | 2 +- tests/lean/theoremType.lean.expected.out | 4 +- tests/lean/typeIncorrectPat.lean.expected.out | 2 +- tests/lean/typeMismatch.lean.expected.out | 4 +- tests/lean/typeOf.lean.expected.out | 10 ++--- tests/lean/univInference.lean.expected.out | 10 ++--- tests/lean/unknownId.lean.expected.out | 6 +-- tests/lean/unsolvedIndCases.lean.expected.out | 18 ++++----- tests/lean/unused_univ.lean.expected.out | 6 +-- tests/lean/weirdmacro.lean.expected.out | 4 +- 77 files changed, 281 insertions(+), 281 deletions(-) diff --git a/tests/lean/217.lean.expected.out b/tests/lean/217.lean.expected.out index 7f6fb55aaa..1d06e22a0c 100644 --- a/tests/lean/217.lean.expected.out +++ b/tests/lean/217.lean.expected.out @@ -1,6 +1,6 @@ -217.lean:5:30: error: don't know how to synthesize placeholder +217.lean:5:30-5:31: error: don't know how to synthesize placeholder context: ⊢ CoreM Unit -217.lean:5:28: error: don't know how to synthesize placeholder +217.lean:5:28-5:29: error: don't know how to synthesize placeholder context: ⊢ CoreM Unit → Name → ConstantInfo → CoreM Unit diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index 4042ffe658..5fe29a5d03 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/tests/lean/StxQuot.lean.expected.out @@ -39,6 +39,6 @@ StxQuot.lean:77:33: error: expected parser to return exactly one syntax object "#[(numLit \"1\"), [(numLit \"2\") (numLit \"3\")], (numLit \"4\")]" "#[(numLit \"2\")]" -StxQuot.lean:90:39: error: unexpected antiquotation splice +StxQuot.lean:90:39-90:44: error: unexpected antiquotation splice fun (a : ?m) => sorryAx (?m a) : (a : ?m) → ?m a "#[(some 1), (some 2)]" diff --git a/tests/lean/attrCmd.lean.expected.out b/tests/lean/attrCmd.lean.expected.out index dac0ba2e61..5c402508af 100644 --- a/tests/lean/attrCmd.lean.expected.out +++ b/tests/lean/attrCmd.lean.expected.out @@ -1,2 +1,2 @@ -attrCmd.lean:6:0: error: failed to synthesize instance +attrCmd.lean:6:0-6:6: error: failed to synthesize instance Pure M diff --git a/tests/lean/autoBoundImplicits1.lean.expected.out b/tests/lean/autoBoundImplicits1.lean.expected.out index 903dca48f6..bc18225431 100644 --- a/tests/lean/autoBoundImplicits1.lean.expected.out +++ b/tests/lean/autoBoundImplicits1.lean.expected.out @@ -1,15 +1,15 @@ myid 10 : Nat myid true : Bool -autoBoundImplicits1.lean:17:18: warning: declaration uses 'sorry' -autoBoundImplicits1.lean:20:25: error: unknown identifier 'size' -autoBoundImplicits1.lean:21:18: warning: declaration uses 'sorry' -autoBoundImplicits1.lean:24:23: error: unknown identifier 'α' -autoBoundImplicits1.lean:24:25: error: unknown identifier 'n' -autoBoundImplicits1.lean:24:33: error: unknown identifier 'α' -autoBoundImplicits1.lean:24:37: error: unknown identifier 'β' -autoBoundImplicits1.lean:24:46: error: unknown identifier 'β' -autoBoundImplicits1.lean:24:48: error: unknown identifier 'n' -autoBoundImplicits1.lean:25:18: warning: declaration uses 'sorry' +autoBoundImplicits1.lean:17:18-17:23: warning: declaration uses 'sorry' +autoBoundImplicits1.lean:20:25-20:29: error: unknown identifier 'size' +autoBoundImplicits1.lean:21:18-21:23: warning: declaration uses 'sorry' +autoBoundImplicits1.lean:24:23-24:24: error: unknown identifier 'α' +autoBoundImplicits1.lean:24:25-24:26: error: unknown identifier 'n' +autoBoundImplicits1.lean:24:33-24:34: error: unknown identifier 'α' +autoBoundImplicits1.lean:24:37-24:38: error: unknown identifier 'β' +autoBoundImplicits1.lean:24:46-24:47: error: unknown identifier 'β' +autoBoundImplicits1.lean:24:48-24:49: error: unknown identifier 'n' +autoBoundImplicits1.lean:25:18-25:23: warning: declaration uses 'sorry' f : {α_1 : Type} → {n_1 : Nat} → Vec α_1 n_1 → Vec α_1 n_1 f mkVec : Vec ?m 0 f mkVec : Vec Nat 0 diff --git a/tests/lean/autoBoundImplicits2.lean.expected.out b/tests/lean/autoBoundImplicits2.lean.expected.out index 5ecc271fab..2f9e1651c5 100644 --- a/tests/lean/autoBoundImplicits2.lean.expected.out +++ b/tests/lean/autoBoundImplicits2.lean.expected.out @@ -1,6 +1,6 @@ -autoBoundImplicits2.lean:9:0: error: invalid auto implicit argument 'b', it depends on explicitly provided argument 'n' +autoBoundImplicits2.lean:9:0-10:3: error: invalid auto implicit argument 'b', it depends on explicitly provided argument 'n' g1 : ?m → ?m -autoBoundImplicits2.lean:30:17: error: unknown universe level 'u' -autoBoundImplicits2.lean:33:17: error: unknown universe level 'β' +autoBoundImplicits2.lean:30:17-30:18: error: unknown universe level 'u' +autoBoundImplicits2.lean:33:17-33:18: error: unknown universe level 'β' def h1.{u} : {m : Type u → Type u} → {α : Type u} → m α → m α := fun {m : Type u → Type u} {α : Type u} (a : m α) => a diff --git a/tests/lean/autoPPExplicit.lean.expected.out b/tests/lean/autoPPExplicit.lean.expected.out index fc903105ea..09baf206b3 100644 --- a/tests/lean/autoPPExplicit.lean.expected.out +++ b/tests/lean/autoPPExplicit.lean.expected.out @@ -1,4 +1,4 @@ -autoPPExplicit.lean:2:2: error: application type mismatch +autoPPExplicit.lean:2:2-2:32: error: application type mismatch @Eq.trans α a (b = c) argument b = c diff --git a/tests/lean/autobound_and_macroscopes.lean.expected.out b/tests/lean/autobound_and_macroscopes.lean.expected.out index 24b413633f..c93735aa23 100644 --- a/tests/lean/autobound_and_macroscopes.lean.expected.out +++ b/tests/lean/autobound_and_macroscopes.lean.expected.out @@ -1,3 +1,3 @@ -autobound_and_macroscopes.lean:2:15: error: unknown identifier 'x✝' -autobound_and_macroscopes.lean:2:19: error: unknown identifier 'x✝' -autobound_and_macroscopes.lean:2:24: warning: declaration uses 'sorry' +autobound_and_macroscopes.lean:2:15-2:16: error: unknown identifier 'x✝' +autobound_and_macroscopes.lean:2:19-2:20: error: unknown identifier 'x✝' +autobound_and_macroscopes.lean:2:24-2:29: warning: declaration uses 'sorry' diff --git a/tests/lean/auxDeclIssue.lean.expected.out b/tests/lean/auxDeclIssue.lean.expected.out index 53d9806032..ad2aa4266e 100644 --- a/tests/lean/auxDeclIssue.lean.expected.out +++ b/tests/lean/auxDeclIssue.lean.expected.out @@ -1,8 +1,8 @@ -auxDeclIssue.lean:5:3: error: tactic 'assumption' failed, +auxDeclIssue.lean:5:3-5:13: error: tactic 'assumption' failed, ⊢ False -auxDeclIssue.lean:11:2: error: tactic 'subst' failed, did not find equation for eliminating 'x' +auxDeclIssue.lean:11:2-11:9: error: tactic 'subst' failed, did not find equation for eliminating 'x' x y : Nat ⊢ x = y -auxDeclIssue.lean:18:3: error: tactic 'assumption' failed, +auxDeclIssue.lean:18:3-18:13: error: tactic 'assumption' failed, ex1 : False ⊢ False diff --git a/tests/lean/beginEndAsMacro.lean.expected.out b/tests/lean/beginEndAsMacro.lean.expected.out index e20fedda61..13da40fd0f 100644 --- a/tests/lean/beginEndAsMacro.lean.expected.out +++ b/tests/lean/beginEndAsMacro.lean.expected.out @@ -1,3 +1,3 @@ -beginEndAsMacro.lean:18:2: error: unsolved goals +beginEndAsMacro.lean:18:2-18:3: error: unsolved goals x : Nat ⊢ x + 0 = x diff --git a/tests/lean/classBadOutParam.lean.expected.out b/tests/lean/classBadOutParam.lean.expected.out index 57e52ad863..705f3cc892 100644 --- a/tests/lean/classBadOutParam.lean.expected.out +++ b/tests/lean/classBadOutParam.lean.expected.out @@ -1 +1 @@ -classBadOutParam.lean:3:1: error: invalid class, parameter #2 depends on `outParam`, but it is not an `outParam` +classBadOutParam.lean:3:1-3:4: error: invalid class, parameter #2 depends on `outParam`, but it is not an `outParam` diff --git a/tests/lean/class_def_must_fail.lean.expected.out b/tests/lean/class_def_must_fail.lean.expected.out index 80b1722e7c..f02a0fd55a 100644 --- a/tests/lean/class_def_must_fail.lean.expected.out +++ b/tests/lean/class_def_must_fail.lean.expected.out @@ -1,2 +1,2 @@ -class_def_must_fail.lean:3:13: error: invalid 'class', declaration 'Foo' must be inductive datatype or structure -class_def_must_fail.lean:8:18: error: invalid 'class', declaration 'Bla' must be inductive datatype or structure +class_def_must_fail.lean:3:13-3:16: error: invalid 'class', declaration 'Foo' must be inductive datatype or structure +class_def_must_fail.lean:8:18-8:21: error: invalid 'class', declaration 'Bla' must be inductive datatype or structure diff --git a/tests/lean/collectDepsIssue.lean.expected.out b/tests/lean/collectDepsIssue.lean.expected.out index e26cd8b5e5..de31b4bcc2 100644 --- a/tests/lean/collectDepsIssue.lean.expected.out +++ b/tests/lean/collectDepsIssue.lean.expected.out @@ -1,8 +1,8 @@ -collectDepsIssue.lean:5:0: error: don't know how to synthesize placeholder +collectDepsIssue.lean:5:0-5:1: error: don't know how to synthesize placeholder context: α : Type a : α ⊢ List α -collectDepsIssue.lean:9:13: warning: declaration uses 'sorry' -collectDepsIssue.lean:12:8: warning: declaration uses 'sorry' -collectDepsIssue.lean:13:8: warning: declaration uses 'sorry' +collectDepsIssue.lean:9:13-9:18: warning: declaration uses 'sorry' +collectDepsIssue.lean:12:8-12:13: warning: declaration uses 'sorry' +collectDepsIssue.lean:13:8-13:13: warning: declaration uses 'sorry' diff --git a/tests/lean/defaultInstance.lean.expected.out b/tests/lean/defaultInstance.lean.expected.out index 4d43968862..37663e4b2d 100644 --- a/tests/lean/defaultInstance.lean.expected.out +++ b/tests/lean/defaultInstance.lean.expected.out @@ -1,4 +1,4 @@ -defaultInstance.lean:20:20: error: failed to synthesize instance +defaultInstance.lean:20:20-20:23: error: failed to synthesize instance Foo Bool (?m x) -defaultInstance.lean:22:35: error: typeclass instance problem contains metavariables +defaultInstance.lean:22:35-22:38: error: typeclass instance problem contains metavariables Foo Bool (?m x) diff --git a/tests/lean/doErrorMsg.lean.expected.out b/tests/lean/doErrorMsg.lean.expected.out index e9b90f9bc1..afc58ebe5d 100644 --- a/tests/lean/doErrorMsg.lean.expected.out +++ b/tests/lean/doErrorMsg.lean.expected.out @@ -1,28 +1,28 @@ -doErrorMsg.lean:3:2: error: type mismatch +doErrorMsg.lean:3:2-3:13: error: type mismatch IO.getStdin has type EIO IO.Error IO.FS.Stream but is expected to have type EIO IO.Error PUnit -doErrorMsg.lean:15:19: error: type mismatch +doErrorMsg.lean:15:19-15:21: error: type mismatch f1 has type ExceptT String (StateT Nat Id) Nat but is expected to have type ExceptT String (StateT Nat Id) String -doErrorMsg.lean:19:19: error: type mismatch +doErrorMsg.lean:19:19-19:24: error: type mismatch f2 10 has type ExceptT String (StateT Nat Id) Nat but is expected to have type ExceptT String (StateT Nat Id) String -doErrorMsg.lean:24:2: error: type mismatch +doErrorMsg.lean:24:2-24:4: error: type mismatch f1 has type ExceptT String (StateT Nat Id) Nat but is expected to have type ExceptT String (StateT Nat Id) String -doErrorMsg.lean:23:10: error: type mismatch +doErrorMsg.lean:23:10-23:12: error: type mismatch f2 has type Nat → ExceptT String (StateT Nat Id) Nat diff --git a/tests/lean/doIssue.lean.expected.out b/tests/lean/doIssue.lean.expected.out index 6bf2091fdb..103237cf18 100644 --- a/tests/lean/doIssue.lean.expected.out +++ b/tests/lean/doIssue.lean.expected.out @@ -1,16 +1,16 @@ -doIssue.lean:2:2: error: type mismatch +doIssue.lean:2:2-2:3: error: type mismatch x has type Nat but is expected to have type EIO IO.Error PUnit -doIssue.lean:10:2: error: type mismatch +doIssue.lean:10:2-10:13: error: type mismatch Array.set! xs 0 1 has type Array Nat but is expected to have type EIO IO.Error PUnit -doIssue.lean:18:2: error: application type mismatch +doIssue.lean:18:2-18:20: error: application type mismatch pure (Array.set! xs 0 1) argument Array.set! xs 0 1 diff --git a/tests/lean/doNotation1.lean.expected.out b/tests/lean/doNotation1.lean.expected.out index 6cc895af87..1f3b715a16 100644 --- a/tests/lean/doNotation1.lean.expected.out +++ b/tests/lean/doNotation1.lean.expected.out @@ -1,36 +1,36 @@ -doNotation1.lean:4:0: error: 'y' cannot be reassigned -doNotation1.lean:8:2: error: 'y' cannot be reassigned -doNotation1.lean:12:2: error: 'p' cannot be reassigned -doNotation1.lean:20:7: error: invalid reassignment, value has type +doNotation1.lean:4:0-4:6: error: 'y' cannot be reassigned +doNotation1.lean:8:2-8:18: error: 'y' cannot be reassigned +doNotation1.lean:12:2-12:17: error: 'p' cannot be reassigned +doNotation1.lean:20:7-20:22: error: invalid reassignment, value has type Vector Nat (n + 1) but is expected to have type Vector Nat n -doNotation1.lean:25:7: error: invalid reassignment, value has type +doNotation1.lean:25:7-25:11: error: invalid reassignment, value has type Bool but is expected to have type Nat -doNotation1.lean:24:0: error: type mismatch, 'for' has type +doNotation1.lean:24:0-24:10: error: type mismatch, 'for' has type PUnit but is expected to have type List Bool -doNotation1.lean:28:0: error: type mismatch, 'for' has type +doNotation1.lean:28:0-28:10: error: type mismatch, 'for' has type PUnit but is expected to have type List Nat -doNotation1.lean:33:2: error: invalid 'do' element, it must be inside 'for' -doNotation1.lean:37:2: error: invalid 'do' element, it must be inside 'for' -doNotation1.lean:40:0: error: must be last element in a 'do' sequence +doNotation1.lean:33:2-33:7: error: invalid 'do' element, it must be inside 'for' +doNotation1.lean:37:2-37:10: error: invalid 'do' element, it must be inside 'for' +doNotation1.lean:40:0-40:9: error: must be last element in a 'do' sequence def f10 : Nat → IO Unit := fun (x : Nat) => IO.println x -doNotation1.lean:51:0: error: type mismatch +doNotation1.lean:51:0-51:13: error: type mismatch IO.mkRef true has type EIO IO.Error (IO.Ref Bool) but is expected to have type EIO IO.Error Unit -doNotation1.lean:58:2: error: type mismatch, result value has type +doNotation1.lean:58:2-58:3: error: type mismatch, result value has type Unit but is expected to have type Bool -doNotation1.lean:66:0: error: 'do' element is unreachable -doNotation1.lean:70:0: error: 'do' element is unreachable +doNotation1.lean:66:0-66:18: error: 'do' element is unreachable +doNotation1.lean:70:0-70:32: error: 'do' element is unreachable diff --git a/tests/lean/doSeqRightIssue.lean.expected.out b/tests/lean/doSeqRightIssue.lean.expected.out index ba009398da..30afc2f7f3 100644 --- a/tests/lean/doSeqRightIssue.lean.expected.out +++ b/tests/lean/doSeqRightIssue.lean.expected.out @@ -1 +1 @@ -doSeqRightIssue.lean:5:24: error: unknown universe level 'v' +doSeqRightIssue.lean:5:24-5:25: error: unknown universe level 'v' diff --git a/tests/lean/elseifDoErrorPos.lean.expected.out b/tests/lean/elseifDoErrorPos.lean.expected.out index a270a9d643..a455a0a6e2 100644 --- a/tests/lean/elseifDoErrorPos.lean.expected.out +++ b/tests/lean/elseifDoErrorPos.lean.expected.out @@ -1,4 +1,4 @@ -elseifDoErrorPos.lean:4:7: error: application type mismatch +elseifDoErrorPos.lean:4:7-7:14: error: application type mismatch ite x argument x diff --git a/tests/lean/emptyc.lean.expected.out b/tests/lean/emptyc.lean.expected.out index fc228f7c89..6a5904246f 100644 --- a/tests/lean/emptyc.lean.expected.out +++ b/tests/lean/emptyc.lean.expected.out @@ -1,4 +1,4 @@ -emptyc.lean:19:0: error: ambiguous, possible interpretations +emptyc.lean:19:0-19:2: error: ambiguous, possible interpretations { x := 0 } EmptyCollection.emptyCollection diff --git a/tests/lean/envExtensionSealed.lean.expected.out b/tests/lean/envExtensionSealed.lean.expected.out index d6f283d6da..aabfad37f3 100644 --- a/tests/lean/envExtensionSealed.lean.expected.out +++ b/tests/lean/envExtensionSealed.lean.expected.out @@ -1,3 +1,3 @@ 1 -envExtensionSealed.lean:14:7: error: invalid {...} notation, source type is not of the form (C ...) +envExtensionSealed.lean:14:7-14:35: error: invalid {...} notation, source type is not of the form (C ...) EnvExtensionInterfaceImp.1 Nat diff --git a/tests/lean/evalWithMVar.lean.expected.out b/tests/lean/evalWithMVar.lean.expected.out index 3c0639418e..388f412569 100644 --- a/tests/lean/evalWithMVar.lean.expected.out +++ b/tests/lean/evalWithMVar.lean.expected.out @@ -1,9 +1,9 @@ Sum.someRight c : Option Nat -evalWithMVar.lean:13:6: error: don't know how to synthesize implicit argument +evalWithMVar.lean:13:6-13:21: error: don't know how to synthesize implicit argument @Sum.someRight ?m Nat c context: ⊢ Type ?u -evalWithMVar.lean:13:20: error: don't know how to synthesize implicit argument +evalWithMVar.lean:13:20-13:21: error: don't know how to synthesize implicit argument @c ?m context: ⊢ Type ?u diff --git a/tests/lean/eval_except.lean.expected.out b/tests/lean/eval_except.lean.expected.out index 4d8c822d0f..69f0a21a69 100644 --- a/tests/lean/eval_except.lean.expected.out +++ b/tests/lean/eval_except.lean.expected.out @@ -1,5 +1,5 @@ -eval_except.lean:4:0: error: this is my error +eval_except.lean:4:0-4:57: error: this is my error -eval_except.lean:5:0: error: no such file or directory (error code: 31) +eval_except.lean:5:0-5:80: error: no such file or directory (error code: 31) file: file.ext diff --git a/tests/lean/file_not_found.lean.expected.out b/tests/lean/file_not_found.lean.expected.out index 8bc0565c75..d93b7eb447 100644 --- a/tests/lean/file_not_found.lean.expected.out +++ b/tests/lean/file_not_found.lean.expected.out @@ -1,9 +1,9 @@ -file_not_found.lean:6:0: error: no such file or directory (error code: 2) +file_not_found.lean:6:0-6:77: error: no such file or directory (error code: 2) file: non-existent-file.txt -file_not_found.lean:13:0: error: permission denied (error code: 13) +file_not_found.lean:13:0-13:69: error: permission denied (error code: 13) file: readonly.txt -file_not_found.lean:14:0: error: invalid argument (error code: 9, bad file descriptor) +file_not_found.lean:14:0-18:9: error: invalid argument (error code: 9, bad file descriptor) diff --git a/tests/lean/forErrors.lean.expected.out b/tests/lean/forErrors.lean.expected.out index d815b27add..898ea84d83 100644 --- a/tests/lean/forErrors.lean.expected.out +++ b/tests/lean/forErrors.lean.expected.out @@ -1,4 +1,4 @@ -forErrors.lean:3:29: error: failed to synthesize instance +forErrors.lean:3:29-3:30: error: failed to synthesize instance ToStream α ?m -forErrors.lean:5:15: error: failed to synthesize instance +forErrors.lean:5:15-5:39: error: failed to synthesize instance ToString α diff --git a/tests/lean/funExpected.lean.expected.out b/tests/lean/funExpected.lean.expected.out index 4cd7f3d966..e2cddfdc89 100644 --- a/tests/lean/funExpected.lean.expected.out +++ b/tests/lean/funExpected.lean.expected.out @@ -1,4 +1,4 @@ -funExpected.lean:4:2: error: function expected at +funExpected.lean:4:2-4:29: error: function expected at List.map (fun (x : Nat) => x + 1) xs term has type List ?m diff --git a/tests/lean/hidingInaccessibleNames.lean.expected.out b/tests/lean/hidingInaccessibleNames.lean.expected.out index b272d3f4e5..263d3b8e50 100644 --- a/tests/lean/hidingInaccessibleNames.lean.expected.out +++ b/tests/lean/hidingInaccessibleNames.lean.expected.out @@ -1,16 +1,16 @@ -hidingInaccessibleNames.lean:4:15: error: don't know how to synthesize placeholder +hidingInaccessibleNames.lean:4:15-4:16: error: don't know how to synthesize placeholder context: ⊢ Nat -hidingInaccessibleNames.lean:3:19: error: don't know how to synthesize placeholder +hidingInaccessibleNames.lean:3:19-3:20: error: don't know how to synthesize placeholder context: a b : Nat : [a, b] ≠ [] ⊢ Nat -hidingInaccessibleNames.lean:2:16: error: don't know how to synthesize placeholder +hidingInaccessibleNames.lean:2:16-2:17: error: don't know how to synthesize placeholder context: : [] ≠ [] ⊢ Nat -hidingInaccessibleNames.lean:10:16: error: don't know how to synthesize placeholder +hidingInaccessibleNames.lean:10:16-10:17: error: don't know how to synthesize placeholder context: x✝⁵ : List Nat x✝⁴ : Nat @@ -19,7 +19,7 @@ x✝² : List Nat x✝¹ : Nat x✝ : x✝² ≠ [] ⊢ Nat -hidingInaccessibleNames.lean:9:19: error: don't know how to synthesize placeholder +hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder context: x✝⁴ : List Nat x✝³ : Nat @@ -27,7 +27,7 @@ x✝² : x✝⁴ ≠ [] a b x✝¹ : Nat x✝ : [a, b] ≠ [] ⊢ Nat -hidingInaccessibleNames.lean:8:16: error: don't know how to synthesize placeholder +hidingInaccessibleNames.lean:8:16-8:17: error: don't know how to synthesize placeholder context: x✝⁴ : List Nat x✝³ : Nat @@ -44,13 +44,13 @@ case inr p q : Prop : q ⊢ q ∨ p -hidingInaccessibleNames.lean:23:25: error: don't know how to synthesize placeholder +hidingInaccessibleNames.lean:23:25-23:26: error: don't know how to synthesize placeholder context: x✝² : Prop x✝¹ : x✝² : x✝² ⊢ decide x✝² = true -hidingInaccessibleNames.lean:27:17: error: don't know how to synthesize placeholder +hidingInaccessibleNames.lean:27:17-27:18: error: don't know how to synthesize placeholder context: x✝ : Char ⊢ x✝.val = x✝.val diff --git a/tests/lean/holeErrors.lean.expected.out b/tests/lean/holeErrors.lean.expected.out index b12183de22..a408f2bbdf 100644 --- a/tests/lean/holeErrors.lean.expected.out +++ b/tests/lean/holeErrors.lean.expected.out @@ -1,24 +1,24 @@ -holeErrors.lean:3:10: error: don't know how to synthesize implicit argument +holeErrors.lean:3:10-3:12: error: don't know how to synthesize implicit argument @id ?m context: ⊢ Sort u_1 -holeErrors.lean:3:7: error: failed to infer definition type -holeErrors.lean:5:9: error: failed to infer definition type -holeErrors.lean:8:9: error: don't know how to synthesize implicit argument +holeErrors.lean:3:7-3:12: error: failed to infer definition type +holeErrors.lean:5:9-5:10: error: failed to infer definition type +holeErrors.lean:8:9-8:11: error: don't know how to synthesize implicit argument @id ?m context: ⊢ Sort u_1 -holeErrors.lean:8:4: error: failed to infer 'let' declaration type -holeErrors.lean:7:7: error: failed to infer definition type -holeErrors.lean:11:11: error: failed to infer definition type -holeErrors.lean:11:7: error: failed to infer binder type -holeErrors.lean:13:15: error: failed to infer definition type -holeErrors.lean:13:12: error: failed to infer binder type -holeErrors.lean:16:4: error: failed to infer binder type -holeErrors.lean:15:7: error: failed to infer definition type -holeErrors.lean:19:13: error: don't know how to synthesize implicit argument +holeErrors.lean:8:4-8:5: error: failed to infer 'let' declaration type +holeErrors.lean:7:7-9:1: error: failed to infer definition type +holeErrors.lean:11:11-11:15: error: failed to infer definition type +holeErrors.lean:11:7-11:8: error: failed to infer binder type +holeErrors.lean:13:15-13:19: error: failed to infer definition type +holeErrors.lean:13:12-13:13: error: failed to infer binder type +holeErrors.lean:16:4-16:5: error: failed to infer binder type +holeErrors.lean:15:7-16:10: error: failed to infer definition type +holeErrors.lean:19:13-19:15: error: don't know how to synthesize implicit argument @id ?m context: x : ?m → ?m ⊢ Sort u_1 -holeErrors.lean:19:8: error: failed to infer 'let rec' declaration type +holeErrors.lean:19:8-19:9: error: failed to infer 'let rec' declaration type diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out index fc9c41304a..2817656f87 100644 --- a/tests/lean/holes.lean.expected.out +++ b/tests/lean/holes.lean.expected.out @@ -1,27 +1,27 @@ -holes.lean:4:4: error: placeholders '_' cannot be used where a function is expected -holes.lean:11:8: error: don't know how to synthesize placeholder +holes.lean:4:4-4:7: error: placeholders '_' cannot be used where a function is expected +holes.lean:11:8-11:13: error: don't know how to synthesize placeholder context: case hole x : Nat y : Nat := g x + g x ⊢ Nat -holes.lean:11:4: error: don't know how to synthesize placeholder +holes.lean:11:4-11:5: error: don't know how to synthesize placeholder context: x : Nat y : Nat := g x + g x ⊢ Nat -holes.lean:10:15: error: don't know how to synthesize implicit argument +holes.lean:10:15-10:18: error: don't know how to synthesize implicit argument @g Nat (?m x) x context: x : Nat ⊢ Type -holes.lean:10:9: error: don't know how to synthesize implicit argument +holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument @g Nat (?m x) x context: x : Nat ⊢ Type -holes.lean:13:7: error: failed to infer binder type -holes.lean:15:16: error: failed to infer binder type -holes.lean:18:6: error: failed to infer binder type -holes.lean:21:25: error: failed to infer definition type -holes.lean:25:8: error: failed to infer 'let rec' declaration type +holes.lean:13:7-13:8: error: failed to infer binder type +holes.lean:15:16-15:17: error: failed to infer binder type +holes.lean:18:6-18:7: error: failed to infer binder type +holes.lean:21:25-22:4: error: failed to infer definition type +holes.lean:25:8-25:9: error: failed to infer 'let rec' declaration type diff --git a/tests/lean/hygienicIntro.lean.expected.out b/tests/lean/hygienicIntro.lean.expected.out index 44214b0a9c..cccaad22c6 100644 --- a/tests/lean/hygienicIntro.lean.expected.out +++ b/tests/lean/hygienicIntro.lean.expected.out @@ -1,2 +1,2 @@ -hygienicIntro.lean:14:6: error: unknown identifier 'a_1' -hygienicIntro.lean:24:18: error: unknown identifier 'h' +hygienicIntro.lean:14:6-14:9: error: unknown identifier 'a_1' +hygienicIntro.lean:24:18-24:19: error: unknown identifier 'h' diff --git a/tests/lean/inductionErrors.lean.expected.out b/tests/lean/inductionErrors.lean.expected.out index 3239305422..3014af9364 100644 --- a/tests/lean/inductionErrors.lean.expected.out +++ b/tests/lean/inductionErrors.lean.expected.out @@ -1,36 +1,36 @@ -inductionErrors.lean:12:12: error: unsolved goals +inductionErrors.lean:12:12-12:14: error: unsolved goals case upper q d : Nat ⊢ q + Nat.succ d > q -inductionErrors.lean:11:12: error: unsolved goals +inductionErrors.lean:11:12-11:14: error: unsolved goals case lower p d : Nat ⊢ p ≤ p + Nat.succ d -inductionErrors.lean:16:19: error: unknown constant 'elimEx2' -inductionErrors.lean:22:8: error: insufficient number of targets for 'elimEx' -inductionErrors.lean:28:16: error: unexpected eliminator resulting type +inductionErrors.lean:16:19-16:26: error: unknown constant 'elimEx2' +inductionErrors.lean:22:8-22:9: error: insufficient number of targets for 'elimEx' +inductionErrors.lean:28:16-28:23: error: unexpected eliminator resulting type Nat -inductionErrors.lean:35:11: error: unsolved goals +inductionErrors.lean:35:11-35:15: error: unsolved goals x : Nat ⊢ 0 + 0 = 0 -inductionErrors.lean:36:11: error: unsolved goals +inductionErrors.lean:36:11-36:15: error: unsolved goals x y : Nat ⊢ 0 + (y + 1) = y + 1 -inductionErrors.lean:40:14: error: unsolved goals +inductionErrors.lean:40:14-40:18: error: unsolved goals case zero ⊢ 0 + Nat.zero = Nat.zero -inductionErrors.lean:41:14: error: unsolved goals +inductionErrors.lean:41:14-41:18: error: unsolved goals case succ y : Nat ⊢ 0 + Nat.succ y = Nat.succ y -inductionErrors.lean:50:2: error: alternative 'cons' is not needed -inductionErrors.lean:53:2: error: alternative for 'Vec.cons' is not needed -inductionErrors.lean:60:2: error: invalid alternative name 'upper2' -inductionErrors.lean:66:23: warning: declaration uses 'sorry' -inductionErrors.lean:65:29: warning: declaration uses 'sorry' -inductionErrors.lean:72:29: warning: declaration uses 'sorry' -inductionErrors.lean:71:29: warning: declaration uses 'sorry' -inductionErrors.lean:74:2: error: unused alternative -inductionErrors.lean:79:29: warning: declaration uses 'sorry' -inductionErrors.lean:78:29: warning: declaration uses 'sorry' -inductionErrors.lean:80:2: error: unused alternative +inductionErrors.lean:50:2-50:16: error: alternative 'cons' is not needed +inductionErrors.lean:53:2-55:16: error: alternative for 'Vec.cons' is not needed +inductionErrors.lean:60:2-60:40: error: invalid alternative name 'upper2' +inductionErrors.lean:66:23-66:28: warning: declaration uses 'sorry' +inductionErrors.lean:65:29-65:34: warning: declaration uses 'sorry' +inductionErrors.lean:72:29-72:34: warning: declaration uses 'sorry' +inductionErrors.lean:71:29-71:34: warning: declaration uses 'sorry' +inductionErrors.lean:74:2-74:34: error: unused alternative +inductionErrors.lean:79:29-79:34: warning: declaration uses 'sorry' +inductionErrors.lean:78:29-78:34: warning: declaration uses 'sorry' +inductionErrors.lean:80:2-80:53: error: unused alternative diff --git a/tests/lean/inductive1.lean.expected.out b/tests/lean/inductive1.lean.expected.out index 0f10e692f6..0cbe42f570 100644 --- a/tests/lean/inductive1.lean.expected.out +++ b/tests/lean/inductive1.lean.expected.out @@ -1,29 +1,29 @@ -inductive1.lean:4:15: error: invalid inductive type, resultant type is not a sort -inductive1.lean:12:0: error: invalid mutually inductive types, resulting universe mismatch, given +inductive1.lean:4:15-4:18: error: invalid inductive type, resultant type is not a sort +inductive1.lean:12:0-12:19: error: invalid mutually inductive types, resulting universe mismatch, given Type expected type Prop -inductive1.lean:22:0: error: invalid mutually inductive types, resulting universe mismatch, given +inductive1.lean:22:0-22:37: error: invalid mutually inductive types, resulting universe mismatch, given Type v expected type Type u -inductive1.lean:31:0: error: invalid mutually inductive types, parameter 'x' has type +inductive1.lean:31:0-31:41: error: invalid mutually inductive types, parameter 'x' has type Bool but is expected to have type Nat -inductive1.lean:40:0: error: invalid inductive type, number of parameters mismatch in mutually inductive datatypes -inductive1.lean:49:0: error: invalid mutually inductive types, binder annotation mismatch at parameter 'x' -inductive1.lean:59:0: error: invalid inductive type, universe parameters mismatch in mutually inductive datatypes -inductive1.lean:69:2: error: 'Boo.T1.bla' has already been declared -inductive1.lean:73:10: error: 'Boo.T1' has already been declared -inductive1.lean:80:0: error: invalid use of 'partial' in inductive declaration -inductive1.lean:81:0: error: invalid use of 'noncomputable' in inductive declaration -inductive1.lean:82:0: error: invalid use of attributes in inductive declaration -inductive1.lean:85:0: error: invalid 'private' constructor in a 'private' inductive datatype -inductive1.lean:93:7: error: invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes -inductive1.lean:100:0: error: constructor resulting type must be specified in inductive family declaration -inductive1.lean:105:0: error: unexpected constructor resulting type, type expected +inductive1.lean:40:0-40:30: error: invalid inductive type, number of parameters mismatch in mutually inductive datatypes +inductive1.lean:49:0-49:40: error: invalid mutually inductive types, binder annotation mismatch at parameter 'x' +inductive1.lean:59:0-59:45: error: invalid inductive type, universe parameters mismatch in mutually inductive datatypes +inductive1.lean:69:2-69:5: error: 'Boo.T1.bla' has already been declared +inductive1.lean:73:10-73:12: error: 'Boo.T1' has already been declared +inductive1.lean:80:0-80:27: error: invalid use of 'partial' in inductive declaration +inductive1.lean:81:0-81:33: error: invalid use of 'noncomputable' in inductive declaration +inductive1.lean:82:0-82:29: error: invalid use of attributes in inductive declaration +inductive1.lean:85:0-85:17: error: invalid 'private' constructor in a 'private' inductive datatype +inductive1.lean:93:7-93:26: error: invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes +inductive1.lean:100:0-100:4: error: constructor resulting type must be specified in inductive family declaration +inductive1.lean:105:0-105:9: error: unexpected constructor resulting type, type expected T1 -inductive1.lean:108:0: error: unexpected constructor resulting type +inductive1.lean:108:0-108:10: error: unexpected constructor resulting type Nat -inductive1.lean:118:7: error: unknown identifier 'cons' +inductive1.lean:118:7-118:11: error: unknown identifier 'cons' diff --git a/tests/lean/invalidFieldName.lean.expected.out b/tests/lean/invalidFieldName.lean.expected.out index 9120ff47cf..482f01ab51 100644 --- a/tests/lean/invalidFieldName.lean.expected.out +++ b/tests/lean/invalidFieldName.lean.expected.out @@ -1 +1 @@ -invalidFieldName.lean:3:2: error: invalid field name 'mk', it is equal to structure constructor name +invalidFieldName.lean:3:2-3:4: error: invalid field name 'mk', it is equal to structure constructor name diff --git a/tests/lean/invalidNamedArgs.lean.expected.out b/tests/lean/invalidNamedArgs.lean.expected.out index 88acbb7a8f..5ba7ba6e2e 100644 --- a/tests/lean/invalidNamedArgs.lean.expected.out +++ b/tests/lean/invalidNamedArgs.lean.expected.out @@ -1,2 +1,2 @@ -invalidNamedArgs.lean:4:9: error: invalid argument name 'b' for function 'List.foldl' -invalidNamedArgs.lean:10:4: error: invalid argument name 'flg' for function 'f' +invalidNamedArgs.lean:4:9-4:17: error: invalid argument name 'b' for function 'List.foldl' +invalidNamedArgs.lean:10:4-10:18: error: invalid argument name 'flg' for function 'f' diff --git a/tests/lean/letrec1.lean.expected.out b/tests/lean/letrec1.lean.expected.out index 096b5f6bde..a3d52fc82a 100644 --- a/tests/lean/letrec1.lean.expected.out +++ b/tests/lean/letrec1.lean.expected.out @@ -1,4 +1,4 @@ -letrec1.lean:6:0: error: 'f1.g' has already been declared -letrec1.lean:18:35: error: unknown identifier 'g' -letrec1.lean:27:8: error: invalid type in 'let rec', it uses 'f' which is being defined simultaneously -letrec1.lean:37:10: error: invalid type in 'let rec', it uses 'g' which is being defined simultaneously +letrec1.lean:6:0-9:7: error: 'f1.g' has already been declared +letrec1.lean:18:35-18:36: error: unknown identifier 'g' +letrec1.lean:27:8-28:9: error: invalid type in 'let rec', it uses 'f' which is being defined simultaneously +letrec1.lean:37:10-37:50: error: invalid type in 'let rec', it uses 'g' which is being defined simultaneously diff --git a/tests/lean/letrecErrors.lean.expected.out b/tests/lean/letrecErrors.lean.expected.out index 632b28f855..5089e28dcb 100644 --- a/tests/lean/letrecErrors.lean.expected.out +++ b/tests/lean/letrecErrors.lean.expected.out @@ -1,3 +1,3 @@ -letrecErrors.lean:2:10: error: 'f1.g' has already been declared -letrecErrors.lean:11:12: error: 'f2.h' has already been declared -letrecErrors.lean:18:2: error: 'f3.h' has already been declared +letrecErrors.lean:2:10-2:30: error: 'f1.g' has already been declared +letrecErrors.lean:11:12-11:32: error: 'f2.h' has already been declared +letrecErrors.lean:18:2-19:5: error: 'f3.h' has already been declared diff --git a/tests/lean/macroPrio.lean.expected.out b/tests/lean/macroPrio.lean.expected.out index c9f94c8a4c..3df230ae6d 100644 --- a/tests/lean/macroPrio.lean.expected.out +++ b/tests/lean/macroPrio.lean.expected.out @@ -1,5 +1,5 @@ 0 + 1 : Nat -macroPrio.lean:12:7: error: ambiguous, possible interpretations +macroPrio.lean:12:7-12:13: error: ambiguous, possible interpretations 1 * 2 1 + 1 diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out index 3753785189..312e927dfb 100644 --- a/tests/lean/macroStack.lean.expected.out +++ b/tests/lean/macroStack.lean.expected.out @@ -1,13 +1,13 @@ -macroStack.lean:4:5: error: unknown identifier 'x' -macroStack.lean:8:6: error: unknown identifier 'x' +macroStack.lean:4:5-4:6: error: unknown identifier 'x' +macroStack.lean:8:6-8:7: error: unknown identifier 'x' with resulting expansion binrel! Greater✝ x 0 while expanding x > 0 while expanding if h : (x > 0) then 1 else 0 -macroStack.lean:11:9: error: invalid use of `(<- ...)`, must be nested inside a 'do' expression -macroStack.lean:17:0: error: failed to synthesize instance +macroStack.lean:11:9-11:15: error: invalid use of `(<- ...)`, must be nested inside a 'do' expression +macroStack.lean:17:0-17:1: error: failed to synthesize instance HAdd Nat String ?m with resulting expansion HAdd.hAdd✝ (x + x✝) x✝¹ diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out index 4617fcb36e..8a10e06e52 100644 --- a/tests/lean/match1.lean.expected.out +++ b/tests/lean/match1.lean.expected.out @@ -10,16 +10,16 @@ 4 ---- inv 10 -match1.lean:82:0: error: type mismatch during dependent match-elimination at pattern variable 'w' with type +match1.lean:82:0-82:73: error: type mismatch during dependent match-elimination at pattern variable 'w' with type VecPred P Vec.nil expected type VecPred P tail✝ [false, true, true] -match1.lean:113:0: error: dependent match elimination failed, inaccessible pattern found +match1.lean:113:0-113:41: error: dependent match elimination failed, inaccessible pattern found .(j + j) constructor expected [false, true, true] -match1.lean:124:7: error: invalid match-expression, type of pattern variable 'a' contains metavariables +match1.lean:124:7-124:22: error: invalid match-expression, type of pattern variable 'a' contains metavariables ?m fun (x : ?m × ?m) => ?m x : ?m × ?m → ?m fun (x : Nat × Nat) => diff --git a/tests/lean/matchErrorLocation.lean.expected.out b/tests/lean/matchErrorLocation.lean.expected.out index 10ccd5b0f0..0678383aec 100644 --- a/tests/lean/matchErrorLocation.lean.expected.out +++ b/tests/lean/matchErrorLocation.lean.expected.out @@ -1,4 +1,4 @@ -matchErrorLocation.lean:5:10: error: type mismatch +matchErrorLocation.lean:5:10-5:14: error: type mismatch h he has type False diff --git a/tests/lean/matchErrorMsg.lean.expected.out b/tests/lean/matchErrorMsg.lean.expected.out index 2c361560d7..c648dae646 100644 --- a/tests/lean/matchErrorMsg.lean.expected.out +++ b/tests/lean/matchErrorMsg.lean.expected.out @@ -1,2 +1,2 @@ -matchErrorMsg.lean:2:1: error: missing cases: +matchErrorMsg.lean:2:1-2:6: error: missing cases: (Prod.mk Nat.zero (Nat.succ _)) diff --git a/tests/lean/moduleOf.lean.expected.out b/tests/lean/moduleOf.lean.expected.out index 8e19ad6e86..ec3944557d 100644 --- a/tests/lean/moduleOf.lean.expected.out +++ b/tests/lean/moduleOf.lean.expected.out @@ -4,4 +4,4 @@ (some Std.Data.HashMap) none none -moduleOf.lean:16:0: error: unknown constant 'foo' +moduleOf.lean:16:0-16:9: error: unknown constant 'foo' diff --git a/tests/lean/mutualWithNamespaceMacro.lean.expected.out b/tests/lean/mutualWithNamespaceMacro.lean.expected.out index ddf73cbb83..e8e3f99790 100644 --- a/tests/lean/mutualWithNamespaceMacro.lean.expected.out +++ b/tests/lean/mutualWithNamespaceMacro.lean.expected.out @@ -1 +1 @@ -mutualWithNamespaceMacro.lean:9:0: error: conflicting namespaces in mutual declaration, using namespace 'Boo', but used 'Foo' in previous declaration +mutualWithNamespaceMacro.lean:9:0-11:23: error: conflicting namespaces in mutual declaration, using namespace 'Boo', but used 'Foo' in previous declaration diff --git a/tests/lean/mutualdef1.lean.expected.out b/tests/lean/mutualdef1.lean.expected.out index 90919b90bd..5c3a088c17 100644 --- a/tests/lean/mutualdef1.lean.expected.out +++ b/tests/lean/mutualdef1.lean.expected.out @@ -1,3 +1,3 @@ -mutualdef1.lean:9:0: error: invalid mutually recursive definitions, cannot mix theorems and definitions -mutualdef1.lean:21:0: error: invalid mutually recursive definitions, cannot mix examples and definitions -mutualdef1.lean:32:7: error: invalid mutually recursive definitions, cannot mix unsafe and safe definitions +mutualdef1.lean:9:0-11:12: error: invalid mutually recursive definitions, cannot mix theorems and definitions +mutualdef1.lean:21:0-22:4: error: invalid mutually recursive definitions, cannot mix examples and definitions +mutualdef1.lean:32:7-34:12: error: invalid mutually recursive definitions, cannot mix unsafe and safe definitions diff --git a/tests/lean/namedHoles.lean.expected.out b/tests/lean/namedHoles.lean.expected.out index 65e5c65351..ba502a68fb 100644 --- a/tests/lean/namedHoles.lean.expected.out +++ b/tests/lean/namedHoles.lean.expected.out @@ -1,4 +1,4 @@ -namedHoles.lean:9:7: error: application type mismatch +namedHoles.lean:9:7-9:14: error: application type mismatch f ?m ?m argument ?m @@ -10,9 +10,9 @@ g ?m ?m : Nat 20 foo (fun (x : Nat) => ?m x) ?m : Nat bla ?m fun (x : Nat) => ?m : Nat -namedHoles.lean:35:38: error: synthetic hole has already been defined with an incompatible local context +namedHoles.lean:35:38-35:43: error: synthetic hole has already been defined with an incompatible local context boo (fun (x : Nat) => ?m x) fun (y : Bool) => sorryAx Nat : Nat 11 12 -namedHoles.lean:58:26: error: synthetic hole has already been defined and assigned to value incompatible with the current context +namedHoles.lean:58:26-58:31: error: synthetic hole has already been defined and assigned to value incompatible with the current context y diff --git a/tests/lean/openExport.lean.expected.out b/tests/lean/openExport.lean.expected.out index 1e46572ebf..3bdff125ad 100644 --- a/tests/lean/openExport.lean.expected.out +++ b/tests/lean/openExport.lean.expected.out @@ -3,8 +3,8 @@ y : Nat B.x : Nat B.x : Nat B.y : Nat -openExport.lean:19:7: error: unknown identifier 'x' -openExport.lean:20:7: error: unknown identifier 'y' +openExport.lean:19:7-19:8: error: unknown identifier 'x' +openExport.lean:20:7-20:8: error: unknown identifier 'y' x : Nat y : Nat x : Nat diff --git a/tests/lean/parserPrio.lean.expected.out b/tests/lean/parserPrio.lean.expected.out index 7ca3941303..de146f7139 100644 --- a/tests/lean/parserPrio.lean.expected.out +++ b/tests/lean/parserPrio.lean.expected.out @@ -1,6 +1,6 @@ [1, 2] 6 -parserPrio.lean:26:7: error: ambiguous, possible interpretations +parserPrio.lean:26:7-26:10: error: ambiguous, possible interpretations 2 * 1 [1] diff --git a/tests/lean/patvar.lean.expected.out b/tests/lean/patvar.lean.expected.out index 4e19d59da4..488d1ab515 100644 --- a/tests/lean/patvar.lean.expected.out +++ b/tests/lean/patvar.lean.expected.out @@ -1,6 +1,6 @@ -patvar.lean:3:0: error: missing cases: +patvar.lean:3:0-3:5: error: missing cases: (List.cons _ _) -patvar.lean:10:0: error: missing cases: +patvar.lean:10:0-10:5: error: missing cases: (List.cons _ _) -patvar.lean:14:0: error: invalid pattern variable, must be atomic -patvar.lean:17:0: error: invalid pattern variable, must be atomic +patvar.lean:14:0-14:21: error: invalid pattern variable, must be atomic +patvar.lean:17:0-17:20: error: invalid pattern variable, must be atomic diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out index 44d85b30ce..c2af02ecc4 100644 --- a/tests/lean/phashmap_inst_coherence.lean.expected.out +++ b/tests/lean/phashmap_inst_coherence.lean.expected.out @@ -1,4 +1,4 @@ -phashmap_inst_coherence.lean:12:6: error: application type mismatch +phashmap_inst_coherence.lean:12:6-12:56: error: application type mismatch PersistentHashMap.find? m argument m @@ -6,5 +6,5 @@ has type @PersistentHashMap Nat Nat instBEq instHashableNat but is expected to have type @PersistentHashMap Nat Nat instBEq natDiffHash -phashmap_inst_coherence.lean:12:0: error: failed to synthesize +phashmap_inst_coherence.lean:12:0-12:56: error: failed to synthesize Lean.Eval ?m diff --git a/tests/lean/private.lean.expected.out b/tests/lean/private.lean.expected.out index 5a3ed01c76..d64383117f 100644 --- a/tests/lean/private.lean.expected.out +++ b/tests/lean/private.lean.expected.out @@ -1,5 +1,5 @@ Bla.foo == "world" : Bool -private.lean:14:12: error: private declaration 'Bla.foo' has already been declared +private.lean:14:12-14:15: error: private declaration 'Bla.foo' has already been declared foo == 0 : Bool Bla.foo : String Boo.Bla.boo == "world" : Bool @@ -9,5 +9,5 @@ boo == 100 : Bool Boo.Bla.boo == "world" : Bool Boo.boo == 100 : Bool Nat.mul10 x : Nat -private.lean:65:12: error: a non-private declaration 'y' has already been declared -private.lean:68:4: error: a private declaration 'z' has already been declared +private.lean:65:12-65:13: error: a non-private declaration 'y' has already been declared +private.lean:68:4-68:5: error: a private declaration 'z' has already been declared diff --git a/tests/lean/protected.lean.expected.out b/tests/lean/protected.lean.expected.out index e375d3af7c..7f83465c9a 100644 --- a/tests/lean/protected.lean.expected.out +++ b/tests/lean/protected.lean.expected.out @@ -1,13 +1,13 @@ -protected.lean:10:7: error: unknown identifier 'x' +protected.lean:10:7-10:8: error: unknown identifier 'x' Foo.x : Nat Foo.y : Nat -protected.lean:22:7: error: unknown identifier 'y' +protected.lean:22:7-22:8: error: unknown identifier 'y' z : Nat -protected.lean:25:14: error: protected declarations must be in a namespace -protected.lean:28:14: error: unknown identifier 'f' +protected.lean:25:14-25:15: error: protected declarations must be in a namespace +protected.lean:28:14-28:15: error: unknown identifier 'f' 8 -protected.lean:38:14: error: unknown identifier 'g' -protected.lean:47:6: error: unknown identifier 'g' -protected.lean:47:0: error: failed to synthesize +protected.lean:38:14-38:15: error: unknown identifier 'g' +protected.lean:47:6-47:7: error: unknown identifier 'g' +protected.lean:47:0-47:9: error: failed to synthesize Lean.Eval ?m 8 diff --git a/tests/lean/pureCoeIssue.lean.expected.out b/tests/lean/pureCoeIssue.lean.expected.out index 8b6bb6af52..18e82dd5ff 100644 --- a/tests/lean/pureCoeIssue.lean.expected.out +++ b/tests/lean/pureCoeIssue.lean.expected.out @@ -1,10 +1,10 @@ -pureCoeIssue.lean:6:2: error: type mismatch +pureCoeIssue.lean:6:2-6:4: error: type mismatch f1 has type Nat → IO Unit but is expected to have type EIO IO.Error PUnit -pureCoeIssue.lean:14:2: error: type mismatch +pureCoeIssue.lean:14:2-14:7: error: type mismatch f2 10 has type Nat → IO Unit diff --git a/tests/lean/redundantAlt.lean.expected.out b/tests/lean/redundantAlt.lean.expected.out index 773496d783..900f6e0842 100644 --- a/tests/lean/redundantAlt.lean.expected.out +++ b/tests/lean/redundantAlt.lean.expected.out @@ -1,2 +1,2 @@ -redundantAlt.lean:5:1: error: redundant alternative -redundantAlt.lean:7:1: error: redundant alternative +redundantAlt.lean:5:1-5:9: error: redundant alternative +redundantAlt.lean:7:1-7:9: error: redundant alternative diff --git a/tests/lean/rewrite.lean.expected.out b/tests/lean/rewrite.lean.expected.out index a66a463908..e579f7e762 100644 --- a/tests/lean/rewrite.lean.expected.out +++ b/tests/lean/rewrite.lean.expected.out @@ -1,7 +1,7 @@ α : Type ?u as bs : List α ⊢ as ++ bs ++ bs = as ++ (bs ++ bs) -rewrite.lean:12:20: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression +rewrite.lean:12:20-12:29: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression List.reverse (List.reverse ?m) α : Type ?u as bs : List α @@ -10,7 +10,7 @@ x y z : Nat h₁ : x = y h₂ : y = z ⊢ x = z -rewrite.lean:31:0: error: tactic 'rewrite' failed, did not find instance of the pattern in the current goal +rewrite.lean:31:0-31:24: error: tactic 'rewrite' failed, did not find instance of the pattern in the current goal x y z : Nat h₁ : 0 + x = y h₂ : 0 + y = z diff --git a/tests/lean/sanitychecks.lean.expected.out b/tests/lean/sanitychecks.lean.expected.out index a3a7f2aca3..8b4f0ca213 100644 --- a/tests/lean/sanitychecks.lean.expected.out +++ b/tests/lean/sanitychecks.lean.expected.out @@ -1,13 +1,13 @@ -sanitychecks.lean:1:8: error: fail to show termination for +sanitychecks.lean:1:8-1:15: error: fail to show termination for unsound with errors structural recursion cannot be used well founded recursion has not been implemented yet -sanitychecks.lean:4:8: error: 'partial' theorems are not allowed, 'partial' is a code generation directive -sanitychecks.lean:7:7: error: 'unsafe' theorems are not allowed -sanitychecks.lean:10:0: error: failed to synthesize instance +sanitychecks.lean:4:8-5:9: error: 'partial' theorems are not allowed, 'partial' is a code generation directive +sanitychecks.lean:7:7-8:9: error: 'unsafe' theorems are not allowed +sanitychecks.lean:10:0-10:9: error: failed to synthesize instance Inhabited False -sanitychecks.lean:18:0: error: failed to compile partial definition 'unsound3', failed to show that type is inhabited -sanitychecks.lean:20:12: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast' -sanitychecks.lean:23:12: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast' +sanitychecks.lean:18:0-18:40: error: failed to compile partial definition 'unsound3', failed to show that type is inhabited +sanitychecks.lean:20:12-20:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast' +sanitychecks.lean:23:12-23:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast' diff --git a/tests/lean/scopedInstanceOutsideNamespace.lean.expected.out b/tests/lean/scopedInstanceOutsideNamespace.lean.expected.out index 7f0c679f4d..dfa6088833 100644 --- a/tests/lean/scopedInstanceOutsideNamespace.lean.expected.out +++ b/tests/lean/scopedInstanceOutsideNamespace.lean.expected.out @@ -1,4 +1,4 @@ -scopedInstanceOutsideNamespace.lean:1:0: error: scoped attributes must be used inside namespaces +scopedInstanceOutsideNamespace.lean:1:0-2:38: error: scoped attributes must be used inside namespaces "true" -scopedInstanceOutsideNamespace.lean:6:0: error: scoped attributes must be used inside namespaces -scopedInstanceOutsideNamespace.lean:8:0: error: scoped attributes must be used inside namespaces +scopedInstanceOutsideNamespace.lean:6:0-6:3: error: scoped attributes must be used inside namespaces +scopedInstanceOutsideNamespace.lean:8:0-10:38: error: scoped attributes must be used inside namespaces diff --git a/tests/lean/scopedLocalInsts.lean.expected.out b/tests/lean/scopedLocalInsts.lean.expected.out index f315078da2..eddb8aafbb 100644 --- a/tests/lean/scopedLocalInsts.lean.expected.out +++ b/tests/lean/scopedLocalInsts.lean.expected.out @@ -1,15 +1,15 @@ -scopedLocalInsts.lean:12:6: error: failed to synthesize instance +scopedLocalInsts.lean:12:6-12:39: error: failed to synthesize instance ToString A -scopedLocalInsts.lean:12:0: error: failed to synthesize +scopedLocalInsts.lean:12:0-12:39: error: failed to synthesize Lean.Eval ?m "A.mk 10 20" -scopedLocalInsts.lean:21:6: error: failed to synthesize instance +scopedLocalInsts.lean:21:6-21:39: error: failed to synthesize instance ToString A -scopedLocalInsts.lean:21:0: error: failed to synthesize +scopedLocalInsts.lean:21:0-21:39: error: failed to synthesize Lean.Eval ?m "{ x := 10, y := 20 }" -scopedLocalInsts.lean:32:6: error: failed to synthesize instance +scopedLocalInsts.lean:32:6-32:39: error: failed to synthesize instance ToString A -scopedLocalInsts.lean:32:0: error: failed to synthesize +scopedLocalInsts.lean:32:0-32:39: error: failed to synthesize Lean.Eval ?m "A.mk 10 20" diff --git a/tests/lean/scopedMacros.lean.expected.out b/tests/lean/scopedMacros.lean.expected.out index e1483f79d5..ea15a2e013 100644 --- a/tests/lean/scopedMacros.lean.expected.out +++ b/tests/lean/scopedMacros.lean.expected.out @@ -1,6 +1,6 @@ 10 + 1 : Nat -scopedMacros.lean:11:7: error: unknown identifier 'foo!' +scopedMacros.lean:11:7-11:11: error: unknown identifier 'foo!' 10 + 1 : Nat -scopedMacros.lean:19:0: error: scoped attributes must be used inside namespaces -scopedMacros.lean:19:0: error: invalid syntax node kind 'termBla!_' -scopedMacros.lean:29:7: error: unknown identifier 'bla!' +scopedMacros.lean:19:0-19:37: error: scoped attributes must be used inside namespaces +scopedMacros.lean:19:0-19:7: error: invalid syntax node kind 'termBla!_' +scopedMacros.lean:29:7-29:11: error: unknown identifier 'bla!' diff --git a/tests/lean/scopedTokens.lean.expected.out b/tests/lean/scopedTokens.lean.expected.out index fc72026eaa..57dc077683 100644 --- a/tests/lean/scopedTokens.lean.expected.out +++ b/tests/lean/scopedTokens.lean.expected.out @@ -1,4 +1,4 @@ 20 + 1 : Nat -scopedTokens.lean:14:7: error: unknown identifier 'foo!' +scopedTokens.lean:14:7-14:11: error: unknown identifier 'foo!' foo! : Nat 20 + 1 : Nat diff --git a/tests/lean/scopedunifhint.lean.expected.out b/tests/lean/scopedunifhint.lean.expected.out index 7685114ad3..8a83fed6f0 100644 --- a/tests/lean/scopedunifhint.lean.expected.out +++ b/tests/lean/scopedunifhint.lean.expected.out @@ -1,4 +1,4 @@ -scopedunifhint.lean:28:7: error: application type mismatch +scopedunifhint.lean:28:7-28:14: error: application type mismatch mul x x argument x @@ -6,7 +6,7 @@ has type Nat but is expected to have type coeSort ?m -scopedunifhint.lean:29:7: error: application type mismatch +scopedunifhint.lean:29:7-29:24: error: application type mismatch mul (x, x) (x, x) argument (x, x) @@ -14,7 +14,7 @@ has type Nat × Nat but is expected to have type coeSort ?m -scopedunifhint.lean:33:7: error: application type mismatch +scopedunifhint.lean:33:7-33:10: error: application type mismatch x*x argument x @@ -24,7 +24,7 @@ but is expected to have type coeSort ?m x*x : coeSort Nat.Magma x*x : coeSort Nat.Magma -scopedunifhint.lean:39:7: error: application type mismatch +scopedunifhint.lean:39:7-39:24: error: application type mismatch (x, x)*(x, x) argument (x, x) @@ -33,7 +33,7 @@ has type but is expected to have type coeSort ?m (x, x)*(x, x) : coeSort (Prod.Magma Nat.Magma Nat.Magma) -scopedunifhint.lean:56:7: error: application type mismatch +scopedunifhint.lean:56:7-56:22: error: application type mismatch (x, x)*(x, x) argument (x, x) diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out index f7d198cebb..f315707757 100644 --- a/tests/lean/shadow.lean.expected.out +++ b/tests/lean/shadow.lean.expected.out @@ -1,30 +1,30 @@ -shadow.lean:6:0: error: type mismatch +shadow.lean:6:0-6:1: error: type mismatch h has type x✝ = x✝ but is expected to have type x = x -shadow.lean:10:0: error: type mismatch +shadow.lean:10:0-10:1: error: type mismatch h has type x = x but is expected to have type x = x -shadow.lean:13:0: error: don't know how to synthesize placeholder +shadow.lean:13:0-13:1: error: don't know how to synthesize placeholder context: α : Type u_1 inst✝¹ : Inhabited α inst✝ inst : α β✝ δ✝ : Type ⊢ α → β✝ → δ✝ → α × β✝ × δ✝ -shadow.lean:17:0: error: don't know how to synthesize placeholder +shadow.lean:17:0-17:1: error: don't know how to synthesize placeholder context: α : Type u_1 inst.68 : Inhabited α inst inst : α β.93 δ.94 : Type ⊢ α → β.93 → δ.94 → α × β.93 × δ.94 -shadow.lean:20:0: error: don't know how to synthesize placeholder +shadow.lean:20:0-20:1: error: don't know how to synthesize placeholder context: α : Type u_1 β : Sort u_2 diff --git a/tests/lean/sorryWarning.lean.expected.out b/tests/lean/sorryWarning.lean.expected.out index 736756888b..7c5e84cfe4 100644 --- a/tests/lean/sorryWarning.lean.expected.out +++ b/tests/lean/sorryWarning.lean.expected.out @@ -1 +1 @@ -sorryWarning.lean:2:2: warning: declaration uses 'sorry' +sorryWarning.lean:2:2-2:7: warning: declaration uses 'sorry' diff --git a/tests/lean/struct1.lean.expected.out b/tests/lean/struct1.lean.expected.out index 81f3b364ad..5c28f2a2c7 100644 --- a/tests/lean/struct1.lean.expected.out +++ b/tests/lean/struct1.lean.expected.out @@ -1,26 +1,26 @@ -struct1.lean:9:14: error: expected Type -struct1.lean:12:20: error: expected structure -struct1.lean:15:27: error: field 'toA' has already been declared -struct1.lean:18:27: error: field 'x' from 'B' has already been declared -struct1.lean:22:1: error: invalid field name '_x', identifiers starting with '_' are reserved to the system -struct1.lean:25:3: error: invalid field name '_y', identifiers starting with '_' are reserved to the system -struct1.lean:29:1: error: field 'x' has already been declared -struct1.lean:32:1: error: field 'x' has been declared in parent structure -struct1.lean:35:6: error: type mismatch +struct1.lean:9:14-9:17: error: expected Type +struct1.lean:12:20-12:29: error: expected structure +struct1.lean:15:27-15:33: error: field 'toA' has already been declared +struct1.lean:18:27-18:33: error: field 'x' from 'B' has already been declared +struct1.lean:22:1-22:3: error: invalid field name '_x', identifiers starting with '_' are reserved to the system +struct1.lean:25:3-25:5: error: invalid field name '_y', identifiers starting with '_' are reserved to the system +struct1.lean:29:1-29:2: error: field 'x' has already been declared +struct1.lean:32:1-32:2: error: field 'x' has been declared in parent structure +struct1.lean:35:6-35:10: error: type mismatch true has type Bool but is expected to have type Nat -struct1.lean:38:5: error: omit field 'x' type to set default value -struct1.lean:41:12: error: type mismatch +struct1.lean:38:5-38:9: error: omit field 'x' type to set default value +struct1.lean:41:12-41:16: error: type mismatch true has type Bool but is expected to have type Nat -struct1.lean:44:0: error: invalid 'private' constructor in a 'private' structure -struct1.lean:47:0: error: invalid 'protected' constructor in a 'private' structure -struct1.lean:50:0: error: invalid 'protected' field in a 'private' structure +struct1.lean:44:0-44:13: error: invalid 'private' constructor in a 'private' structure +struct1.lean:47:0-47:15: error: invalid 'protected' constructor in a 'private' structure +struct1.lean:50:0-50:19: error: invalid 'protected' field in a 'private' structure S : Type S.mk2 : Nat → S diff --git a/tests/lean/structAutoBound.lean.expected.out b/tests/lean/structAutoBound.lean.expected.out index e3e148a212..ecc433737e 100644 --- a/tests/lean/structAutoBound.lean.expected.out +++ b/tests/lean/structAutoBound.lean.expected.out @@ -1,8 +1,8 @@ inductive Foo.{v, u_1} : {α : Sort u_1} → (α → Type v) → Sort (max u_1 (v + 1)) constructors: Foo.mk : {α : Sort u_1} → {β : α → Type v} → (a : α) → β a → Foo β -structAutoBound.lean:9:15: error: a universe level named 'u' has already been declared +structAutoBound.lean:9:15-9:16: error: a universe level named 'u' has already been declared inductive Boo.{u, v} : Type u → Type v → Type (max u v) constructors: Boo.mk : {α : Type u} → {β : Type v} → α → β → Boo α β -structAutoBound.lean:18:0: error: unused universe parameter 'w' +structAutoBound.lean:18:0-20:7: error: unused universe parameter 'w' diff --git a/tests/lean/structDefault.lean.expected.out b/tests/lean/structDefault.lean.expected.out index ac18a5414b..eaf80b5189 100644 --- a/tests/lean/structDefault.lean.expected.out +++ b/tests/lean/structDefault.lean.expected.out @@ -1,4 +1,4 @@ -structDefault.lean:11:11: error: type mismatch +structDefault.lean:11:11-11:15: error: type mismatch true has type Bool diff --git a/tests/lean/structInstError.lean.expected.out b/tests/lean/structInstError.lean.expected.out index d595614467..32fc54a551 100644 --- a/tests/lean/structInstError.lean.expected.out +++ b/tests/lean/structInstError.lean.expected.out @@ -1,2 +1,2 @@ -structInstError.lean:5:7: error: invalid {...} notation, expected type is not known +structInstError.lean:5:7-5:29: error: invalid {...} notation, expected type is not known { x := 10, b := true } : Foo diff --git a/tests/lean/substlet.lean.expected.out b/tests/lean/substlet.lean.expected.out index 9c278cdafb..f17ae2e8eb 100644 --- a/tests/lean/substlet.lean.expected.out +++ b/tests/lean/substlet.lean.expected.out @@ -18,7 +18,7 @@ case intro n : Nat m : Nat := n ⊢ 0 + n = n -substlet.lean:25:2: error: tactic 'subst' failed, variable 'v' is a let-declaration +substlet.lean:25:2-25:9: error: tactic 'subst' failed, variable 'v' is a let-declaration n : Nat h : n = 0 m : Nat := n + 1 diff --git a/tests/lean/syntaxErrors.lean.expected.out b/tests/lean/syntaxErrors.lean.expected.out index 5cb4ca7113..97dfaa08b5 100644 --- a/tests/lean/syntaxErrors.lean.expected.out +++ b/tests/lean/syntaxErrors.lean.expected.out @@ -1,2 +1,2 @@ -syntaxErrors.lean:1:7: error: parser 'withPosition' does not take two arguments -syntaxErrors.lean:3:7: error: parser 'withPosition' is not a constant, it takes one argument +syntaxErrors.lean:1:7-1:33: error: parser 'withPosition' does not take two arguments +syntaxErrors.lean:3:7-3:19: error: parser 'withPosition' is not a constant, it takes one argument diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh index 6ca44fe528..f9171faec0 100755 --- a/tests/lean/test_single.sh +++ b/tests/lean/test_single.sh @@ -2,5 +2,5 @@ source ../common.sh # these tests don't have to succeed -exec_capture lean "$f" || true +exec_capture lean -DprintMessageEndPos=true "$f" || true diff_produced diff --git a/tests/lean/theoremType.lean.expected.out b/tests/lean/theoremType.lean.expected.out index 8c71c1feb4..2a843b34ec 100644 --- a/tests/lean/theoremType.lean.expected.out +++ b/tests/lean/theoremType.lean.expected.out @@ -1,6 +1,6 @@ -theoremType.lean:1:22: error: don't know how to synthesize placeholder +theoremType.lean:1:22-1:23: error: don't know how to synthesize placeholder context: ⊢ Nat -theoremType.lean:4:18: error: don't know how to synthesize placeholder +theoremType.lean:4:18-4:19: error: don't know how to synthesize placeholder context: ⊢ Nat diff --git a/tests/lean/typeIncorrectPat.lean.expected.out b/tests/lean/typeIncorrectPat.lean.expected.out index 09bae8a93e..b52d5338e5 100644 --- a/tests/lean/typeIncorrectPat.lean.expected.out +++ b/tests/lean/typeIncorrectPat.lean.expected.out @@ -1,4 +1,4 @@ -typeIncorrectPat.lean:2:1: error: pattern +typeIncorrectPat.lean:2:1-2:17: error: pattern true has type Bool diff --git a/tests/lean/typeMismatch.lean.expected.out b/tests/lean/typeMismatch.lean.expected.out index 42c6cbd9fa..dbf7faba23 100644 --- a/tests/lean/typeMismatch.lean.expected.out +++ b/tests/lean/typeMismatch.lean.expected.out @@ -1,10 +1,10 @@ -typeMismatch.lean:7:0: error: type mismatch +typeMismatch.lean:7:0-7:13: error: type mismatch IO.println "" has type IO Unit but is expected to have type IO Nat -typeMismatch.lean:12:0: error: type mismatch +typeMismatch.lean:12:0-12:16: error: type mismatch Meta.isDefEq x x has type MetaM Bool diff --git a/tests/lean/typeOf.lean.expected.out b/tests/lean/typeOf.lean.expected.out index 9e8785f4e3..5b7eff61e1 100644 --- a/tests/lean/typeOf.lean.expected.out +++ b/tests/lean/typeOf.lean.expected.out @@ -1,13 +1,13 @@ -typeOf.lean:11:21: error: failed to synthesize instance +typeOf.lean:11:21-11:24: error: failed to synthesize instance HAdd Nat Nat Bool -typeOf.lean:12:0: error: failed to synthesize instance +typeOf.lean:12:0-12:5: error: failed to synthesize instance HAdd Bool Nat Nat -typeOf.lean:10:4: error: (kernel) declaration has metavariables 'f2' -typeOf.lean:20:54: error: invalid reassignment, term has type +typeOf.lean:10:4-10:6: error: (kernel) declaration has metavariables 'f2' +typeOf.lean:20:54-20:60: error: invalid reassignment, term has type Bool but is expected to have type Nat -typeOf.lean:29:53: error: natural number expected, value has type +typeOf.lean:29:53-29:57: error: natural number expected, value has type Bool but is expected to have type Nat diff --git a/tests/lean/univInference.lean.expected.out b/tests/lean/univInference.lean.expected.out index 18162bc9dc..e34301a95e 100644 --- a/tests/lean/univInference.lean.expected.out +++ b/tests/lean/univInference.lean.expected.out @@ -1,9 +1,9 @@ -univInference.lean:26:0: error: failed to compute resulting universe level of inductive datatype, provide universe explicitly +univInference.lean:26:0-28:9: error: failed to compute resulting universe level of inductive datatype, provide universe explicitly S6 : Sort (max w₁ w₂) → Type w₂ → Sort (max w₁ (w₂ + 1)) -univInference.lean:46:0: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u' +univInference.lean:46:0-47:17: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u' max u v -univInference.lean:65:0: error: failed to compute resulting universe level of inductive datatype, provide universe explicitly -univInference.lean:74:0: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u' +univInference.lean:65:0-66:22: error: failed to compute resulting universe level of inductive datatype, provide universe explicitly +univInference.lean:74:0-75:22: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u' max u v -univInference.lean:82:0: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u' +univInference.lean:82:0-83:22: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u' max u v diff --git a/tests/lean/unknownId.lean.expected.out b/tests/lean/unknownId.lean.expected.out index bd3a6f5a5e..0bcf12387c 100644 --- a/tests/lean/unknownId.lean.expected.out +++ b/tests/lean/unknownId.lean.expected.out @@ -1,3 +1,3 @@ -unknownId.lean:3:7: error: unknown identifier 'bla✝' -unknownId.lean:6:2: error: unknown identifier 'bla✝' -unknownId.lean:11:6: error: unknown identifier 'bla✝' +unknownId.lean:3:7-3:10: error: unknown identifier 'bla✝' +unknownId.lean:6:2-6:5: error: unknown identifier 'bla✝' +unknownId.lean:11:6-11:9: error: unknown identifier 'bla✝' diff --git a/tests/lean/unsolvedIndCases.lean.expected.out b/tests/lean/unsolvedIndCases.lean.expected.out index ba80291432..504c01c5ba 100644 --- a/tests/lean/unsolvedIndCases.lean.expected.out +++ b/tests/lean/unsolvedIndCases.lean.expected.out @@ -1,43 +1,43 @@ -unsolvedIndCases.lean:3:11: error: unsolved goals +unsolvedIndCases.lean:3:11-3:13: error: unsolved goals case zero ⊢ 0 + Nat.zero = Nat.zero -unsolvedIndCases.lean:4:11: error: unsolved goals +unsolvedIndCases.lean:4:11-4:13: error: unsolved goals case succ y : Nat ⊢ 0 + Nat.succ y = Nat.succ y -unsolvedIndCases.lean:8:14: error: unsolved goals +unsolvedIndCases.lean:8:14-8:16: error: unsolved goals case zero ⊢ 0 + Nat.zero = Nat.zero -unsolvedIndCases.lean:9:14: error: unsolved goals +unsolvedIndCases.lean:9:14-9:16: error: unsolved goals case succ y : Nat ih : 0 + y = y ⊢ 0 + Nat.succ y = Nat.succ y -unsolvedIndCases.lean:14:11: error: unsolved goals +unsolvedIndCases.lean:14:11-14:13: error: unsolved goals case succ y : Nat ⊢ 0 + Nat.succ y = Nat.succ y -unsolvedIndCases.lean:18:18: error: unsolved goals +unsolvedIndCases.lean:18:18-18:20: error: unsolved goals case ind x y : Nat h₁ : 0 < y ∧ y ≤ x ih : y > 0 → (x - y) % y < y h : y > 0 ⊢ x % y < y -unsolvedIndCases.lean:19:18: error: unsolved goals +unsolvedIndCases.lean:19:18-19:20: error: unsolved goals case base x y : Nat h₁ : ¬(0 < y ∧ y ≤ x) h : y > 0 ⊢ x % y < y -unsolvedIndCases.lean:23:18: error: unsolved goals +unsolvedIndCases.lean:23:18-23:20: error: unsolved goals case ind x y : Nat h : y > 0 h₁ : 0 < y ∧ y ≤ x ih : x = x - y → y = y → x % y < y ⊢ x % y < y -unsolvedIndCases.lean:24:18: error: unsolved goals +unsolvedIndCases.lean:24:18-24:20: error: unsolved goals case base x y : Nat h : y > 0 diff --git a/tests/lean/unused_univ.lean.expected.out b/tests/lean/unused_univ.lean.expected.out index 92faefa1f7..009a531546 100644 --- a/tests/lean/unused_univ.lean.expected.out +++ b/tests/lean/unused_univ.lean.expected.out @@ -1,3 +1,3 @@ -unused_univ.lean:5:0: error: unused universe parameter 'u' -unused_univ.lean:10:0: error: unused universe parameter 'w' -unused_univ.lean:13:0: error: unused universe parameter 'w' +unused_univ.lean:5:0-6:1: error: unused universe parameter 'u' +unused_univ.lean:10:0-11:1: error: unused universe parameter 'w' +unused_univ.lean:13:0-13:36: error: unused universe parameter 'w' diff --git a/tests/lean/weirdmacro.lean.expected.out b/tests/lean/weirdmacro.lean.expected.out index e377c0dc13..542bf1e782 100644 --- a/tests/lean/weirdmacro.lean.expected.out +++ b/tests/lean/weirdmacro.lean.expected.out @@ -1,4 +1,4 @@ weirdmacro.lean:1:6: error: expected no space before ':' or string literal -weirdmacro.lean:1:30: error: elaboration function for 'antiquot' has not been implemented +weirdmacro.lean:1:30-1:32: error: elaboration function for 'antiquot' has not been implemented weirdmacro.lean:1:32: error: expected term -weirdmacro.lean:3:7: error: unknown identifier 'term' +weirdmacro.lean:3:7-3:11: error: unknown identifier 'term'