diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 8847007bb..9fc877ec5 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -7,6 +7,8 @@ import Data.List import Data.List1 import Data.Vect import Parser.Source +import Text.PrettyPrint.Prettyprinter +import Text.PrettyPrint.Prettyprinter.Util import public Data.IORef import System @@ -44,6 +46,15 @@ Show DotReason where show UserDotted = "User dotted" show UnknownDot = "Unknown reason" +export +Pretty DotReason where + pretty NonLinearVar = reflow "Non linear pattern variable" + pretty VarApplied = reflow "Variable applied to arguments" + pretty NotConstructor = reflow "Not a constructor application or primitive" + pretty ErasedArg = reflow "Erased argument" + pretty UserDotted = reflow "User dotted" + pretty UnknownDot = reflow "Unknown reason" + -- All possible errors, carrying a location public export data Error : Type where diff --git a/src/Core/TT.idr b/src/Core/TT.idr index 1bbf98835..1208db432 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -8,7 +8,8 @@ import Data.List import Data.NameMap import Data.Vect import Decidable.Equality -import Text.PrettyPrint.PrettyPrinter +import Text.PrettyPrint.Prettyprinter +import Text.PrettyPrint.Prettyprinter.Util import public Algebra @@ -101,8 +102,8 @@ Pretty Constant where pretty (B16 x) = pretty x pretty (B32 x) = pretty x pretty (B64 x) = pretty x - pretty (Str x) = pretty x - pretty (Ch x) = pretty x + pretty (Str x) = dquotes (pretty x) + pretty (Ch x) = squotes (pretty x) pretty (Db x) = pretty x pretty WorldVal = pretty "%MkWorld" pretty IntType = pretty "Int" @@ -557,6 +558,12 @@ Show Visibility where show Export = "export" show Public = "public export" +export +Pretty Visibility where + pretty Private = pretty "private" + pretty Export = pretty "export" + pretty Public = pretty "public" <+> pretty "export" + export Eq Visibility where Private == Private = True @@ -610,6 +617,16 @@ Show PartialReason where show (RecPath ns) = "possibly not terminating due to recursive path " ++ showSep " -> " (map show ns) +export +Pretty PartialReason where + pretty NotStrictlyPositive = reflow "not strictly positive" + pretty (BadCall [n]) + = reflow "possibly not terminating due to call to" <++> pretty n + pretty (BadCall ns) + = reflow "possibly not terminating due to calls to" <++> concatWith (surround (comma <+> space)) (pretty <$> ns) + pretty (RecPath ns) + = reflow "possibly not terminating due to recursive path" <++> concatWith (surround (pretty " -> ")) (pretty <$> ns) + public export data Terminating = Unchecked @@ -622,6 +639,12 @@ Show Terminating where show IsTerminating = "terminating" show (NotTerminating p) = show p +export +Pretty Terminating where + pretty Unchecked = reflow "not yet checked" + pretty IsTerminating = pretty "terminating" + pretty (NotTerminating p) = pretty p + public export data Covering = IsCovering @@ -637,6 +660,15 @@ Show Covering where show (NonCoveringCall cs) = "not covering due to calls to functions " ++ showSep ", " (map show cs) +export +Pretty Covering where + pretty IsCovering = pretty "covering" + pretty (MissingCases c) = reflow "not covering all cases" + pretty (NonCoveringCall [f]) + = reflow "not covering due to call to function" <++> pretty f + pretty (NonCoveringCall cs) + = reflow "not covering due to calls to functions" <++> concatWith (surround (comma <+> space)) (pretty <$> cs) + -- Totality status of a definition. We separate termination checking from -- coverage checking. public export @@ -648,7 +680,7 @@ record Totality where export Show Totality where show tot - = let t = isTerminating tot + = let t = isTerminating tot c = isCovering tot in showTot t c where @@ -658,6 +690,13 @@ Show Totality where showTot t IsCovering = show t showTot t c = show c ++ "; " ++ show t +export +Pretty Totality where + pretty (MkTotality IsTerminating IsCovering) = pretty "total" + pretty (MkTotality IsTerminating c) = pretty c + pretty (MkTotality t IsCovering) = pretty t + pretty (MkTotality t c) = pretty c <+> semi <++> pretty t + export unchecked : Totality unchecked = MkTotality Unchecked IsCovering diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 2bdcd7c51..3e73f31af 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -73,6 +73,10 @@ data CLOpt Quiet | ||| Run Idris 2 in verbose mode (cancels quiet if it's the default) Verbose | + ||| Set the console width for REPL output + ConsoleWidth Nat | + ||| Whether to use color in the console output + Color Bool | ||| Set the log level globally Logging Nat | ||| Add a package as a dependency @@ -214,6 +218,12 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] (Just "Suppress the banner"), MkOpt ["--quiet", "-q"] [] [Quiet] (Just "Quiet mode; display fewer messages"), + MkOpt ["--consolewidth"] [RequiredNat "console width"] (\l => [ConsoleWidth l]) + (Just "Width for console output (0 for unbounded) (120 by default)"), + MkOpt ["--color", "--colour"] [] ([Color True]) + (Just "Forces colored console output (enabled by default)"), + MkOpt ["--no-color", "--no-colour"] [] ([Color False]) + (Just "Disables colored console output"), MkOpt ["--verbose"] [] [Verbose] (Just "Verbose mode (default)"), MkOpt ["--log"] [RequiredNat "log level"] (\l => [Logging l]) diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index c82e4a42e..d5cf2f135 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -47,19 +47,21 @@ pshowNoNorm env tm ploc : {auto o : Ref ROpts REPLOpts} -> FC -> Core (Doc IdrisAnn) ploc EmptyFC = pure emptyDoc -ploc (MkFC _ s e) = do +ploc fc@(MkFC fn s e) = do let sr = fromInteger $ cast $ fst s let sc = fromInteger $ cast $ snd s let er = fromInteger $ cast $ fst e let ec = fromInteger $ cast $ snd e let nsize = length $ show (er + 1) + let head = annotate FileCtxt (pretty fc) + let firstRow = annotate FileCtxt (spaces (cast $ nsize + 2) <+> pipe) source <- lines <$> getCurrentElabSource if sr == er then do - let line = maybe emptyDoc pretty (elemAt source sr) - let emph = spaces (cast sc) <+> pretty (Extra.replicate (ec `minus` sc) '^') - pure $ space <+> pretty (sr + 1) <++> pipe <++> align (vsep [line, emph]) - else pure $ vsep (addLineNumbers nsize sr (pretty <$> extractRange sr (Prelude.min er (sr + 5)) source)) + let line = (annotate FileCtxt pipe) <++> maybe emptyDoc pretty (elemAt source sr) + let emph = (annotate FileCtxt pipe) <++> spaces (cast sc) <+> annotate Error (pretty (Extra.replicate (ec `minus` sc) '^')) + pure $ vsep [emptyDoc, head, firstRow, annotate FileCtxt (space <+> pretty (sr + 1)) <++> align (vsep [line, emph]), emptyDoc] + else pure $ vsep (emptyDoc :: head :: addLineNumbers nsize sr (pretty <$> extractRange sr (Prelude.min er (sr + 5)) source)) <+> line where extractRange : Nat -> Nat -> List String -> List String extractRange s e xs = take ((e `minus` s) + 1) (drop s xs) @@ -67,7 +69,7 @@ ploc (MkFC _ s e) = do pad size s = replicate (size `minus` length s) '0' ++ s addLineNumbers : Nat -> Nat -> List (Doc IdrisAnn) -> List (Doc IdrisAnn) addLineNumbers size st xs = - snd $ foldl (\(i, s), l => (S i, snoc s (space <+> pretty (pad size $ show $ i + 1) <++> pipe <++> l))) (st, []) xs + snd $ foldl (\(i, s), l => (S i, snoc s (space <+> annotate FileCtxt (pretty (pad size $ show $ i + 1) <++> pipe) <++> l))) (st, []) xs export perror : {auto c : Ref Ctxt Defs} -> @@ -76,88 +78,80 @@ perror : {auto c : Ref Ctxt Defs} -> Error -> Core (Doc IdrisAnn) perror (Fatal err) = perror err perror (CantConvert fc env l r) - = pure $ vsep [ reflow "Mismatch between" <+> colon - , indent 4 !(pshow env l) + = pure $ errorDesc (hsep [ reflow "Mismatch between" <+> colon + , code !(pshow env l) , pretty "and" - , indent 4 !(pshow env r) - , pretty "at" <+> colon - , !(ploc fc) - ] + , code !(pshow env r) <+> dot + ]) <+> line <+> !(ploc fc) perror (CantSolveEq fc env l r) - = pure $ vsep [ reflow "Can't solve constraint between" <+> colon - , indent 4 !(pshow env l) + = pure $ errorDesc (hsep [ reflow "Can't solve constraint between" <+> colon + , code !(pshow env l) , pretty "and" - , indent 4 !(pshow env r) - , pretty "at" <+> colon - , !(ploc fc) - ] + , code !(pshow env r) <+> dot + ]) <+> line <+> !(ploc fc) perror (PatternVariableUnifies fc env n tm) - = pure $ vsep [ reflow "Pattern variable" <++> pretty (showPVar n) <++> reflow "unifies with" <+> colon - , indent 4 !(pshow env tm) - , pretty "at" <+> colon - , !(ploc fc) - ] + = pure $ errorDesc (hsep [ reflow "Pattern variable" + , code (prettyVar n) + , reflow "unifies with" <+> colon + , code !(pshow env tm) <+> dot + ]) <+> line <+> !(ploc fc) where - showPVar : Name -> String - showPVar (PV n _) = showPVar n - showPVar n = show n + prettyVar : Name -> Doc IdrisAnn + prettyVar (PV n _) = prettyVar n + prettyVar n = pretty n perror (CyclicMeta fc env n tm) - = pure $ reflow "Cycle detected in solution of metavariable" <++> pretty !(prettyName n) <++> equals - <++> !(pshow env tm) <++> pretty "at" <+> colon <+> line - <+> !(ploc fc) + = pure $ errorDesc (reflow "Cycle detected in solution of metavariable" <++> meta (pretty !(prettyName n)) <++> equals + <++> code !(pshow env tm)) <+> line <+> !(ploc fc) perror (WhenUnifying _ env x y err) - = pure $ reflow "When unifying" <++> !(pshow env x) <++> pretty "and" - <++> !(pshow env y) <+> line - <+> !(perror err) + = pure $ errorDesc (reflow "When unifying" <++> code !(pshow env x) <++> pretty "and" + <++> code !(pshow env y)) <+> dot <+> line <+> !(perror err) perror (ValidCase fc env (Left tm)) - = pure $ !(pshow env tm) <++> reflow "is not a valid impossible case at" - <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (code !(pshow env tm) <++> reflow "is not a valid impossible case.") + <+> line <+> !(ploc fc) perror (ValidCase _ env (Right err)) - = pure $ reflow "Impossible pattern gives an error" <+> colon <+> line <+> !(perror err) + = pure $ errorDesc (reflow "Impossible pattern gives an error" <+> colon) <+> line <+> !(perror err) perror (UndefinedName fc x) - = pure $ reflow "Undefined name" <++> pretty (show x) - <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Undefined name" <++> code (pretty x) <+> dot) <++> line <+> !(ploc fc) perror (InvisibleName fc n (Just ns)) - = pure $ pretty "Name" <++> pretty (show n) <++> reflow "is inaccessible since" - <++> concatWith (surround dot) (pretty <$> reverse ns) <++> reflow "is not explicitly imported at" - <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (pretty "Name" <++> code (pretty n) <++> reflow "is inaccessible since" + <++> code (concatWith (surround dot) (pretty <$> reverse ns)) <++> reflow "is not explicitly imported.") + <+> line <+> !(ploc fc) perror (InvisibleName fc x Nothing) - = pure $ pretty "Name" <++> pretty (show x) <++> reflow "is private at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (pretty "Name" <++> code (pretty x) <++> reflow "is private.") <+> line <+> !(ploc fc) perror (BadTypeConType fc n) - = pure $ reflow "Return type of" <++> pretty (show n) <++> reflow "must be Type at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Return type of" <++> code (pretty n) <++> reflow "must be" <++> code (pretty "Type") + <+> dot) <+> line <+> !(ploc fc) perror (BadDataConType fc n fam) - = pure $ reflow "Return type of" <++> pretty (show n) <++> reflow "must be in" - <++> pretty (show !(toFullNames fam)) <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Return type of" <++> code (pretty n) <++> reflow "must be in" + <++> code (pretty !(toFullNames fam))) <++> line <+> !(ploc fc) perror (NotCovering fc n IsCovering) - = pure $ reflow "Internal error" <++> parens (reflow "Coverage of" <++> pretty (show n)) + = pure $ errorDesc (reflow "Internal error" <++> parens (reflow "Coverage of" <++> code (pretty n))) perror (NotCovering fc n (MissingCases cs)) - = pure $ vsep [ pretty !(prettyName n) <++> reflow "is not covering at" <+> colon - , !(ploc fc) - , reflow "Missing cases" <+> colon - , indent 4 (vsep !(traverse (pshow []) cs)) - ] + = pure $ errorDesc (code (pretty !(prettyName n)) <++> reflow "is not covering.") + <+> line <+> !(ploc fc) <+> line + <+> reflow "Missing cases" <+> colon <+> line + <+> indent 4 (vsep !(traverse (pshow []) cs)) perror (NotCovering fc n (NonCoveringCall ns)) - = pure $ vsep [ pretty !(prettyName n) <++> reflow "is not covering at" <+> colon - , !(ploc fc) - , reflow "Calls non covering function" <+> - case ns of - [fn] => space <+> pretty (show fn) - _ => pretty 's' <+> colon <++> concatWith (surround (comma <+> space)) (pretty . show <$> ns) - ] + = pure $ errorDesc (pretty !(prettyName n) <++> reflow "is not covering.") + <+> line <+> !(ploc fc) <+> line + <+> reflow "Calls non covering function" <+> + case ns of + [fn] => space <+> pretty fn + _ => pretty 's' <+> colon <++> concatWith (surround (comma <+> space)) (pretty <$> ns) perror (NotTotal fc n r) - = pure $ vsep [ pretty !(prettyName n) <++> reflow "is not total" <+> colon - , pretty (show r) - , pretty "at" <+> colon - , !(ploc fc) - ] + = pure $ errorDesc (code (pretty !(prettyName n)) <++> reflow "is not total," <++> pretty r) + <+> line <+> !(ploc fc) perror (LinearUsed fc count n) - = pure $ reflow "There are" <++> pretty (show count) <++> reflow "uses of linear name" <++> pretty (sugarName n) - <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "There are" <++> pretty count <++> reflow "uses of linear name" + <++> code (pretty (sugarName n)) <+> dot) + <++> line <+> !(ploc fc) perror (LinearMisuse fc n exp ctx) = if isErased exp - then pure $ pretty (show n) <++> reflow "is not accessible in this context at" <+> colon <+> line <+> !(ploc fc) - else pure $ reflow "Trying to use" <++> prettyRig exp <++> pretty "name" <++> pretty (sugarName n) <++> - pretty "in" <++> prettyRel ctx <++> pretty "context at" <+> colon <+> line <+> !(ploc fc) + then pure $ errorDesc (code (pretty n) <++> reflow "is not accessible in this context.") + <+> line <+> !(ploc fc) + else pure $ errorDesc (reflow "Trying to use" <++> prettyRig exp <++> pretty "name" + <++> code (pretty (sugarName n)) <++> pretty "in" <++> prettyRel ctx <++> pretty "context.") + <+> line <+> !(ploc fc) where prettyRig : RigCount -> Doc ann prettyRig = elimSemi (pretty "irrelevant") @@ -169,45 +163,43 @@ perror (LinearMisuse fc n exp ctx) (pretty "relevant") (const $ pretty "non-linear") perror (BorrowPartial fc env tm arg) - = pure $ !(pshow env tm) <++> - reflow "borrows argument" <++> !(pshow env arg) <++> - reflow "so must be fully applied at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (code !(pshow env tm) <++> reflow "borrows argument" <++> code !(pshow env arg) + <++> reflow "so must be fully applied.") + <+> line <+> !(ploc fc) perror (BorrowPartialType fc env tm) - = pure $ !(pshow env tm) <++> - reflow "borrows, so must return a concrete type at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (code !(pshow env tm) <++> + reflow "borrows, so must return a concrete type.") <+> line <+> !(ploc fc) perror (AmbiguousName fc ns) - = pure $ pretty "Ambiguous name" <++> pretty (show ns) <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (pretty "Ambiguous name" <++> code (pretty ns)) + <+> line <+> !(ploc fc) perror (AmbiguousElab fc env ts) = do pp <- getPPrint setPPrint (record { fullNamespace = True } pp) - let res = vsep [ reflow "Ambiguous elaboration at" <+> colon - , !(ploc fc) - , reflow "Possible correct results" <+> colon + let res = vsep [ errorDesc (reflow "Ambiguous elaboration. Possible results" <+> colon) , indent 4 (vsep !(traverse (pshow env) ts)) - ] + ] <+> line <+> !(ploc fc) setPPrint pp pure res perror (AmbiguousSearch fc env tgt ts) - = pure $ vsep [ reflow "Multiple solutions found in search of" <+> colon + = pure $ vsep [ errorDesc (reflow "Multiple solutions found in search of" <+> colon) , indent 4 !(pshowNoNorm env tgt) - , pretty "at" <+> colon , !(ploc fc) , reflow "Possible correct results" <+> colon , indent 4 (vsep !(traverse (pshowNoNorm env) ts)) ] perror (AmbiguityTooDeep fc n ns) - = pure $ reflow "Maximum ambiguity depth exceeded in" <++> pretty (show !(getFullName n)) - <+> colon <++> concatWith (surround (pretty " --> ")) (pretty . show <$> !(traverse getFullName ns)) - <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Maximum ambiguity depth exceeded in" <++> code (pretty !(getFullName n)) + <+> colon) <+> line <+> concatWith (surround (pretty " --> ")) (pretty <$> !(traverse getFullName ns)) + <++> line <+> !(ploc fc) perror (AllFailed ts) = case allUndefined ts of Just e => perror e - _ => pure $ reflow "Sorry, I can't find any elaboration which works. All errors" <+> colon <+> line + _ => pure $ errorDesc (reflow "Sorry, I can't find any elaboration which works. All errors" <+> colon) <+> line <+> vsep !(traverse pAlterror ts) where pAlterror : (Maybe Name, Error) -> Core (Doc IdrisAnn) pAlterror (Just n, err) - = pure $ pretty "If" <++> pretty (show !(aliasName !(getFullName n))) <+> colon <++> !(perror err) <+> line + = pure $ pretty "If" <++> code (pretty !(aliasName !(getFullName n))) <+> colon <++> !(perror err) pAlterror (Nothing, err) = pure $ reflow "Possible error" <+> colon <+> line <+> indent 4 !(perror err) @@ -217,39 +209,39 @@ perror (AllFailed ts) allUndefined ((_, UndefinedName _ e) :: es) = allUndefined es allUndefined _ = Nothing perror (RecordTypeNeeded fc _) - = pure $ reflow "Can't infer type for this record update at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Can't infer type for this record update.") <+> line <+> !(ploc fc) perror (NotRecordField fc fld Nothing) - = pure $ pretty fld <++> reflow "is not part of a record type at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (code (pretty fld) <++> reflow "is not part of a record type.") <+> line <+> !(ploc fc) perror (NotRecordField fc fld (Just ty)) - = pure $ reflow "Record type" <++> pretty (show !(getFullName ty)) <++> reflow "has no field" <++> pretty fld - <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Record type" <++> code (pretty !(getFullName ty)) <++> reflow "has no field" + <++> code (pretty fld) <+> dot) <+> line <+> !(ploc fc) perror (NotRecordType fc ty) - = pure $ pretty (show !(getFullName ty)) <++> reflow "is not a record type at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (code (pretty !(getFullName ty)) <++> reflow "is not a record type.") <+> line <+> !(ploc fc) perror (IncompatibleFieldUpdate fc flds) = pure $ reflow "Field update" <++> concatWith (surround (pretty "->")) (pretty <$> flds) <++> reflow "not compatible with other updates at" <+> colon <+> line <+> !(ploc fc) perror (InvalidImplicits fc env [Just n] tm) - = pure $ pretty (show n) <++> reflow "is not a valid implicit argument in" <++> !(pshow env tm) - <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (code (pretty n) <++> reflow "is not a valid implicit argument in" <++> !(pshow env tm) + <+> dot) <+> line <+> !(ploc fc) perror (InvalidImplicits fc env ns tm) - = pure $ concatWith (surround (comma <+> space)) (pretty . show <$> ns) - <++> reflow "are not valid implicit arguments in" <++> !(pshow env tm) - <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (concatWith (surround (comma <+> space)) (code . pretty <$> ns) + <++> reflow "are not valid implicit arguments in" <++> !(pshow env tm) <+> dot) + <+> line <+> !(ploc fc) perror (TryWithImplicits fc env imps) - = pure $ reflow "Need to bind implicits" - <++> concatWith (surround (comma <+> space)) !(traverse (tshow env) imps) - <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Need to bind implicits" + <++> concatWith (surround (comma <+> space)) !(traverse (tshow env) imps) <+> dot) + <+> line <+> !(ploc fc) where tshow : {vars : _} -> Env Term vars -> (Name, Term vars) -> Core (Doc IdrisAnn) - tshow env (n, ty) = pure $ pretty (show n) <++> colon <++> !(pshow env ty) + tshow env (n, ty) = pure $ pretty n <++> colon <++> code !(pshow env ty) perror (BadUnboundImplicit fc env n ty) - = pure $ reflow "Can't bind name" <++> pretty (nameRoot n) <++> reflow "with type" <++> !(pshow env ty) - <++> reflow "here at" <+> colon <+> line <+> !(ploc fc) <+> line <+> reflow "Try binding explicitly." + = pure $ errorDesc (reflow "Can't bind name" <++> code (pretty (nameRoot n)) <++> reflow "with type" <++> code !(pshow env ty) + <+> colon) <+> line <+> !(ploc fc) <+> line <+> reflow "Try binding explicitly." perror (CantSolveGoal fc env g) = let (_ ** (env', g')) = dropEnv env g in - pure $ reflow "Can't find an implementation for" <++> !(pshow env' g') - <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + pure $ errorDesc (reflow "Can't find an implementation for" <++> code !(pshow env' g') + <+> dot) <+> line <+> !(ploc fc) where -- For display, we don't want to see the full top level type; just the -- return type @@ -261,101 +253,105 @@ perror (CantSolveGoal fc env g) dropEnv env tm = (_ ** (env, tm)) perror (DeterminingArg fc n i env g) - = pure $ reflow "Can't find an implementation for" <++> !(pshow env g) <+> line - <+> reflow "since I can't infer a value for argument" <++> pretty (show n) - <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Can't find an implementation for" <++> code !(pshow env g) <+> line + <+> reflow "since I can't infer a value for argument" <++> code (pretty n) <+> dot) + <+> line <+> !(ploc fc) perror (UnsolvedHoles hs) - = pure $ reflow "Unsolved holes" <+> colon <+> line <+> prettyHoles hs + = pure $ errorDesc (reflow "unsolved holes" <+> colon) <+> line <+> !(prettyHoles hs) where - prettyHoles : List (FC, Name) -> Doc IdrisAnn - prettyHoles [] = emptyDoc + prettyHoles : List (FC, Name) -> Core (Doc IdrisAnn) + prettyHoles [] = pure emptyDoc prettyHoles ((fc, n) :: hs) - = pretty (show n) <++> reflow "introduced at" <++> pretty (show fc) <+> line <+> prettyHoles hs + = pure $ meta (pretty n) <++> reflow "introduced at:" <++> !(ploc fc) <+> !(prettyHoles hs) perror (CantInferArgType fc env n h ty) - = pure $ reflow "Can't infer type for argument" <++> pretty (show n) <+> line - <+> pretty "Got" <++> !(pshow env ty) <++> reflow "with hole" <++> pretty (show h) - <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Can't infer type for argument" <++> code (pretty n)) <+> line + <+> pretty "Got" <++> code !(pshow env ty) <++> reflow "with hole" <++> meta (pretty h) <+> dot + <+> line <+> !(ploc fc) perror (SolvedNamedHole fc env h tm) - = pure $ reflow "Named hole" <++> pretty (show h) <++> reflow "has been solved by unification" <+> line - <+> pretty "Result" <+> colon <++> !(pshow env tm) - <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Named hole" <++> meta (pretty h) <++> reflow "has been solved by unification.") <+> line + <+> pretty "Result" <+> colon <++> code !(pshow env tm) + <+> line <+> !(ploc fc) perror (VisibilityError fc vx x vy y) - = pure $ pretty (show vx) <++> pretty (sugarName !(toFullNames x)) - <++> reflow "cannot refer to" <++> pretty (show vy) <++> pretty (sugarName !(toFullNames y)) - <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (keyword (pretty vx) <++> code (pretty (sugarName !(toFullNames x))) + <++> reflow "cannot refer to" <++> keyword (pretty vy) <++> code (pretty (sugarName !(toFullNames y)))) + <+> line <+> !(ploc fc) perror (NonLinearPattern fc n) - = pure $ reflow "Non linear pattern" <++> pretty (sugarName n) <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Non linear pattern" <++> code (pretty (sugarName n)) <+> dot) <+> line <+> !(ploc fc) perror (BadPattern fc n) - = pure $ reflow "Pattern not allowed here" <+> colon <++> pretty (show n) <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Pattern not allowed here" <+> colon <++> code (pretty n) <+> dot) <+> line <+> !(ploc fc) perror (NoDeclaration fc n) - = pure $ reflow "No type declaration for" <++> pretty (show n) <++> pretty "at" <+> colon <+> line <+> !(ploc fc) -perror (AlreadyDefined fc n) = pure $ pretty (show n) <++> reflow "is already defined" + = pure $ errorDesc (reflow "No type declaration for" <++> code (pretty n) <+> dot) <+> line <+> !(ploc fc) +perror (AlreadyDefined fc n) = pure $ errorDesc (code (pretty n) <++> reflow "is already defined.") <+> line <+> !(ploc fc) perror (NotFunctionType fc env tm) - = pure $ !(pshow env tm) <++> reflow "is not a function type at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (code !(pshow env tm) <++> reflow "is not a function type.") <+> line <+> !(ploc fc) perror (RewriteNoChange fc env rule ty) - = pure $ reflow "Rewriting by" <++> !(pshow env rule) - <++> reflow "did not change type" <++> !(pshow env ty) - <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Rewriting by" <++> code !(pshow env rule) + <++> reflow "did not change type" <++> code !(pshow env ty) <+> dot) + <+> line <+> !(ploc fc) perror (NotRewriteRule fc env rule) - = pure $ !(pshow env rule) <++> reflow "is not a rewrite rule type at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (code !(pshow env rule) <++> reflow "is not a rewrite rule type.") <+> line <+> !(ploc fc) perror (CaseCompile fc n DifferingArgNumbers) - = pure $ reflow "Patterns for" <++> pretty !(prettyName n) <++> reflow "have differing numbers of arguments at" - <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Patterns for" <++> code (pretty !(prettyName n)) <++> reflow "have differing numbers of arguments.") + <+> line <+> !(ploc fc) perror (CaseCompile fc n DifferingTypes) - = pure $ reflow "Patterns for" <++> pretty !(prettyName n) <++> reflow "require matching on different types at" - <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Patterns for" <++> code (pretty !(prettyName n)) <++> reflow "require matching on different types.") + <+> line <+> !(ploc fc) perror (CaseCompile fc n UnknownType) - = pure $ reflow "Can't infer type to match in" <++> pretty !(prettyName n) <++> pretty "at" - <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Can't infer type to match in" <++> code (pretty !(prettyName n)) <+> dot) + <+> line <+> !(ploc fc) perror (CaseCompile fc n (NotFullyApplied cn)) - = pure $ pretty "Constructor" <++> pretty (show !(toFullNames cn)) <++> reflow "is not fully applied at" - <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (pretty "Constructor" <++> code (pretty !(toFullNames cn)) <++> reflow "is not fully applied.") + <+> line <+> !(ploc fc) perror (CaseCompile fc n (MatchErased (_ ** (env, tm)))) - = pure $ reflow "Attempt to match on erased argument" <++> !(pshow env tm) <++> pretty "in" - <++> pretty !(prettyName n) <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Attempt to match on erased argument" <++> code !(pshow env tm) <++> pretty "in" + <++> code (pretty !(prettyName n)) <+> dot) <+> line <+> !(ploc fc) perror (BadDotPattern fc env reason x y) - = pure $ reflow "Can't match on" <++> !(pshow env x) - <++> parens (pretty (show reason)) <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Can't match on" <++> code !(pshow env x) + <++> parens (pretty reason) <+> dot) <+> line <+> !(ploc fc) perror (MatchTooSpecific fc env tm) - = pure $ reflow "Can't match on" <++> !(pshow env tm) - <++> reflow "as it has a polymorphic type at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Can't match on" <++> code !(pshow env tm) + <++> reflow "as it has a polymorphic type.") <+> line <+> !(ploc fc) perror (BadImplicit fc str) - = pure $ reflow "Can't infer type for unbound implicit name" <++> pretty str <++> pretty "at" <+> colon + = pure $ errorDesc (reflow "Can't infer type for unbound implicit name" <++> code (pretty str) <+> dot) <+> line <+> !(ploc fc) <+> line <+> reflow "Try making it a bound implicit." perror (BadRunElab fc env script) - = pure $ reflow "Bad elaborator script" <++> !(pshow env script) - <++> pretty "at" <+> colon <+> line <+> !(ploc fc) -perror (GenericMsg fc str) = pure $ pretty str <++> pretty "at" <+> colon <+> line <+> !(ploc fc) + = pure $ errorDesc (reflow "Bad elaborator script" <++> code !(pshow env script) <+> dot) + <+> line <+> !(ploc fc) +perror (GenericMsg fc str) = pure $ pretty str <+> line <+> !(ploc fc) perror (TTCError msg) - = pure $ reflow "Error in TTC file" <+> colon <++> pretty (show msg) + = pure $ errorDesc (reflow "Error in TTC file" <+> colon <++> pretty (show msg)) <++> parens (pretty "the most likely case is that the ./build directory in your current project contains files from a previous build of idris2 or the idris2 executable is from a different build than the installed .ttc files") perror (FileErr fname err) - = pure $ reflow "File error in" <++> pretty fname <++> colon <++> pretty (show err) + = pure $ errorDesc (reflow "File error in" <++> pretty fname <++> colon) <++> pretty (show err) perror (ParseFail _ err) = pure $ pretty (show err) perror (ModuleNotFound _ ns) - = pure $ concatWith (surround dot) (pretty <$> reverse ns) <++> reflow "not found" + = pure $ errorDesc (concatWith (surround dot) (pretty <$> reverse ns) <++> reflow "not found") perror (CyclicImports ns) - = pure $ reflow "Module imports form a cycle" <+> colon <++> concatWith (surround (pretty " -> ")) (prettyMod <$> ns) + = pure $ errorDesc (reflow "Module imports form a cycle" <+> colon) <++> concatWith (surround (pretty " -> ")) (prettyMod <$> ns) where prettyMod : List String -> Doc IdrisAnn prettyMod ns = concatWith (surround dot) (pretty <$> reverse ns) -perror ForceNeeded = pure $ reflow "Internal error when resolving implicit laziness" -perror (InternalError str) = pure $ reflow "INTERNAL ERROR" <+> colon <++> pretty str -perror (UserError str) = pure $ pretty "Error" <+> colon <++> pretty str +perror ForceNeeded = pure $ errorDesc (reflow "Internal error when resolving implicit laziness") +perror (InternalError str) = pure $ errorDesc (reflow "INTERNAL ERROR" <+> colon) <++> pretty str +perror (UserError str) = pure $ errorDesc (pretty "Error" <+> colon) <++> pretty str perror (InType fc n err) - = pure $ reflow "While processing type of" <++> pretty !(prettyName n) - <++> pretty "at" <++> pretty (show fc) <+> colon <+> line <+> !(perror err) + = pure $ hsep [ errorDesc (reflow "While processing type of" <++> code (pretty !(prettyName n))) <+> dot + , !(perror err) + ] perror (InCon fc n err) - = pure $ reflow "While processing constructor" <++> pretty !(prettyName n) - <++> pretty "at" <++> pretty (show fc) <+> colon <+> line <+> !(perror err) + = pure $ hsep [ errorDesc (reflow "While processing constructor" <++> code (pretty !(prettyName n))) <+> dot + , !(perror err) + ] perror (InLHS fc n err) - = pure $ reflow "While processing left hand side of" <++> pretty !(prettyName n) - <++> pretty "at" <++> pretty (show fc) <+> colon <+> line <+> !(perror err) + = pure $ hsep [ errorDesc (reflow "While processing left hand side of" <++> code (pretty !(prettyName n))) <+> dot + , !(perror err) + ] perror (InRHS fc n err) - = pure $ reflow "While processing right hand side of" <++> pretty !(prettyName n) - <++> pretty "at" <++> pretty (show fc) <+> colon <+> line <+> !(perror err) + = pure $ hsep [ errorDesc (reflow "While processing right hand side of" <++> code (pretty !(prettyName n))) <+> dot + , !(perror err) + ] export pwarning : {auto c : Ref Ctxt Defs} -> @@ -363,9 +359,9 @@ pwarning : {auto c : Ref Ctxt Defs} -> {auto o : Ref ROpts REPLOpts} -> Warning -> Core (Doc IdrisAnn) pwarning (UnreachableClause fc env tm) - = pure $ annotate Warning (pretty "Warning" <+> colon) - <++> pretty "unreachable clause" <+> colon - <++> !(pshow env tm) + = pure $ errorDesc (reflow "Unreachable clause:" + <++> code !(pshow env tm)) + <+> line <+> !(ploc fc) prettyMaybeLoc : Maybe FC -> Doc IdrisAnn prettyMaybeLoc Nothing = emptyDoc @@ -376,8 +372,8 @@ display : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto o : Ref ROpts REPLOpts} -> Error -> Core (Doc IdrisAnn) -display err - = pure $ prettyMaybeLoc (getErrorLoc err) <+> !(perror err) +display err = do + pure $ annotate Error (pretty "Error:") <++> !(perror err) export displayWarning : {auto c : Ref Ctxt Defs} -> @@ -385,4 +381,4 @@ displayWarning : {auto c : Ref Ctxt Defs} -> {auto o : Ref ROpts REPLOpts} -> Warning -> Core (Doc IdrisAnn) displayWarning w - = pure $ prettyMaybeLoc (getWarningLoc w) <+> !(pwarning w) + = pure $ annotate Warning (pretty "Warning:") <++> !(pwarning w) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index dee36a5b5..fdaf16643 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1785,6 +1785,9 @@ data CmdArg : Type where ||| The command takes a string StringArg : CmdArg + ||| The command takes a on or off. + OnOffArg : CmdArg + ||| The command takes multiple arguments. Args : List CmdArg -> CmdArg @@ -1799,6 +1802,7 @@ Show CmdArg where show FileArg = "" show ModuleArg = "" show StringArg = "" + show OnOffArg = "(on|off)" show (Args args) = showSep " " (map show args) export @@ -1925,6 +1929,19 @@ numberArgCmd parseCmd command doc = (names, NumberArg, doc, parse) i <- intLit pure (command (fromInteger i)) +onOffArgCmd : ParseCmd -> (Bool -> REPLCmd) -> String -> CommandDefinition +onOffArgCmd parseCmd command doc = (names, OnOffArg, doc, parse) + where + names : List String + names = extractNames parseCmd + + parse : Rule REPLCmd + parse = do + symbol ":" + runParseCmd parseCmd + i <- onOffLit + pure (command i) + compileArgsCmd : ParseCmd -> (PTerm -> String -> REPLCmd) -> String -> CommandDefinition compileArgsCmd parseCmd command doc = (names, Args [FileArg, ExprArg], doc, parse) @@ -1961,6 +1978,8 @@ parserCommandsForHelp = , nameArgCmd (ParseIdentCmd "doc") Doc "Show documentation for a name" , moduleArgCmd (ParseIdentCmd "browse") Browse "Browse contents of a namespace" , numberArgCmd (ParseREPLCmd ["log", "logging"]) SetLog "Set logging level" + , numberArgCmd (ParseREPLCmd ["consolewidth"]) SetConsoleWidth "Set the width of the console output (0 for unbounded)" + , onOffArgCmd (ParseREPLCmd ["color", "colour"]) SetColor "Whether to use color for the console output (enabled by default)" , noArgCmd (ParseREPLCmd ["m", "metavars"]) Metavars "Show remaining proof obligations (metavariables or holes)" , noArgCmd (ParseREPLCmd ["version"]) ShowVersion "Display the Idris version" , noArgCmd (ParseREPLCmd ["?", "h", "help"]) Help "Display this help text" diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr index 9703c9128..7b877e6d9 100644 --- a/src/Idris/Pretty.idr +++ b/src/Idris/Pretty.idr @@ -5,51 +5,51 @@ import Text.PrettyPrint.Prettyprinter import Text.PrettyPrint.Prettyprinter.Render.Terminal import Text.PrettyPrint.Prettyprinter.Util +import Idris.REPLOpts import Idris.Syntax %default covering -public export -data SyntaxAnn - = Typ - | Function - | Data - | Keyword - | Bound - | Pragma - | Meta - public export data IdrisAnn = Warning | Error + | ErrorDesc | FileCtxt - | Syntax SyntaxAnn + | Code + | Meta + | Keyword + | Pragma export colorAnn : IdrisAnn -> AnsiStyle -colorAnn Warning = color Yellow -colorAnn Error = color BrightRed +colorAnn Warning = color Yellow <+> bold +colorAnn Error = color BrightRed <+> bold +colorAnn ErrorDesc = bold colorAnn FileCtxt = color BrightBlue -colorAnn (Syntax Typ) = color Magenta -colorAnn (Syntax Function) = neutral -colorAnn (Syntax Data) = color Blue -colorAnn (Syntax Keyword) = color Red -colorAnn (Syntax Bound) = color Green -colorAnn (Syntax Pragma) = color BrightMagenta -colorAnn (Syntax Meta) = color Magenta +colorAnn Code = color Magenta +colorAnn Keyword = color Red +colorAnn Pragma = color BrightMagenta +colorAnn Meta = color Green +export +errorDesc : Doc IdrisAnn -> Doc IdrisAnn +errorDesc = annotate ErrorDesc + +export keyword : Doc IdrisAnn -> Doc IdrisAnn --- keyword = annotate (Syntax Keyword) -keyword = id +keyword = annotate Keyword -meta : String -> Doc IdrisAnn --- meta s = annotate (Syntax Meta) (pretty s) -meta s = pretty s +export +meta : Doc IdrisAnn -> Doc IdrisAnn +meta = annotate Meta + +export +code : Doc IdrisAnn -> Doc IdrisAnn +code = annotate Code ite : Doc IdrisAnn -> Doc IdrisAnn -> Doc IdrisAnn -> Doc IdrisAnn --- ite x t e = keyword (pretty "if") <++> x <++> hang 3 (fillSep [keyword (pretty "then") <++> t, keyword (pretty "else") <++> e]) -ite x t e = (pretty "if") <++> x <++> hang 3 (fillSep [(pretty "then") <++> t, (pretty "else") <++> e]) +ite x t e = keyword (pretty "if") <++> x <++> align (fillSep [keyword (pretty "then") <++> t, keyword (pretty "else") <++> e]) let_ : Doc IdrisAnn let_ = keyword (pretty "let") @@ -84,13 +84,9 @@ default_ = keyword (pretty "default") rewrite_ : Doc IdrisAnn rewrite_ = keyword (pretty "rewrite") -pragma : String -> Doc IdrisAnn --- pragma s = annotate (Syntax Pragma) (pretty s) -pragma s = (pretty s) - -bound : Doc IdrisAnn -> Doc IdrisAnn --- bound = annotate (Syntax Bound) -bound = id +export +pragma : Doc IdrisAnn -> Doc IdrisAnn +pragma = annotate Pragma prettyParens : (1 _ : Bool) -> Doc ann -> Doc ann prettyParens False s = s @@ -189,16 +185,15 @@ mutual else go d f <++> braces (pretty n <++> equals <++> pretty a) go d (PImplicitApp _ f (Just n) a) = go d f <++> braces (pretty n <++> equals <++> go d a) - go d (PSearch _ _) = pragma "%search" + go d (PSearch _ _) = pragma (pretty "%search") go d (PQuote _ tm) = pretty '`' <+> parens (go d tm) go d (PQuoteName _ n) = pretty '`' <+> braces (braces (pretty n)) go d (PQuoteDecl _ tm) = pretty '`' <+> brackets (angles (angles (pretty "declaration"))) go d (PUnquote _ tm) = pretty '~' <+> parens (go d tm) - go d (PRunElab _ tm) = pragma "%runElab" <++> go d tm + go d (PRunElab _ tm) = pragma (pretty "%runElab") <++> go d tm go d (PPrimVal _ c) = pretty c - go d (PHole _ _ n) = meta (strCons '?' n) - -- go d (PType _) = annotate (Syntax Typ) (pretty "Type") - go d (PType _) = (pretty "Type") + go d (PHole _ _ n) = meta (pretty (strCons '?' n)) + go d (PType _) = pretty "Type" go d (PAs _ n p) = pretty n <+> pretty '@' <+> go d p go d (PDotted _ p) = dot <+> go d p go d (PImplicit _) = pretty '_' @@ -242,3 +237,24 @@ mutual go d (PPostfixProjsSection fc fields args) = parens (dot <+> concatWith (surround dot) (go d <$> fields) <+> fillSep (go App <$> args)) go d (PWithUnambigNames fc ns rhs) = with_ <++> pretty ns <++> go d rhs + +export +render : {auto o : Ref ROpts REPLOpts} -> Doc IdrisAnn -> Core String +render doc = do + consoleWidth <- getConsoleWidth + color <- getColor + let opts = MkLayoutOptions $ if consoleWidth == 0 + then Unbounded + else AvailablePerLine (cast consoleWidth) 1 + let layout = layoutPretty opts doc + pure $ renderString $ if color then reAnnotateS colorAnn layout else unAnnotateS layout + +export +renderWithoutColor : {auto o : Ref ROpts REPLOpts} -> Doc IdrisAnn -> Core String +renderWithoutColor doc = do + consoleWidth <- getConsoleWidth + let opts = MkLayoutOptions $ if consoleWidth == 0 + then Unbounded + else AvailablePerLine (cast consoleWidth) 1 + let layout = layoutPretty opts doc + pure $ renderString $ unAnnotateS layout diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 5feaeaab0..cdd6b848d 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -54,6 +54,7 @@ import Data.NameMap import Data.Stream import Data.Strings import Text.PrettyPrint.Prettyprinter +import Text.PrettyPrint.Prettyprinter.Util import Text.PrettyPrint.Prettyprinter.Render.Terminal import System @@ -534,6 +535,8 @@ data REPLResult : Type where FoundHoles : List HoleData -> REPLResult OptionsSet : List REPLOpt -> REPLResult LogLevelSet : Nat -> REPLResult + ConsoleWidthSet : Nat -> REPLResult + ColorSet : Bool -> REPLResult VersionIs : Version -> REPLResult DefDeclared : REPLResult Exited : REPLResult @@ -766,6 +769,12 @@ process GetOpts process (SetLog lvl) = do setLogLevel lvl pure $ LogLevelSet lvl +process (SetConsoleWidth n) + = do setConsoleWidth n + pure $ ConsoleWidthSet n +process (SetColor b) + = do setColor b + pure $ ColorSet b process Metavars = do defs <- get Ctxt let ctxt = gamma defs @@ -819,9 +828,8 @@ processCatch cmd put UST u' put Syn s' put ROpts o' - pmsg <- display err - let msg = reAnnotateS colorAnn $ layoutPretty defaultLayoutOptions pmsg -- FIXME: tmp - pure $ REPLError $ renderString msg + msg <- display err >>= render + pure $ REPLError msg ) parseEmptyCmd : SourceEmptyRule (Maybe REPLCmd) @@ -928,38 +936,66 @@ mutual {auto s : Ref Syn SyntaxInfo} -> {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> REPLResult -> Core () - displayResult (REPLError err) = printError err - displayResult (Evaluated x Nothing) = printResult $ show x - displayResult (Evaluated x (Just y)) = printResult $ show x ++ " : " ++ show y - displayResult (Printed xs) = printResult (showSep "\n" xs) - displayResult (TermChecked x y) = printResult $ show x ++ " : " ++ show y - displayResult (FileLoaded x) = printResult $ "Loaded file " ++ x - displayResult (ModuleLoaded x) = printResult $ "Imported module " ++ x - displayResult (ErrorLoadingModule x err) = printError $ "Error loading module " ++ x ++ ": " ++ (renderString (layoutPretty defaultLayoutOptions (reAnnotate colorAnn !(perror err)))) -- FIXME: tmp - displayResult (ErrorLoadingFile x err) = printError $ "Error loading file " ++ x ++ ": " ++ show err - displayResult (ErrorsBuildingFile x errs) = printError $ "Error(s) building file " ++ x -- messages already displayed while building - displayResult NoFileLoaded = printError "No file can be reloaded" - displayResult (CurrentDirectory dir) = printResult ("Current working directory is '" ++ dir ++ "'") - displayResult CompilationFailed = printError "Compilation failed" - displayResult (Compiled f) = printResult $ "File " ++ f ++ " written" - displayResult (ProofFound x) = printResult $ show x - displayResult (Missed cases) = printResult $ showSep "\n" $ map handleMissing cases - displayResult (CheckedTotal xs) = printResult $ showSep "\n" $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs - displayResult (FoundHoles []) = printResult $ "No holes" - displayResult (FoundHoles [x]) = printResult $ "1 hole: " ++ show x.name - displayResult (FoundHoles xs) = printResult $ show (length xs) ++ " holes: " ++ - showSep ", " (map (show . name) xs) - displayResult (LogLevelSet k) = printResult $ "Set loglevel to " ++ show k - displayResult (VersionIs x) = printResult $ showVersion True x - displayResult (RequestedHelp) = printResult displayHelp - displayResult (Edited (DisplayEdit [])) = pure () - displayResult (Edited (DisplayEdit xs)) = printResult $ showSep "\n" xs - displayResult (Edited (EditError x)) = printError x - displayResult (Edited (MadeLemma lit name pty pappstr)) = printResult (relit lit (show name ++ " : " ++ show pty ++ "\n") ++ pappstr) - displayResult (Edited (MadeWith lit wapp)) = printResult $ showSep "\n" (map (relit lit) wapp) - displayResult (Edited (MadeCase lit cstr)) = printResult $ showSep "\n" (map (relit lit) cstr) - displayResult (OptionsSet opts) = printResult $ showSep "\n" $ map show opts - displayResult _ = pure () + displayResult (REPLError err) = printError err + displayResult (Evaluated x Nothing) = do + term <- render (prettyTerm x) + printResult term + displayResult (Evaluated x (Just y)) = do + term <- render (prettyTerm x <++> colon <++> code (prettyTerm y)) + printResult term + displayResult (Printed xs) = do + xs' <- render (vsep (pretty <$> xs)) + printResult xs' + displayResult (TermChecked x y) = do + term <- render (prettyTerm x <++> colon <++> code (prettyTerm y)) + printResult term + displayResult (FileLoaded x) = do + msg <- render (reflow "Loaded file" <++> pretty x) + printResult msg + displayResult (ModuleLoaded x) = do + msg <- render (reflow "Imported module" <++> pretty x) + printResult msg + displayResult (ErrorLoadingModule x err) = do + msg <- render (reflow "Error loading module" <++> pretty x <+> colon <++> !(perror err)) + printError msg + displayResult (ErrorLoadingFile x err) = do + msg <- render (reflow "Error loading file" <++> pretty x <+> colon <++> pretty (show err)) + printError msg + displayResult (ErrorsBuildingFile x errs) = do + msg <- render (reflow "Error(s) building file" <++> pretty x) + printError msg -- messages already displayed while building + displayResult NoFileLoaded = printError !(render (reflow "No file can be reloaded")) + displayResult (CurrentDirectory dir) = do + msg <- render (reflow "Current working directory is" <++> squotes (pretty dir)) + printResult msg + displayResult CompilationFailed = printError !(render (reflow "Compilation failed")) + displayResult (Compiled f) = do + msg <- render (pretty "File" <++> pretty f <++> pretty "written") + printResult msg + displayResult (ProofFound x) = printResult !(render (prettyTerm x)) + displayResult (Missed cases) = printResult $ showSep "\n" $ map handleMissing cases -- FIXME + displayResult (CheckedTotal xs) = do + msg <- render (vsep (map (\(fn, tot) => pretty fn <++> pretty "is" <++> pretty tot) xs)) + printResult msg + displayResult (FoundHoles []) = printResult !(render (reflow "No holes")) + displayResult (FoundHoles [x]) = printResult !(render (reflow "1 hole" <+> colon <++> pretty x.name)) + displayResult (FoundHoles xs) = do + let holes = concatWith (surround (pretty ", ")) (pretty . name <$> xs) + msg <- render (pretty (length xs) <++> pretty "holes" <+> colon <++> holes) + printResult msg + displayResult (LogLevelSet k) = printResult !(render (reflow "Set loglevel to" <++> pretty k)) + displayResult (ConsoleWidthSet k) = printResult !(render (reflow "Set consolewidth to" <++> pretty k)) + displayResult (ColorSet b) = printResult !(render (reflow (if b then "Set color on" else "Set color off"))) + displayResult (VersionIs x) = printResult !(render (pretty (showVersion True x))) + displayResult (RequestedHelp) = printResult displayHelp -- FIXME + displayResult (Edited (DisplayEdit [])) = pure () + displayResult (Edited (DisplayEdit xs)) = printResult $ showSep "\n" xs + displayResult (Edited (EditError x)) = printError x + displayResult (Edited (MadeLemma lit name pty pappstr)) = printResult (relit lit (show name ++ " : " ++ show pty ++ "\n") ++ pappstr) + displayResult (Edited (MadeWith lit wapp)) = printResult $ showSep "\n" (map (relit lit) wapp) + displayResult (Edited (MadeCase lit cstr)) = printResult $ showSep "\n" (map (relit lit) cstr) + displayResult (OptionsSet opts) = printResult !(render (vsep (pretty <$> opts))) + displayResult _ = pure () export displayHelp : String @@ -983,5 +1019,7 @@ mutual {auto s : Ref Syn SyntaxInfo} -> {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> REPLResult -> Core () - displayErrors (ErrorLoadingFile x err) = printError $ "File error in " ++ x ++ ": " ++ show err + displayErrors (ErrorLoadingFile x err) = do + msg <- render (reflow "File error in" <++> pretty x <+> colon <++> pretty (show err)) + printError msg displayErrors _ = pure () diff --git a/src/Idris/REPLCommon.idr b/src/Idris/REPLCommon.idr index 428c889a2..fdc5baca7 100644 --- a/src/Idris/REPLCommon.idr +++ b/src/Idris/REPLCommon.idr @@ -61,12 +61,10 @@ emitError err = do opts <- get ROpts case idemode opts of REPL _ => - do pmsg <- reAnnotate colorAnn <$> display err - let msg = renderString (layoutPretty defaultLayoutOptions pmsg) -- FIXME: tmp + do msg <- display err >>= render coreLift $ putStrLn msg IDEMode i _ f => - do pmsg <- reAnnotate colorAnn <$> perror err - let msg = renderString (layoutPretty defaultLayoutOptions pmsg) -- FIXME: tmp + do msg <- perror err >>= renderWithoutColor case getErrorLoc err of Nothing => iputStrLn msg Just fc => @@ -91,12 +89,10 @@ emitWarning w = do opts <- get ROpts case idemode opts of REPL _ => - do pmsg <- reAnnotate colorAnn <$> displayWarning w - let msg = renderString (layoutPretty defaultLayoutOptions pmsg) -- FIXME: tmp + do msg <- displayWarning w >>= render coreLift $ putStrLn msg IDEMode i _ f => - do pmsg <- reAnnotate colorAnn <$> pwarning w - let msg = renderString (layoutPretty defaultLayoutOptions pmsg) -- FIXME: tmp + do msg <- pwarning w >>= renderWithoutColor case getWarningLoc w of Nothing => iputStrLn msg Just fc => diff --git a/src/Idris/REPLOpts.idr b/src/Idris/REPLOpts.idr index 6b434eda5..62585964d 100644 --- a/src/Idris/REPLOpts.idr +++ b/src/Idris/REPLOpts.idr @@ -34,12 +34,14 @@ record REPLOpts where -- TODO: Move extraCodegens from here, it doesn't belong, but there's nowhere -- better to stick it now. extraCodegens : List (String, Codegen) + consoleWidth : Nat + color : Bool export defaultOpts : Maybe String -> OutputMode -> List (String, Codegen) -> REPLOpts defaultOpts fname outmode cgs = MkREPLOpts False NormaliseAll fname (litStyle fname) "" "vim" - Nothing outmode "" Nothing Nothing cgs + Nothing outmode "" Nothing Nothing cgs 120 True where litStyle : Maybe String -> Maybe LiterateStyle litStyle Nothing = Nothing @@ -141,3 +143,23 @@ getCodegen : {auto o : Ref ROpts REPLOpts} -> String -> Core (Maybe Codegen) getCodegen s = do opts <- get ROpts pure $ lookup s (extraCodegens opts) + +export +getConsoleWidth : {auto o : Ref ROpts REPLOpts} -> Core Nat +getConsoleWidth = do opts <- get ROpts + pure $ opts.consoleWidth + +export +setConsoleWidth : {auto o : Ref ROpts REPLOpts} -> Nat -> Core () +setConsoleWidth n = do opts <- get ROpts + put ROpts (record { consoleWidth = n } opts) + +export +getColor : {auto o : Ref ROpts REPLOpts} -> Core Bool +getColor = do opts <- get ROpts + pure $ opts.color + +export +setColor : {auto o : Ref ROpts REPLOpts} -> Bool -> Core () +setColor b = do opts <- get ROpts + put ROpts (record { color = b } opts) diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index d1de37335..98d4665c7 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -118,6 +118,12 @@ preOptions (DumpVMCode f :: opts) preOptions (Logging n :: opts) = do setSession (record { logLevel = n } !getSession) preOptions opts +preOptions (ConsoleWidth n :: opts) + = do setConsoleWidth n + preOptions opts +preOptions (Color b :: opts) + = do setColor b + preOptions opts preOptions (_ :: opts) = preOptions opts -- Options to be processed after type checking. Returns whether execution diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 7c98f9f05..9119216b7 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -15,6 +15,8 @@ import Data.ANameMap import Data.List import Data.NameMap import Data.StringMap +import Text.PrettyPrint.Prettyprinter +import Text.PrettyPrint.Prettyprinter.Util %default covering @@ -360,6 +362,12 @@ Show REPLEval where show NormaliseAll = "normalise" show Execute = "execute" +export +Pretty REPLEval where + pretty EvalTC = pretty "typecheck" + pretty NormaliseAll = pretty "normalise" + pretty Execute = pretty "execute" + public export data REPLOpt : Type where ShowImplicits : Bool -> REPLOpt @@ -378,6 +386,14 @@ Show REPLOpt where show (Editor editor) = "editor = " ++ show editor show (CG str) = "cg = " ++ str +export +Pretty REPLOpt where + pretty (ShowImplicits impl) = pretty "showimplicits" <++> equals <++> pretty impl + pretty (ShowNamespace ns) = pretty "shownamespace" <++> equals <++> pretty ns + pretty (ShowTypes typs) = pretty "showtypes" <++> equals <++> pretty typs + pretty (EvalMode mod) = pretty "eval" <++> equals <++> pretty mod + pretty (Editor editor) = pretty "editor" <++> equals <++> pretty editor + pretty (CG str) = pretty "cg" <++> equals <++> pretty str public export data EditCmd : Type where @@ -417,6 +433,8 @@ data REPLCmd : Type where Doc : Name -> REPLCmd Browse : List String -> REPLCmd SetLog : Nat -> REPLCmd + SetConsoleWidth : Nat -> REPLCmd + SetColor : Bool -> REPLCmd Metavars : REPLCmd Editing : EditCmd -> REPLCmd ShowVersion : REPLCmd diff --git a/src/Parser/Rule/Source.idr b/src/Parser/Rule/Source.idr index 2d4683ee9..1be048116 100644 --- a/src/Parser/Rule/Source.idr +++ b/src/Parser/Rule/Source.idr @@ -70,6 +70,15 @@ intLit IntegerLit i => Just i _ => Nothing) +export +onOffLit : Rule Bool +onOffLit + = terminal "Expected on or off" + (\x => case tok x of + Ident "on" => Just True + Ident "off" => Just False + _ => Nothing) + export strLit : Rule String strLit diff --git a/tests/chez/chez001/run b/tests/chez/chez001/run index be8b6c9a1..7b4861c3b 100755 --- a/tests/chez/chez001/run +++ b/tests/chez/chez001/run @@ -1,3 +1,3 @@ -$1 --no-banner Total.idr < input +$1 --no-color --no-banner Total.idr < input rm -rf build diff --git a/tests/chez/chez002/run b/tests/chez/chez002/run index 6cc0deda5..9acdde0e5 100755 --- a/tests/chez/chez002/run +++ b/tests/chez/chez002/run @@ -1,2 +1,2 @@ -$1 --no-banner Pythag.idr < input +$1 --no-color --no-banner Pythag.idr < input rm -rf build diff --git a/tests/chez/chez003/run b/tests/chez/chez003/run index de9e1bb30..2a8fc3099 100755 --- a/tests/chez/chez003/run +++ b/tests/chez/chez003/run @@ -1,2 +1,2 @@ -$1 --no-banner IORef.idr < input +$1 --no-color --no-banner IORef.idr < input rm -rf build diff --git a/tests/chez/chez004/run b/tests/chez/chez004/run index 42c7841b6..363603003 100755 --- a/tests/chez/chez004/run +++ b/tests/chez/chez004/run @@ -1,2 +1,2 @@ -$1 -p contrib --no-banner Buffer.idr < input +$1 --no-color -p contrib --no-banner Buffer.idr < input rm -rf build test.buf diff --git a/tests/chez/chez005/run b/tests/chez/chez005/run index 1d3408f3c..8350eb077 100755 --- a/tests/chez/chez005/run +++ b/tests/chez/chez005/run @@ -1,3 +1,3 @@ -$1 --no-banner Filter.idr < input +$1 --no-color --no-banner Filter.idr < input rm -rf build diff --git a/tests/chez/chez006/expected b/tests/chez/chez006/expected index 09d6bf97f..268ec12cd 100644 --- a/tests/chez/chez006/expected +++ b/tests/chez/chez006/expected @@ -15,13 +15,17 @@ Main> Main.strangeId': strangeId' _ Main> Bye for now! 1/1: Building TypeCase2 (TypeCase2.idr) -TypeCase2.idr:5:14--5:17:While processing left hand side -of strangeId at TypeCase2.idr:5:1--6:1: -Can't match on Nat (Erased argument) at: +Error: While processing left hand side of strangeId. Can't match on Nat (Erased argument). + +TypeCase2.idr:5:14--5:17 + | 5 | strangeId {a=Nat} x = x+1 - ^^^ -TypeCase2.idr:9:5--9:8:While processing left hand side -of foo at TypeCase2.idr:9:1--10:1: -Can't match on Nat (Erased argument) at: + | ^^^ + +Error: While processing left hand side of foo. Can't match on Nat (Erased argument). + +TypeCase2.idr:9:5--9:8 + | 9 | foo Nat = "Nat" - ^^^ + | ^^^ + diff --git a/tests/chez/chez006/run b/tests/chez/chez006/run index 780e18baf..8d7409331 100755 --- a/tests/chez/chez006/run +++ b/tests/chez/chez006/run @@ -1,4 +1,4 @@ -$1 --no-banner TypeCase.idr < input -$1 --no-banner TypeCase2.idr --check +$1 --no-color --no-banner TypeCase.idr < input +$1 --no-color --no-banner TypeCase2.idr --check rm -rf build diff --git a/tests/chez/chez007/run b/tests/chez/chez007/run index c8819a02f..cd67b1298 100755 --- a/tests/chez/chez007/run +++ b/tests/chez/chez007/run @@ -1,3 +1,3 @@ -$1 --no-banner TypeCase.idr < input +$1 --no-color --no-banner TypeCase.idr < input rm -rf build diff --git a/tests/chez/chez008/run b/tests/chez/chez008/run index 6a6a4c9a8..12b776604 100755 --- a/tests/chez/chez008/run +++ b/tests/chez/chez008/run @@ -1,3 +1,3 @@ -$1 --no-banner Nat.idr < input +$1 --no-color --no-banner Nat.idr < input rm -rf build diff --git a/tests/chez/chez009/run b/tests/chez/chez009/run index a74ec8ba5..0c148d582 100755 --- a/tests/chez/chez009/run +++ b/tests/chez/chez009/run @@ -1,3 +1,3 @@ -$1 --no-banner uni.idr < input +$1 --no-color --no-banner uni.idr < input rm -rf build diff --git a/tests/chez/chez010/run b/tests/chez/chez010/run index 2b7f55e95..474c51f2d 100755 --- a/tests/chez/chez010/run +++ b/tests/chez/chez010/run @@ -9,6 +9,6 @@ case `uname -s` in esac ${MAKE} all > /dev/null -$1 --no-banner CB.idr < input +$1 --no-color --no-banner CB.idr < input rm -rf build ${MAKE} clean > /dev/null diff --git a/tests/chez/chez011/run b/tests/chez/chez011/run index e4d1b228b..96a6c1e20 100644 --- a/tests/chez/chez011/run +++ b/tests/chez/chez011/run @@ -1,3 +1,3 @@ -$1 --no-banner bangs.idr < input +$1 --no-color --no-banner bangs.idr < input rm -rf build diff --git a/tests/chez/chez012/run b/tests/chez/chez012/run index 840535647..d562f949a 100755 --- a/tests/chez/chez012/run +++ b/tests/chez/chez012/run @@ -1,2 +1,2 @@ -$1 --no-banner array.idr < input +$1 --no-color --no-banner array.idr < input rm -rf build diff --git a/tests/chez/chez013/run b/tests/chez/chez013/run index 0ce0a1119..9fd325b65 100755 --- a/tests/chez/chez013/run +++ b/tests/chez/chez013/run @@ -9,6 +9,6 @@ case `uname -s` in esac ${MAKE} all > /dev/null -$1 --no-banner Struct.idr < input +$1 --no-color --no-banner Struct.idr < input rm -rf build ${MAKE} clean > /dev/null diff --git a/tests/chez/chez014/run b/tests/chez/chez014/run index 7d1b656f3..8e32d5b46 100755 --- a/tests/chez/chez014/run +++ b/tests/chez/chez014/run @@ -1,3 +1,3 @@ -$1 --no-banner -p network Echo.idr < input +$1 --no-color --no-banner -p network Echo.idr < input rm -rf build diff --git a/tests/chez/chez015/run b/tests/chez/chez015/run index 4d8a58ff6..8c1099fa1 100755 --- a/tests/chez/chez015/run +++ b/tests/chez/chez015/run @@ -1,3 +1,3 @@ -$1 --no-banner Numbers.idr < input +$1 --no-color --no-banner Numbers.idr < input rm -rf build diff --git a/tests/chez/chez016/run b/tests/chez/chez016/run index 15bfe1713..c06581881 100755 --- a/tests/chez/chez016/run +++ b/tests/chez/chez016/run @@ -16,5 +16,5 @@ IDRIS2_EXEC="$(basename "$1")" cd "folder with spaces" || exit -"$IDRIS2_DIR/$IDRIS2_EXEC" --no-banner Main.idr < ../input +"$IDRIS2_DIR/$IDRIS2_EXEC" --no-color --no-banner Main.idr < ../input rm -rf build diff --git a/tests/chez/chez017/run b/tests/chez/chez017/run index 7d0c0da1b..943d88bed 100755 --- a/tests/chez/chez017/run +++ b/tests/chez/chez017/run @@ -1,4 +1,4 @@ ./gen_expected.sh -$1 --no-banner dir.idr < input +$1 --no-color --no-banner dir.idr < input cat testdir/test.txt rm -rf build testdir diff --git a/tests/chez/chez018/run b/tests/chez/chez018/run index 1ad3ee2ac..0754dcf3d 100755 --- a/tests/chez/chez018/run +++ b/tests/chez/chez018/run @@ -1,3 +1,3 @@ -$1 --no-banner File.idr < input +$1 --no-color --no-banner File.idr < input rm -rf build testout.txt diff --git a/tests/chez/chez019/run b/tests/chez/chez019/run index ca359b28f..95a0c7295 100755 --- a/tests/chez/chez019/run +++ b/tests/chez/chez019/run @@ -1,3 +1,3 @@ -$1 --no-banner partial.idr < input +$1 --no-color --no-banner partial.idr < input rm -rf build testout.txt diff --git a/tests/chez/chez020/run b/tests/chez/chez020/run index 482adba57..aaa1f95bb 100644 --- a/tests/chez/chez020/run +++ b/tests/chez/chez020/run @@ -1,3 +1,3 @@ -POPEN_CMD="$1 --version" $1 --no-banner Popen.idr < input +POPEN_CMD="$1 --version" $1 --no-color --no-banner Popen.idr < input rm -rf build diff --git a/tests/chez/chez021/run b/tests/chez/chez021/run index 8a38cd689..1ddbf249f 100644 --- a/tests/chez/chez021/run +++ b/tests/chez/chez021/run @@ -1,3 +1,3 @@ -$1 --no-banner Bits.idr < input +$1 --no-color --no-banner Bits.idr < input rm -rf build diff --git a/tests/chez/chez022/run b/tests/chez/chez022/run index d422196d9..32c18634e 100755 --- a/tests/chez/chez022/run +++ b/tests/chez/chez022/run @@ -9,6 +9,6 @@ case `uname -s` in esac ${MAKE} all > /dev/null -$1 --no-banner usealloc.idr < input +$1 --no-color --no-banner usealloc.idr < input rm -rf build ${MAKE} clean > /dev/null diff --git a/tests/chez/chez023/run b/tests/chez/chez023/run index a04a0bfc0..6dd14b632 100644 --- a/tests/chez/chez023/run +++ b/tests/chez/chez023/run @@ -1,3 +1,3 @@ -$1 --no-banner File.idr < input +$1 --no-color --no-banner File.idr < input rm -rf build test.txt diff --git a/tests/chez/chez024/run b/tests/chez/chez024/run index 5f8729e95..7a7ab1a0a 100644 --- a/tests/chez/chez024/run +++ b/tests/chez/chez024/run @@ -1,3 +1,3 @@ -$1 --no-banner Envy.idr < input +$1 --no-color --no-banner Envy.idr < input rm -rf build diff --git a/tests/chez/chez025/run b/tests/chez/chez025/run index de7d06ee0..9700a7d88 100755 --- a/tests/chez/chez025/run +++ b/tests/chez/chez025/run @@ -1,3 +1,3 @@ -$1 --no-banner runst.idr < input +$1 --no-color --no-banner runst.idr < input rm -rf build diff --git a/tests/chez/chez026/dummy.ipkg b/tests/chez/chez026/dummy.ipkg index ab454bea6..072d62288 100644 --- a/tests/chez/chez026/dummy.ipkg +++ b/tests/chez/chez026/dummy.ipkg @@ -10,6 +10,7 @@ modules = Dummy main = Dummy executable = check_dir +opts = "--no-color" builddir = "custom_build" outputdir = "custom_output" diff --git a/tests/chez/chez027/run b/tests/chez/chez027/run index e9dffeb09..b326658e1 100644 --- a/tests/chez/chez027/run +++ b/tests/chez/chez027/run @@ -1,3 +1,3 @@ -$1 --no-banner -p contrib StringParser.idr < input +$1 --no-color --no-banner -p contrib StringParser.idr < input rm -rf build diff --git a/tests/chez/reg001/run b/tests/chez/reg001/run index 7f4525409..4ce1d5369 100755 --- a/tests/chez/reg001/run +++ b/tests/chez/reg001/run @@ -1,3 +1,3 @@ -$1 numbers.idr -x main +$1 --no-color numbers.idr -x main rm -rf build diff --git a/tests/ideMode/ideMode001/run b/tests/ideMode/ideMode001/run index 86bdf7144..6d01c177f 100755 --- a/tests/ideMode/ideMode001/run +++ b/tests/ideMode/ideMode001/run @@ -1,3 +1,3 @@ -$1 --ide-mode < input +$1 --no-color --ide-mode < input rm -rf build diff --git a/tests/ideMode/ideMode002/run b/tests/ideMode/ideMode002/run index eb8ec9618..bc4837c7a 100755 --- a/tests/ideMode/ideMode002/run +++ b/tests/ideMode/ideMode002/run @@ -1,4 +1,4 @@ -$1 --version | awk '{print $4}' | ./gen_expected.sh -$1 --ide-mode < input +$1 --no-color --version | awk '{print $4}' | ./gen_expected.sh +$1 --no-color --ide-mode < input rm -rf build diff --git a/tests/ideMode/ideMode003/run b/tests/ideMode/ideMode003/run index 86bdf7144..6d01c177f 100755 --- a/tests/ideMode/ideMode003/run +++ b/tests/ideMode/ideMode003/run @@ -1,3 +1,3 @@ -$1 --ide-mode < input +$1 --no-color --ide-mode < input rm -rf build diff --git a/tests/idris2/api001/run b/tests/idris2/api001/run index a99a49367..c833d2dc0 100644 --- a/tests/idris2/api001/run +++ b/tests/idris2/api001/run @@ -1,3 +1,3 @@ -$1 --no-banner -p idris2 -p contrib -p network LazyCodegen.idr -o lazy-idris2 > /dev/null -./build/exec/lazy-idris2 --no-banner --cg lazy Hello.idr -o hello -rm -rf build \ No newline at end of file +$1 --no-color --no-banner -p idris2 -p contrib -p network LazyCodegen.idr -o lazy-idris2 > /dev/null +./build/exec/lazy-idris2 --no-color --no-banner --cg lazy Hello.idr -o hello +rm -rf build diff --git a/tests/idris2/basic001/expected b/tests/idris2/basic001/expected index 3d5ae9dec..566ef5c5b 100644 --- a/tests/idris2/basic001/expected +++ b/tests/idris2/basic001/expected @@ -1,11 +1,11 @@ 1/1: Building Vect (Vect.idr) Main> Main> Cons (S Z) (Cons (S (S Z)) []) : Vect (S (S Z)) Nat -Main> (interactive):1:28--1:51:When unifying Vect (S (S Z)) Nat and Vect (S Z) Nat -Mismatch between: - S Z -and - Z -at: +Main> Error: When unifying Vect (S (S Z)) Nat and Vect (S Z) Nat. +Mismatch between: S Z and Z. + +(interactive):1:28--1:51 + | 1 | zipWith plus (Cons Z Nil) (Cons (S Z) (Cons Z Nil)) - ^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^ + Main> Bye for now! diff --git a/tests/idris2/basic001/run b/tests/idris2/basic001/run index 2dd78c31f..c9a705c59 100755 --- a/tests/idris2/basic001/run +++ b/tests/idris2/basic001/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude Vect.idr < input +$1 --no-color --no-banner --no-prelude Vect.idr < input rm -rf build diff --git a/tests/idris2/basic002/run b/tests/idris2/basic002/run index 039d5565e..a550140c1 100755 --- a/tests/idris2/basic002/run +++ b/tests/idris2/basic002/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude Do.idr < input +$1 --no-color --no-banner --no-prelude Do.idr < input rm -rf build diff --git a/tests/idris2/basic003/expected b/tests/idris2/basic003/expected index 10dd418e2..ef2d4aa3b 100644 --- a/tests/idris2/basic003/expected +++ b/tests/idris2/basic003/expected @@ -1,12 +1,13 @@ 1/1: Building Ambig1 (Ambig1.idr) Main> Bye for now! 1/1: Building Ambig2 (Ambig2.idr) -Ambig2.idr:26:21--26:27:While processing right hand side -of keepUnique at Ambig2.idr:26:1--28:1: -Ambiguous elaboration at: - 26 | keepUnique {b} xs = toList (fromList xs) - ^^^^^^ -Possible correct results: +Error: While processing right hand side of keepUnique. Ambiguous elaboration. Possible results: Main.Set.toList ?arg Main.Vect.toList ?arg + +Ambig2.idr:26:21--26:27 + | + 26 | keepUnique {b} xs = toList (fromList xs) + | ^^^^^^ + Main> Bye for now! diff --git a/tests/idris2/basic003/run b/tests/idris2/basic003/run index 8d8d310a6..fe3b7cbce 100755 --- a/tests/idris2/basic003/run +++ b/tests/idris2/basic003/run @@ -1,4 +1,4 @@ -echo ':q' | $1 --no-banner --no-prelude Ambig1.idr -echo ':q' | $1 --no-banner --no-prelude Ambig2.idr +echo ':q' | $1 --no-color --no-banner --no-prelude Ambig1.idr +echo ':q' | $1 --no-color --no-banner --no-prelude Ambig2.idr rm -rf build diff --git a/tests/idris2/basic004/run b/tests/idris2/basic004/run index e5c44df5b..024be335f 100755 --- a/tests/idris2/basic004/run +++ b/tests/idris2/basic004/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude Wheres.idr < input +$1 --no-color --no-banner --no-prelude Wheres.idr < input rm -rf build diff --git a/tests/idris2/basic005/expected b/tests/idris2/basic005/expected index 6a7a83688..a5c2bf082 100644 --- a/tests/idris2/basic005/expected +++ b/tests/idris2/basic005/expected @@ -1,5 +1,9 @@ 1/1: Building NoInfer (NoInfer.idr) -NoInfer.idr:1:7--1:8:Unsolved holes: -Main.{_:1} introduced at NoInfer.idr:1:7--1:8 +Error: unsolved holes: +Main.{_:1} introduced at: +NoInfer.idr:1:7--1:8 + | + 1 | foo : ? -> Int + | ^ Main> Bye for now! diff --git a/tests/idris2/basic005/run b/tests/idris2/basic005/run index ddb70cfcb..7e69c6998 100755 --- a/tests/idris2/basic005/run +++ b/tests/idris2/basic005/run @@ -1,3 +1,3 @@ -echo ':q' | $1 --no-banner --no-prelude NoInfer.idr +echo ':q' | $1 --no-color --no-banner --no-prelude NoInfer.idr rm -rf build diff --git a/tests/idris2/basic006/run b/tests/idris2/basic006/run index ab3720d24..6189e1620 100755 --- a/tests/idris2/basic006/run +++ b/tests/idris2/basic006/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude PMLet.idr < input +$1 --no-color --no-banner --no-prelude PMLet.idr < input rm -rf build diff --git a/tests/idris2/basic007/run b/tests/idris2/basic007/run index f7e9afd5c..f5bfb9bca 100755 --- a/tests/idris2/basic007/run +++ b/tests/idris2/basic007/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude DoLocal.idr < input +$1 --no-color --no-banner --no-prelude DoLocal.idr < input rm -rf build diff --git a/tests/idris2/basic008/run b/tests/idris2/basic008/run index b4bfef215..79628de2f 100755 --- a/tests/idris2/basic008/run +++ b/tests/idris2/basic008/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude If.idr < input +$1 --no-color --no-banner --no-prelude If.idr < input rm -rf build diff --git a/tests/idris2/basic009/run b/tests/idris2/basic009/run index 4dda89815..6832ef631 100755 --- a/tests/idris2/basic009/run +++ b/tests/idris2/basic009/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude LetCase.idr < input +$1 --no-color --no-banner --no-prelude LetCase.idr < input rm -rf build diff --git a/tests/idris2/basic010/run b/tests/idris2/basic010/run index acc73cd27..ae4d6fe87 100755 --- a/tests/idris2/basic010/run +++ b/tests/idris2/basic010/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude Comp.idr < input +$1 --no-color --no-banner --no-prelude Comp.idr < input rm -rf build diff --git a/tests/idris2/basic011/expected b/tests/idris2/basic011/expected index 104dcb8c3..d5ecd029f 100644 --- a/tests/idris2/basic011/expected +++ b/tests/idris2/basic011/expected @@ -1,14 +1,17 @@ 1/1: Building Dots1 (Dots1.idr) 1/1: Building Dots2 (Dots2.idr) -Dots2.idr:2:7--2:8:While processing left hand side of foo at Dots2.idr:2:1--4:1: -Can't match on ?x [no locals in scope] (Non linear pattern variable) at: +Error: While processing left hand side of foo. Can't match on ?x [no locals in scope] (Non linear pattern variable). + +Dots2.idr:2:7--2:8 + | 2 | foo x x = x + x - ^ + | ^ + 1/1: Building Dots3 (Dots3.idr) -Dots3.idr:5:29--5:30:While processing left hand side -of addBaz at Dots3.idr:5:1--6:1: -Pattern variable z unifies with: - ?y [no locals in scope] -at: +Error: While processing left hand side of addBaz. Pattern variable z unifies with: ?y [no locals in scope]. + +Dots3.idr:5:29--5:30 + | 5 | addBaz (x + y) (AddThings x z) = x + y - ^ + | ^ + diff --git a/tests/idris2/basic011/run b/tests/idris2/basic011/run index 9d0c25092..ec9f9c5d2 100755 --- a/tests/idris2/basic011/run +++ b/tests/idris2/basic011/run @@ -1,5 +1,5 @@ -$1 --check Dots1.idr -$1 --check Dots2.idr -$1 --check Dots3.idr +$1 --no-color --check Dots1.idr +$1 --no-color --check Dots2.idr +$1 --no-color --check Dots3.idr rm -rf build diff --git a/tests/idris2/basic012/run b/tests/idris2/basic012/run index 056d37b60..16320c882 100755 --- a/tests/idris2/basic012/run +++ b/tests/idris2/basic012/run @@ -1,3 +1,3 @@ -$1 --check VIndex.idr +$1 --no-color --check VIndex.idr rm -rf build diff --git a/tests/idris2/basic013/run b/tests/idris2/basic013/run index 6fbbed4fe..36839db4e 100755 --- a/tests/idris2/basic013/run +++ b/tests/idris2/basic013/run @@ -1,3 +1,3 @@ -$1 --check Implicits.idr +$1 --no-color --check Implicits.idr rm -rf build diff --git a/tests/idris2/basic014/expected b/tests/idris2/basic014/expected index 0007e0cc9..7aced536e 100644 --- a/tests/idris2/basic014/expected +++ b/tests/idris2/basic014/expected @@ -1,11 +1,16 @@ 1/1: Building Rewrite (Rewrite.idr) -Rewrite.idr:15:25--15:57:While processing right hand side -of wrongCommutes at Rewrite.idr:15:1--17:1: -Rewriting by m + k = k + m did not change type S k + m = m + S k at: +Error: While processing right hand side of wrongCommutes. Rewriting by m + k = k + m did not change +type S k + m = m + S k. + +Rewrite.idr:15:25--15:57 + | 15 | wrongCommutes (S k) m = rewrite plusCommutes m k in ?bar - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Rewrite.idr:19:26--19:43:While processing right hand side -of wrongCommutes2 at Rewrite.idr:19:1--20:1: -Nat is not a rewrite rule type at: + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +Error: While processing right hand side of wrongCommutes2. Nat is not a rewrite rule type. + +Rewrite.idr:19:26--19:43 + | 19 | wrongCommutes2 (S k) m = rewrite m in ?bar - ^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^ + diff --git a/tests/idris2/basic014/run b/tests/idris2/basic014/run index 8f43cf56d..c6a578628 100755 --- a/tests/idris2/basic014/run +++ b/tests/idris2/basic014/run @@ -1,3 +1,3 @@ -$1 --check Rewrite.idr +$1 --no-color --check Rewrite.idr rm -rf build diff --git a/tests/idris2/basic015/run b/tests/idris2/basic015/run index 0b299827d..c53a7648a 100755 --- a/tests/idris2/basic015/run +++ b/tests/idris2/basic015/run @@ -1,3 +1,3 @@ -$1 --check George.idr +$1 --no-color --check George.idr rm -rf build diff --git a/tests/idris2/basic016/expected b/tests/idris2/basic016/expected index 33c6c296d..9325f5372 100644 --- a/tests/idris2/basic016/expected +++ b/tests/idris2/basic016/expected @@ -1,33 +1,27 @@ 1/1: Building Eta (Eta.idr) -Eta.idr:14:10--14:14:While processing right hand side -of etaBad at Eta.idr:14:1--15:1: -When -unifying \x => (\y => (MkTest ?_ ?_)) = \x => (\y => (MkTest ?_ ?_)) and MkTest = \x => (\y => (MkTest ?_ ?_)) -Mismatch between: - Nat -and - Integer -at: +Error: While processing right hand side of etaBad. When +unifying \x => (\y => (MkTest ?_ ?_)) = \x => (\y => (MkTest ?_ ?_)) and MkTest = \x => (\y => (MkTest ?_ ?_)). +Mismatch between: Nat and Int. + +Eta.idr:14:10--14:14 + | 14 | etaBad = Refl - ^^^^ + | ^^^^ + 1/1: Building Eta2 (Eta2.idr) -Eta2.idr:2:8--2:12:While processing right hand side -of test at Eta2.idr:2:1--4:1: -When unifying \x => (S ?_) = \x => (S ?_) and S = \x => (S ?_) -Mismatch between: - a -and - Nat -at: +Error: While processing right hand side of test. When unifying \x => (S ?_) = \x => (S ?_) and S = \x => (S ?_). +Mismatch between: a and Nat. + +Eta2.idr:2:8--2:12 + | 2 | test = Refl - ^^^^ -Eta2.idr:5:44--5:48:While processing right hand side -of test2 at Eta2.idr:5:1--6:1: -When unifying \x => (S ?_) = \x => (S ?_) and S = \x => (S ?_) -Mismatch between: - a -and - Nat -at: + | ^^^^ + +Error: While processing right hand side of test2. When unifying \x => (S ?_) = \x => (S ?_) and S = \x => (S ?_). +Mismatch between: a and Nat. + +Eta2.idr:5:44--5:48 + | 5 | test2 = {a : _} -> the (S = \x : a => S _) Refl - ^^^^ + | ^^^^ + diff --git a/tests/idris2/basic016/run b/tests/idris2/basic016/run index 0644ed6f1..a92aacb38 100755 --- a/tests/idris2/basic016/run +++ b/tests/idris2/basic016/run @@ -1,4 +1,4 @@ -$1 --check Eta.idr -$1 --check Eta2.idr +$1 --no-color --check Eta.idr +$1 --no-color --check Eta2.idr rm -rf build diff --git a/tests/idris2/basic017/run b/tests/idris2/basic017/run index fffd6fd05..fac2cae83 100755 --- a/tests/idris2/basic017/run +++ b/tests/idris2/basic017/run @@ -1,3 +1,3 @@ -$1 --no-banner CaseInf.idr < input +$1 --no-color --no-banner CaseInf.idr < input rm -rf build diff --git a/tests/idris2/basic018/expected b/tests/idris2/basic018/expected index c76ae3fe3..199d16961 100644 --- a/tests/idris2/basic018/expected +++ b/tests/idris2/basic018/expected @@ -1,6 +1,8 @@ 1/1: Building Fin (Fin.idr) -Fin.idr:34:7--34:8:While processing right hand side -of bar at Fin.idr:34:1--36:1: -Can't find an implementation for IsJust (integerToFin 8 5) at: +Error: While processing right hand side of bar. Can't find an implementation for IsJust (integerToFin 8 5). + +Fin.idr:34:7--34:8 + | 34 | bar = 8 - ^ + | ^ + diff --git a/tests/idris2/basic018/run b/tests/idris2/basic018/run index b7e07ce81..8c9d06a4e 100755 --- a/tests/idris2/basic018/run +++ b/tests/idris2/basic018/run @@ -1,3 +1,3 @@ -$1 --check Fin.idr +$1 --no-color --check Fin.idr rm -rf build diff --git a/tests/idris2/basic019/run b/tests/idris2/basic019/run index 289e67c2d..6ccb4e625 100755 --- a/tests/idris2/basic019/run +++ b/tests/idris2/basic019/run @@ -1,3 +1,3 @@ -$1 --no-banner CaseBlock.idr < input +$1 --no-color --no-banner CaseBlock.idr < input rm -rf build diff --git a/tests/idris2/basic020/run b/tests/idris2/basic020/run index fa0bf9c01..02fc956f0 100755 --- a/tests/idris2/basic020/run +++ b/tests/idris2/basic020/run @@ -1,3 +1,3 @@ -$1 --no-banner Mut.idr < input +$1 --no-color --no-banner Mut.idr < input rm -rf build diff --git a/tests/idris2/basic021/run b/tests/idris2/basic021/run index b5a979300..722000b4c 100755 --- a/tests/idris2/basic021/run +++ b/tests/idris2/basic021/run @@ -1,3 +1,3 @@ -$1 --no-banner CaseDep.idr < input +$1 --no-color --no-banner CaseDep.idr < input rm -rf build diff --git a/tests/idris2/basic022/expected b/tests/idris2/basic022/expected index 4313d93a6..f9cabac9e 100644 --- a/tests/idris2/basic022/expected +++ b/tests/idris2/basic022/expected @@ -1,13 +1,17 @@ 1/1: Building Erase (Erase.idr) -Erase.idr:5:5--5:10:While processing left hand side -of bad at Erase.idr:5:1--6:1: -Can't match on False (Erased argument) at: +Error: While processing left hand side of bad. Can't match on False (Erased argument). + +Erase.idr:5:5--5:10 + | 5 | bad False = True - ^^^^^ -Erase.idr:19:18--19:21:While processing left hand side -of minusBad at Erase.idr:19:1--20:1: -Can't match on LeZ (Erased argument) at: + | ^^^^^ + +Error: While processing left hand side of minusBad. Can't match on LeZ (Erased argument). + +Erase.idr:19:18--19:21 + | 19 | minusBad (S k) Z LeZ = S k - ^^^ + | ^^^ + Main> \m => minus (S (S m)) m prf Main> Bye for now! diff --git a/tests/idris2/basic022/run b/tests/idris2/basic022/run index 7733a673d..1f9301788 100755 --- a/tests/idris2/basic022/run +++ b/tests/idris2/basic022/run @@ -1,3 +1,3 @@ -$1 --no-banner Erase.idr < input +$1 --no-color --no-banner Erase.idr < input rm -rf build diff --git a/tests/idris2/basic023/run b/tests/idris2/basic023/run index c2f0c3089..8e787d1e1 100755 --- a/tests/idris2/basic023/run +++ b/tests/idris2/basic023/run @@ -1,3 +1,3 @@ -$1 --no-banner Params.idr < input +$1 --no-color --no-banner Params.idr < input rm -rf build diff --git a/tests/idris2/basic024/run b/tests/idris2/basic024/run index e4f4b94e8..a7008e9e8 100755 --- a/tests/idris2/basic024/run +++ b/tests/idris2/basic024/run @@ -1,3 +1,3 @@ -$1 --no-banner PatLam.idr < input +$1 --no-color --no-banner PatLam.idr < input rm -rf build diff --git a/tests/idris2/basic025/run b/tests/idris2/basic025/run index cf575737b..1852e9c94 100755 --- a/tests/idris2/basic025/run +++ b/tests/idris2/basic025/run @@ -1,3 +1,3 @@ -$1 --no-banner < input +$1 --no-color --no-banner < input rm -rf build diff --git a/tests/idris2/basic026/run b/tests/idris2/basic026/run index e87219263..6e112c3c7 100755 --- a/tests/idris2/basic026/run +++ b/tests/idris2/basic026/run @@ -1,3 +1,3 @@ -$1 --check Erl.idr +$1 --no-color --check Erl.idr rm -rf build diff --git a/tests/idris2/basic027/run b/tests/idris2/basic027/run index 2f5386681..ae907e9d4 100755 --- a/tests/idris2/basic027/run +++ b/tests/idris2/basic027/run @@ -1,3 +1,3 @@ -$1 --check Temp.idr +$1 --no-color --check Temp.idr rm -rf build diff --git a/tests/idris2/basic028/run b/tests/idris2/basic028/run index fba69dc39..70b1b77e8 100755 --- a/tests/idris2/basic028/run +++ b/tests/idris2/basic028/run @@ -1,5 +1,5 @@ unset IDRIS2_PATH -$1 --no-banner --no-prelude < input +$1 --no-color --no-banner --no-prelude < input rm -rf build diff --git a/tests/idris2/basic029/run b/tests/idris2/basic029/run index c2f0c3089..8e787d1e1 100644 --- a/tests/idris2/basic029/run +++ b/tests/idris2/basic029/run @@ -1,3 +1,3 @@ -$1 --no-banner Params.idr < input +$1 --no-color --no-banner Params.idr < input rm -rf build diff --git a/tests/idris2/basic030/expected b/tests/idris2/basic030/expected index e3f289b31..e42a6c80a 100644 --- a/tests/idris2/basic030/expected +++ b/tests/idris2/basic030/expected @@ -1,11 +1,9 @@ 1/1: Building arity (arity.idr) -arity.idr:4:16--4:21:While processing right hand side -of foo at arity.idr:4:1--7:1: -When unifying (1 _ : Nat) -> MyN and MyN -Mismatch between: - (1 _ : Nat) -> MyN -and - MyN -at: +Error: While processing right hand side of foo. When unifying (1 _ : Nat) -> MyN and MyN. +Mismatch between: (1 _ : Nat) -> MyN and MyN. + +arity.idr:4:16--4:21 + | 4 | foo x y = case MkN x of - ^^^^^ + | ^^^^^ + diff --git a/tests/idris2/basic030/run b/tests/idris2/basic030/run index 2828781d9..195109118 100644 --- a/tests/idris2/basic030/run +++ b/tests/idris2/basic030/run @@ -1,3 +1,3 @@ -$1 --check arity.idr +$1 --no-color --check arity.idr rm -rf build diff --git a/tests/idris2/basic031/expected b/tests/idris2/basic031/expected index d3f2beccb..7f553fbd4 100644 --- a/tests/idris2/basic031/expected +++ b/tests/idris2/basic031/expected @@ -1,6 +1,8 @@ 1/1: Building erased (erased.idr) -erased.idr:7:17--7:21:While processing left hand side -of nameOf at erased.idr:7:1--8:1: -Can't match on Bool (Erased argument) at: +Error: While processing left hand side of nameOf. Can't match on Bool (Erased argument). + +erased.idr:7:17--7:21 + | 7 | nameOf (MyMaybe Bool) = "MyMaybe Bool" - ^^^^ + | ^^^^ + diff --git a/tests/idris2/basic031/run b/tests/idris2/basic031/run index 4c45e9dcb..d140ddc79 100644 --- a/tests/idris2/basic031/run +++ b/tests/idris2/basic031/run @@ -1,3 +1,3 @@ -$1 --check erased.idr +$1 --no-color --check erased.idr rm -rf build diff --git a/tests/idris2/basic032/run b/tests/idris2/basic032/run index 9765ac18d..990ff8f3d 100755 --- a/tests/idris2/basic032/run +++ b/tests/idris2/basic032/run @@ -1,3 +1,3 @@ -$1 --no-banner Idiom.idr < input +$1 --no-color --no-banner Idiom.idr < input rm -rf build diff --git a/tests/idris2/basic033/expected b/tests/idris2/basic033/expected index f853f84bf..598d2c453 100644 --- a/tests/idris2/basic033/expected +++ b/tests/idris2/basic033/expected @@ -1,11 +1,15 @@ 1/1: Building unboundimps (unboundimps.idr) -unboundimps.idr:18:11--18:13:While processing type -of len' at unboundimps.idr:18:1--18:20: -Undefined name xs at: +Error: While processing type of len'. Undefined name xs. + +unboundimps.idr:18:11--18:13 + | 18 | len': Env xs -> Nat - ^^ -unboundimps.idr:19:16--19:17:While processing type -of append' at unboundimps.idr:19:1--19:49: -Undefined name n at: + | ^^ + +Error: While processing type of append'. Undefined name n. + +unboundimps.idr:19:16--19:17 + | 19 | append' : Vect n a -> Vect m a -> Vect (n + m) a - ^ + | ^ + diff --git a/tests/idris2/basic033/run b/tests/idris2/basic033/run index 4a1a4d211..b57d8171a 100644 --- a/tests/idris2/basic033/run +++ b/tests/idris2/basic033/run @@ -1,3 +1,3 @@ -$1 --check unboundimps.idr +$1 --no-color --check unboundimps.idr rm -rf build diff --git a/tests/idris2/basic034/expected b/tests/idris2/basic034/expected index f16dd5c59..89a2cb065 100644 --- a/tests/idris2/basic034/expected +++ b/tests/idris2/basic034/expected @@ -1,11 +1,9 @@ 1/1: Building lets (lets.idr) -lets.idr:22:39--22:40:While processing right hand side -of dolet2 at lets.idr:21:1--26:1: -When unifying Maybe Int and Maybe String -Mismatch between: - Int -and - String -at: +Error: While processing right hand side of dolet2. When unifying Maybe Int and Maybe String. +Mismatch between: Int and String. + +lets.idr:22:39--22:40 + | 22 | = do let Just x' : Maybe String = x - ^ + | ^ + diff --git a/tests/idris2/basic034/run b/tests/idris2/basic034/run index 29fbe0d33..40dc39dce 100644 --- a/tests/idris2/basic034/run +++ b/tests/idris2/basic034/run @@ -1,3 +1,3 @@ -$1 --check lets.idr +$1 --no-color --check lets.idr rm -rf build diff --git a/tests/idris2/basic035/run b/tests/idris2/basic035/run index 751bebdcf..3aa97e108 100755 --- a/tests/idris2/basic035/run +++ b/tests/idris2/basic035/run @@ -1,3 +1,3 @@ -$1 --no-banner using.idr < input +$1 --no-color --no-banner using.idr < input rm -rf build diff --git a/tests/idris2/basic036/run b/tests/idris2/basic036/run index 6aeb8643a..1b161b0de 100755 --- a/tests/idris2/basic036/run +++ b/tests/idris2/basic036/run @@ -1,3 +1,3 @@ -$1 --no-banner defimp.idr < input +$1 --no-color --no-banner defimp.idr < input rm -rf build diff --git a/tests/idris2/basic037/run b/tests/idris2/basic037/run index 08d4f6845..fab6ebf4a 100644 --- a/tests/idris2/basic037/run +++ b/tests/idris2/basic037/run @@ -1,4 +1,4 @@ -echo ':q' | $1 --no-banner --no-prelude Comments.idr -echo ':q' | $1 --no-banner Issue279.idr +echo ':q' | $1 --no-color --no-banner --no-prelude Comments.idr +echo ':q' | $1 --no-color --no-banner Issue279.idr -rm -rf build \ No newline at end of file +rm -rf build diff --git a/tests/idris2/basic038/run b/tests/idris2/basic038/run index 9363d3429..8225c1a14 100644 --- a/tests/idris2/basic038/run +++ b/tests/idris2/basic038/run @@ -1,3 +1,3 @@ -$1 --no-banner Resugar.idr < input +$1 --no-color --no-banner Resugar.idr < input -rm -rf build \ No newline at end of file +rm -rf build diff --git a/tests/idris2/basic039/run b/tests/idris2/basic039/run index fe350f886..66364c742 100755 --- a/tests/idris2/basic039/run +++ b/tests/idris2/basic039/run @@ -1,3 +1,3 @@ -$1 --no-banner Main.idr < input +$1 --no-color --no-banner Main.idr < input rm -rf build diff --git a/tests/idris2/basic040/run b/tests/idris2/basic040/run index ba049685e..5cfff0487 100755 --- a/tests/idris2/basic040/run +++ b/tests/idris2/basic040/run @@ -1,3 +1,3 @@ -echo ":q" | $1 --no-banner Default.idr +echo ":q" | $1 --no-color --no-banner Default.idr rm -rf build diff --git a/tests/idris2/basic041/run b/tests/idris2/basic041/run index 24a0859d4..3ae26bc29 100755 --- a/tests/idris2/basic041/run +++ b/tests/idris2/basic041/run @@ -1,3 +1,3 @@ -$1 --check QDo.idr +$1 --no-color --check QDo.idr rm -rf build diff --git a/tests/idris2/coverage001/run b/tests/idris2/coverage001/run index 7a6b014fb..202730ee6 100755 --- a/tests/idris2/coverage001/run +++ b/tests/idris2/coverage001/run @@ -1,3 +1,3 @@ -$1 --no-banner Vect.idr < input +$1 --no-color --no-banner Vect.idr < input rm -rf build diff --git a/tests/idris2/coverage002/run b/tests/idris2/coverage002/run index 7a6b014fb..202730ee6 100755 --- a/tests/idris2/coverage002/run +++ b/tests/idris2/coverage002/run @@ -1,3 +1,3 @@ -$1 --no-banner Vect.idr < input +$1 --no-color --no-banner Vect.idr < input rm -rf build diff --git a/tests/idris2/coverage003/expected b/tests/idris2/coverage003/expected index 2ddd72086..c26744b09 100644 --- a/tests/idris2/coverage003/expected +++ b/tests/idris2/coverage003/expected @@ -1,9 +1,11 @@ 1/1: Building Cover (Cover.idr) -Cover.idr:16:1--16:7:While processing left hand side -of badBar at Cover.idr:16:1--17:1: -Can't match on 0 as it has a polymorphic type at: +Error: While processing left hand side of badBar. Can't match on 0 as it has a polymorphic type. + +Cover.idr:16:1--16:7 + | 16 | badBar Z = Z - ^^^^^^ + | ^^^^^^ + Main> Main.foo: foo (0, S _) foo (S _, _) diff --git a/tests/idris2/coverage003/run b/tests/idris2/coverage003/run index e3632d9b2..0c52ac349 100755 --- a/tests/idris2/coverage003/run +++ b/tests/idris2/coverage003/run @@ -1,3 +1,3 @@ -$1 --no-banner Cover.idr < input +$1 --no-color --no-banner Cover.idr < input rm -rf build diff --git a/tests/idris2/coverage004/expected b/tests/idris2/coverage004/expected index 8ea7a6b61..f65ec8de8 100644 --- a/tests/idris2/coverage004/expected +++ b/tests/idris2/coverage004/expected @@ -1,9 +1,11 @@ 1/1: Building Cover (Cover.idr) -Cover.idr:14:1--14:4:While processing left hand side -of bad at Cover.idr:14:1--15:1: -Can't match on Just (fromInteger 0) as it has a polymorphic type at: +Error: While processing left hand side of bad. Can't match on Just (fromInteger 0) as it has a polymorphic type. + +Cover.idr:14:1--14:4 + | 14 | bad (Just 0) _ = False - ^^^ + | ^^^ + Main> Main.okay: okay (S _) IsNat okay False IsBool diff --git a/tests/idris2/coverage004/run b/tests/idris2/coverage004/run index e3632d9b2..0c52ac349 100755 --- a/tests/idris2/coverage004/run +++ b/tests/idris2/coverage004/run @@ -1,3 +1,3 @@ -$1 --no-banner Cover.idr < input +$1 --no-color --no-banner Cover.idr < input rm -rf build diff --git a/tests/idris2/coverage005/run b/tests/idris2/coverage005/run index e3632d9b2..0c52ac349 100755 --- a/tests/idris2/coverage005/run +++ b/tests/idris2/coverage005/run @@ -1,3 +1,3 @@ -$1 --no-banner Cover.idr < input +$1 --no-color --no-banner Cover.idr < input rm -rf build diff --git a/tests/idris2/coverage006/run b/tests/idris2/coverage006/run index feeae1a10..423937d80 100755 --- a/tests/idris2/coverage006/run +++ b/tests/idris2/coverage006/run @@ -1,3 +1,3 @@ -$1 --no-banner foobar.idr < input +$1 --no-color --no-banner foobar.idr < input rm -rf build diff --git a/tests/idris2/coverage007/expected b/tests/idris2/coverage007/expected index 2376a7ac9..f4b4b6c93 100644 --- a/tests/idris2/coverage007/expected +++ b/tests/idris2/coverage007/expected @@ -1,7 +1,15 @@ 1/1: Building eq (eq.idr) -eq.idr:27:1--27:23:badeq x y p is not a valid impossible case at: +Error: badeq x y p is not a valid impossible case. + +eq.idr:27:1--27:23 + | 27 | badeq x y p impossible - ^^^^^^^^^^^^^^^^^^^^^^ -eq.idr:30:1--30:26:badeqL xs ys p is not a valid impossible case at: + | ^^^^^^^^^^^^^^^^^^^^^^ + +Error: badeqL xs ys p is not a valid impossible case. + +eq.idr:30:1--30:26 + | 30 | badeqL xs ys p impossible - ^^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^^^ + diff --git a/tests/idris2/coverage007/run b/tests/idris2/coverage007/run index 25cac64e6..4fe9b9f33 100755 --- a/tests/idris2/coverage007/run +++ b/tests/idris2/coverage007/run @@ -1,3 +1,3 @@ -$1 --no-banner eq.idr --check +$1 --no-color --no-banner eq.idr --check rm -rf build diff --git a/tests/idris2/coverage008/run b/tests/idris2/coverage008/run index 0820e9f21..a14139e9f 100755 --- a/tests/idris2/coverage008/run +++ b/tests/idris2/coverage008/run @@ -1,3 +1,3 @@ -$1 --no-banner wcov.idr < input +$1 --no-color --no-banner wcov.idr < input rm -rf build diff --git a/tests/idris2/coverage009/expected b/tests/idris2/coverage009/expected index 3cf96e48e..533bf4b87 100644 --- a/tests/idris2/coverage009/expected +++ b/tests/idris2/coverage009/expected @@ -1,3 +1,15 @@ 1/1: Building unreachable (unreachable.idr) -unreachable.idr:3:1--3:17:Warning: unreachable clause: foo Nothing True -unreachable.idr:5:1--5:18:Warning: unreachable clause: foo Nothing False +Warning: Unreachable clause: foo Nothing True + +unreachable.idr:3:1--3:17 + | + 3 | foo Nothing True = 94 + | ^^^^^^^^^^^^^^^^ + +Warning: Unreachable clause: foo Nothing False + +unreachable.idr:5:1--5:18 + | + 5 | foo Nothing False = 42 + | ^^^^^^^^^^^^^^^^^ + diff --git a/tests/idris2/coverage009/run b/tests/idris2/coverage009/run index 84e1ec928..7239c61b6 100755 --- a/tests/idris2/coverage009/run +++ b/tests/idris2/coverage009/run @@ -1,3 +1,3 @@ -$1 --check unreachable.idr +$1 --no-color --check unreachable.idr rm -rf build diff --git a/tests/idris2/coverage010/expected b/tests/idris2/coverage010/expected index 8ad6d98f7..76c13ed5e 100644 --- a/tests/idris2/coverage010/expected +++ b/tests/idris2/coverage010/expected @@ -1,5 +1,8 @@ 1/1: Building casetot (casetot.idr) -casetot.idr:12:1--13:1:main is not covering at: +Error: main is not covering. + +casetot.idr:12:1--13:1 12 | main : IO () 13 | main = do + Calls non covering function Main.case block in case block in main diff --git a/tests/idris2/coverage010/run b/tests/idris2/coverage010/run index 6074c1095..a41c0ac7d 100755 --- a/tests/idris2/coverage010/run +++ b/tests/idris2/coverage010/run @@ -1,3 +1,3 @@ -$1 --check casetot.idr +$1 --no-color --check casetot.idr rm -rf build diff --git a/tests/idris2/docs001/expected b/tests/idris2/docs001/expected index ff51ae617..0da4bdadd 100644 --- a/tests/idris2/docs001/expected +++ b/tests/idris2/docs001/expected @@ -12,7 +12,6 @@ Z : Nat Zero. S : (1 _ : Nat) -> Nat Successor. - Main> Prelude.List : (1 _ : Type) -> Type Generic lists. @@ -20,7 +19,6 @@ Constructors: Nil : List a Empty list :: : (1 _ : a) -> (1 _ : List a) -> List a - Main> Prelude.Show : Type -> Type Things that have a canonical `String` representation. Parameters: ty @@ -61,7 +59,6 @@ Implementations: Show a => Show (List a) Show a => Show (Maybe a) (Show a, Show b) => Show (Either a b) - Main> Prelude.show : Show ty => ty -> String Convert a value to its `String` representation. @ x the value to convert @@ -82,5 +79,4 @@ Implementations: Monad Maybe Monad (Either e) Monad List - Main> Bye for now! diff --git a/tests/idris2/docs001/run b/tests/idris2/docs001/run index cf575737b..1852e9c94 100755 --- a/tests/idris2/docs001/run +++ b/tests/idris2/docs001/run @@ -1,3 +1,3 @@ -$1 --no-banner < input +$1 --no-color --no-banner < input rm -rf build diff --git a/tests/idris2/docs002/run b/tests/idris2/docs002/run index f8e6ab97a..fe442deec 100755 --- a/tests/idris2/docs002/run +++ b/tests/idris2/docs002/run @@ -1,3 +1,3 @@ -$1 --no-banner Doc.idr < input +$1 --no-color --no-banner Doc.idr < input rm -rf build diff --git a/tests/idris2/error001/expected b/tests/idris2/error001/expected index 7ed9cfc29..89f21d34a 100644 --- a/tests/idris2/error001/expected +++ b/tests/idris2/error001/expected @@ -1,11 +1,9 @@ 1/1: Building Error (Error.idr) -Error.idr:6:19--6:20:While processing right hand side -of wrong at Error.idr:6:1--7:1: -When unifying a and Vect ?k ?a -Mismatch between: - a -and - Vect ?k ?a -at: +Error: While processing right hand side of wrong. When unifying a and Vect ?k ?a. +Mismatch between: a and Vect ?k ?a. + +Error.idr:6:19--6:20 + | 6 | wrong x xs = x :: x - ^ + | ^ + diff --git a/tests/idris2/error001/run b/tests/idris2/error001/run index 61fddcc79..f202ad20d 100755 --- a/tests/idris2/error001/run +++ b/tests/idris2/error001/run @@ -1,3 +1,3 @@ -$1 --check Error.idr +$1 --no-color --check Error.idr rm -rf build diff --git a/tests/idris2/error002/expected b/tests/idris2/error002/expected index 7f17ec159..ef296b495 100644 --- a/tests/idris2/error002/expected +++ b/tests/idris2/error002/expected @@ -1,6 +1,8 @@ 1/1: Building Error (Error.idr) -Error.idr:6:17--6:19:While processing right hand side -of wrong at Error.idr:6:1--7:1: -Undefined name ys at: +Error: While processing right hand side of wrong. Undefined name ys. + +Error.idr:6:17--6:19 + | 6 | wrong xs = x :: ys - ^^ + | ^^ + diff --git a/tests/idris2/error002/run b/tests/idris2/error002/run index 61fddcc79..f202ad20d 100755 --- a/tests/idris2/error002/run +++ b/tests/idris2/error002/run @@ -1,3 +1,3 @@ -$1 --check Error.idr +$1 --no-color --check Error.idr rm -rf build diff --git a/tests/idris2/error003/expected b/tests/idris2/error003/expected index efa0f2fc3..7e21b1fe9 100644 --- a/tests/idris2/error003/expected +++ b/tests/idris2/error003/expected @@ -1,31 +1,26 @@ 1/1: Building Error (Error.idr) -Error.idr:12:18--12:19:While processing right hand side -of wrong at Error.idr:12:1--13:1: -Sorry, I can't find any elaboration which works. All errors: -If Main.length: When unifying Nat and Vect ?n ?a -Mismatch between: - Nat -and - Vect ?n ?a -at: - 12 | wrong x = length x - ^ +Error: While processing right hand side of wrong. Sorry, I can't find any elaboration which works. All errors: +If Main.length: When unifying Nat and Vect ?n ?a. +Mismatch between: Nat and Vect ?n ?a. -If Prelude.List.length: When unifying Nat and List ?a -Mismatch between: - Nat -and - List ?a -at: +Error.idr:12:18--12:19 + | 12 | wrong x = length x - ^ + | ^ -If Prelude.Strings.length: When unifying Nat and String -Mismatch between: - Nat -and - String -at: +If Prelude.List.length: When unifying Nat and List ?a. +Mismatch between: Nat and List ?a. + +Error.idr:12:18--12:19 + | 12 | wrong x = length x - ^ + | ^ + +If Prelude.Strings.length: When unifying Nat and String. +Mismatch between: Nat and String. + +Error.idr:12:18--12:19 + | + 12 | wrong x = length x + | ^ diff --git a/tests/idris2/error003/run b/tests/idris2/error003/run index 61fddcc79..f202ad20d 100755 --- a/tests/idris2/error003/run +++ b/tests/idris2/error003/run @@ -1,3 +1,3 @@ -$1 --check Error.idr +$1 --no-color --check Error.idr rm -rf build diff --git a/tests/idris2/error004/expected b/tests/idris2/error004/expected index 0a47f361d..7bde871f5 100644 --- a/tests/idris2/error004/expected +++ b/tests/idris2/error004/expected @@ -1,25 +1,27 @@ 1/1: Building Error1 (Error1.idr) -Error1.idr:8:9--9:1:While processing right hand side -of wrong at Error1.idr:8:1--9:1: -Can't find an implementation for Show (Vect 4 Integer) at: +Error: While processing right hand side of wrong. Can't find an implementation for Show (Vect 4 Int). + +Error1.idr:8:9--9:1 8 | wrong = show (the (Vect _ _) [1,2,3,4]) + 1/1: Building Error2 (Error2.idr) -Error2.idr:13:38--13:45:While processing right hand side -of show at Error2.idr:13:3--15:1: -Multiple solutions found in search of: - Show (Vect k Integer) -at: +Error: While processing right hand side of show. Multiple solutions found in search of: + Show (Vect k Int) + +Error2.idr:13:38--13:45 + | 13 | show (x :: xs) = show x ++ ", " ++ show xs - ^^^^^^^ + | ^^^^^^^ + Possible correct results: Show implementation at Error2.idr:11:1--15:1 Show implementation at Error2.idr:7:1--11:1 -Error2.idr:16:9--17:1:While processing right hand side -of wrong at Error2.idr:16:1--17:1: -Multiple solutions found in search of: - Show (Vect 1 Integer) -at: +Error: While processing right hand side of wrong. Multiple solutions found in search of: + Show (Vect 1 Int) + +Error2.idr:16:9--17:1 16 | wrong = show (the (Vect _ _) [1]) + Possible correct results: Show implementation at Error2.idr:11:1--15:1 Show implementation at Error2.idr:7:1--11:1 diff --git a/tests/idris2/error004/run b/tests/idris2/error004/run index ce9cbc4cd..54530c3cf 100755 --- a/tests/idris2/error004/run +++ b/tests/idris2/error004/run @@ -1,4 +1,4 @@ -$1 --check Error1.idr -$1 --check Error2.idr +$1 --no-color --check Error1.idr +$1 --no-color --check Error2.idr rm -rf build diff --git a/tests/idris2/error005/expected b/tests/idris2/error005/expected index a179142f9..288b735e0 100644 --- a/tests/idris2/error005/expected +++ b/tests/idris2/error005/expected @@ -1,11 +1,15 @@ 1/1: Building IfErr (IfErr.idr) -IfErr.idr:4:11--4:17:While processing right hand side -of foo at IfErr.idr:4:1--6:1: -Can't find an implementation for Eq a at: +Error: While processing right hand side of foo. Can't find an implementation for Eq a. + +IfErr.idr:4:11--4:17 + | 4 | foo x y = x == y - ^^^^^^ -IfErr.idr:7:11--7:17:While processing right hand side -of bar at IfErr.idr:7:1--8:1: -Can't find an implementation for Eq Wibble at: + | ^^^^^^ + +Error: While processing right hand side of bar. Can't find an implementation for Eq Wibble. + +IfErr.idr:7:11--7:17 + | 7 | bar x y = x == y - ^^^^^^ + | ^^^^^^ + diff --git a/tests/idris2/error005/run b/tests/idris2/error005/run index 29ec128c2..a4da9d84c 100755 --- a/tests/idris2/error005/run +++ b/tests/idris2/error005/run @@ -1,3 +1,3 @@ -$1 --check IfErr.idr +$1 --no-color --check IfErr.idr rm -rf build diff --git a/tests/idris2/error006/expected b/tests/idris2/error006/expected index a9ea2cfba..cf184c886 100644 --- a/tests/idris2/error006/expected +++ b/tests/idris2/error006/expected @@ -1,11 +1,15 @@ 1/1: Building IfErr (IfErr.idr) -IfErr.idr:15:10--15:30:While processing right hand side -of test at IfErr.idr:15:1--17:1: -Can't find an implementation for Eq Foo at: +Error: While processing right hand side of test. Can't find an implementation for Eq Foo. + +IfErr.idr:15:10--15:30 + | 15 | test x = showIfEq MkFoo MkBar - ^^^^^^^^^^^^^^^^^^^^ -IfErr.idr:23:9--23:29:While processing right hand side -of test2 at IfErr.idr:23:1--25:1: -Can't find an implementation for Show Foo at: + | ^^^^^^^^^^^^^^^^^^^^ + +Error: While processing right hand side of test2. Can't find an implementation for Show Foo. + +IfErr.idr:23:9--23:29 + | 23 | test2 = showIfEq MkFoo MkBar - ^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^ + diff --git a/tests/idris2/error006/run b/tests/idris2/error006/run index 29ec128c2..a4da9d84c 100755 --- a/tests/idris2/error006/run +++ b/tests/idris2/error006/run @@ -1,3 +1,3 @@ -$1 --check IfErr.idr +$1 --no-color --check IfErr.idr rm -rf build diff --git a/tests/idris2/error007/expected b/tests/idris2/error007/expected index ebac93056..3b687853c 100644 --- a/tests/idris2/error007/expected +++ b/tests/idris2/error007/expected @@ -1,10 +1,8 @@ 1/1: Building CongErr (CongErr.idr) -CongErr.idr:4:11--4:19:While processing right hand side -of fsprf at CongErr.idr:4:1--5:1: -Can't solve constraint between: - ?_ x -and - FS x -at: +Error: While processing right hand side of fsprf. Can't solve constraint between: ?_ x and FS x. + +CongErr.idr:4:11--4:19 + | 4 | fsprf p = cong _ p - ^^^^^^^^ + | ^^^^^^^^ + diff --git a/tests/idris2/error007/run b/tests/idris2/error007/run index 70cb675c7..c8aed1b72 100755 --- a/tests/idris2/error007/run +++ b/tests/idris2/error007/run @@ -1,3 +1,3 @@ -$1 --check CongErr.idr +$1 --no-color --check CongErr.idr rm -rf build diff --git a/tests/idris2/error008/run b/tests/idris2/error008/run index 5bdcf9d32..e3d945fbd 100755 --- a/tests/idris2/error008/run +++ b/tests/idris2/error008/run @@ -1,3 +1,3 @@ -$1 --no-banner DoesntExist.idr < input +$1 --no-color --no-banner DoesntExist.idr < input rm -rf build diff --git a/tests/idris2/error009/expected b/tests/idris2/error009/expected index 793df03fa..1092025bd 100644 --- a/tests/idris2/error009/expected +++ b/tests/idris2/error009/expected @@ -1,2 +1,2 @@ -Exists.idr:1:1--3:1:DoesntExist not found +Error: DoesntExist not found Main> Bye for now! diff --git a/tests/idris2/error009/run b/tests/idris2/error009/run index b37ec2a8c..b1d6656d0 100755 --- a/tests/idris2/error009/run +++ b/tests/idris2/error009/run @@ -1,3 +1,3 @@ -$1 --no-banner Exists.idr < input +$1 --no-color --no-banner Exists.idr < input rm -rf build diff --git a/tests/idris2/error010/expected b/tests/idris2/error010/expected index 57f0f5b6e..e1003b1a8 100644 --- a/tests/idris2/error010/expected +++ b/tests/idris2/error010/expected @@ -1,4 +1,8 @@ 1/1: Building Loop (Loop.idr) -Loop.idr:2:11--2:19:While processing right hand side -of example at Loop.idr:2:1--3:1: -Main.example is already defined +Error: While processing right hand side of example. Main.example is already defined. + +Loop.idr:2:11--2:19 + | + 2 | example = ?example + | ^^^^^^^^ + diff --git a/tests/idris2/error010/run b/tests/idris2/error010/run index 998042235..b82e2bd6a 100755 --- a/tests/idris2/error010/run +++ b/tests/idris2/error010/run @@ -1,3 +1,3 @@ -$1 Loop.idr --check +$1 --no-color Loop.idr --check rm -rf build diff --git a/tests/idris2/error011/expected b/tests/idris2/error011/expected index e2ca12a14..9bca88042 100644 --- a/tests/idris2/error011/expected +++ b/tests/idris2/error011/expected @@ -1,3 +1,15 @@ 1/1: Building ConstructorDuplicate (ConstructorDuplicate.idr) -ConstructorDuplicate.idr:1:14--3:1:Main.B is already defined -ConstructorDuplicate.idr:5:3--5:15:Main.D is already defined +Error: Main.B is already defined. + +ConstructorDuplicate.idr:1:14--3:1 + 1 | data A = B | B + 2 | + 3 | data C : Type -> Type where + +Error: Main.D is already defined. + +ConstructorDuplicate.idr:5:3--5:15 + | + 5 | D : C String + | ^^^^^^^^^^^^ + diff --git a/tests/idris2/error011/run b/tests/idris2/error011/run index a39439a82..d761d6e85 100755 --- a/tests/idris2/error011/run +++ b/tests/idris2/error011/run @@ -1,3 +1,3 @@ -$1 ConstructorDuplicate.idr --check +$1 --no-color ConstructorDuplicate.idr --check rm -rf build diff --git a/tests/idris2/error012/run b/tests/idris2/error012/run index 7958e4a87..1e7bf4582 100755 --- a/tests/idris2/error012/run +++ b/tests/idris2/error012/run @@ -1 +1 @@ -$1 nothere.idr -o argh +$1 --no-color nothere.idr -o argh diff --git a/tests/idris2/import001/run b/tests/idris2/import001/run index 7109e5909..851dabed5 100755 --- a/tests/idris2/import001/run +++ b/tests/idris2/import001/run @@ -1,6 +1,6 @@ -$1 --no-banner --no-prelude Test.idr < input +$1 --no-color --no-banner --no-prelude Test.idr < input sleep 1 touch Mult.idr -$1 --no-banner --no-prelude Test.idr < input +$1 --no-color --no-banner --no-prelude Test.idr < input rm -rf build diff --git a/tests/idris2/import002/expected b/tests/idris2/import002/expected index cdf12af0f..dbc933634 100644 --- a/tests/idris2/import002/expected +++ b/tests/idris2/import002/expected @@ -1,11 +1,17 @@ 1/3: Building Nat (Nat.idr) 2/3: Building Mult (Mult.idr) 3/3: Building Test (Test.idr) -Test.idr:5:9--5:12:While processing type of thing at Test.idr:5:1--5:19: -Undefined name Nat at: +Error: While processing type of thing. Undefined name Nat. + +Test.idr:5:9--5:12 + | 5 | thing : Nat -> Nat - ^^^ -Test.idr:6:1--8:1:No type declaration for Test.thing at: + | ^^^ + +Error: No type declaration for Test.thing. + +Test.idr:6:1--8:1 6 | thing x = mult x (plus x x) 7 | + Test> Bye for now! diff --git a/tests/idris2/import002/run b/tests/idris2/import002/run index c44cc79cc..3116a63e5 100755 --- a/tests/idris2/import002/run +++ b/tests/idris2/import002/run @@ -1,3 +1,3 @@ -echo ':q' | $1 --no-banner --no-prelude Test.idr +echo ':q' | $1 --no-color --no-banner --no-prelude Test.idr rm -rf build diff --git a/tests/idris2/import003/run b/tests/idris2/import003/run index 7cbf21362..7ee33f5dc 100755 --- a/tests/idris2/import003/run +++ b/tests/idris2/import003/run @@ -1,4 +1,4 @@ -$1 --no-banner B.idr < input -$1 --no-banner C.idr < input +$1 --no-color --no-banner B.idr < input +$1 --no-color --no-banner C.idr < input rm -rf build diff --git a/tests/idris2/import004/run b/tests/idris2/import004/run index b98862582..6cf3c1e0c 100755 --- a/tests/idris2/import004/run +++ b/tests/idris2/import004/run @@ -1,4 +1,4 @@ -$1 --no-banner Cycle1.idr -$1 --no-banner Loop.idr +$1 --no-color --no-banner Cycle1.idr +$1 --no-color --no-banner Loop.idr rm -rf build diff --git a/tests/idris2/import005/run b/tests/idris2/import005/run index c75fcaf94..03fab4e89 100644 --- a/tests/idris2/import005/run +++ b/tests/idris2/import005/run @@ -1,3 +1,3 @@ -$1 --no-banner As.idr < input +$1 --no-color --no-banner As.idr < input rm -rf build diff --git a/tests/idris2/interactive001/run b/tests/idris2/interactive001/run index 1d5482f45..09546b35b 100755 --- a/tests/idris2/interactive001/run +++ b/tests/idris2/interactive001/run @@ -1,3 +1,3 @@ -$1 --no-banner LocType.idr < input +$1 --no-color --no-banner LocType.idr < input rm -rf build diff --git a/tests/idris2/interactive002/run b/tests/idris2/interactive002/run index 95e2e7edc..934c37d57 100755 --- a/tests/idris2/interactive002/run +++ b/tests/idris2/interactive002/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.idr < input +$1 --no-color --no-banner IEdit.idr < input rm -rf build diff --git a/tests/idris2/interactive003/run b/tests/idris2/interactive003/run index e7920ddd5..c9d6f4d28 100755 --- a/tests/idris2/interactive003/run +++ b/tests/idris2/interactive003/run @@ -1,4 +1,4 @@ -$1 --no-banner IEdit.idr < input -$1 --no-banner IEdit2.idr < input2 +$1 --no-color --no-banner IEdit.idr < input +$1 --no-color --no-banner IEdit2.idr < input2 rm -rf build diff --git a/tests/idris2/interactive004/run b/tests/idris2/interactive004/run index 95e2e7edc..934c37d57 100755 --- a/tests/idris2/interactive004/run +++ b/tests/idris2/interactive004/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.idr < input +$1 --no-color --no-banner IEdit.idr < input rm -rf build diff --git a/tests/idris2/interactive005/run b/tests/idris2/interactive005/run index 95e2e7edc..934c37d57 100755 --- a/tests/idris2/interactive005/run +++ b/tests/idris2/interactive005/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.idr < input +$1 --no-color --no-banner IEdit.idr < input rm -rf build diff --git a/tests/idris2/interactive006/run b/tests/idris2/interactive006/run index 95e2e7edc..934c37d57 100755 --- a/tests/idris2/interactive006/run +++ b/tests/idris2/interactive006/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.idr < input +$1 --no-color --no-banner IEdit.idr < input rm -rf build diff --git a/tests/idris2/interactive007/run b/tests/idris2/interactive007/run index 95e2e7edc..934c37d57 100755 --- a/tests/idris2/interactive007/run +++ b/tests/idris2/interactive007/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.idr < input +$1 --no-color --no-banner IEdit.idr < input rm -rf build diff --git a/tests/idris2/interactive008/run b/tests/idris2/interactive008/run index 95e2e7edc..934c37d57 100755 --- a/tests/idris2/interactive008/run +++ b/tests/idris2/interactive008/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.idr < input +$1 --no-color --no-banner IEdit.idr < input rm -rf build diff --git a/tests/idris2/interactive009/run b/tests/idris2/interactive009/run index 9d8c8cf20..f99859bb6 100755 --- a/tests/idris2/interactive009/run +++ b/tests/idris2/interactive009/run @@ -1,3 +1,3 @@ -$1 --no-banner Door.idr < input +$1 --no-color --no-banner Door.idr < input rm -rf build diff --git a/tests/idris2/interactive010/run b/tests/idris2/interactive010/run index 95e2e7edc..934c37d57 100755 --- a/tests/idris2/interactive010/run +++ b/tests/idris2/interactive010/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.idr < input +$1 --no-color --no-banner IEdit.idr < input rm -rf build diff --git a/tests/idris2/interactive011/run b/tests/idris2/interactive011/run index 95e2e7edc..934c37d57 100755 --- a/tests/idris2/interactive011/run +++ b/tests/idris2/interactive011/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.idr < input +$1 --no-color --no-banner IEdit.idr < input rm -rf build diff --git a/tests/idris2/interactive012/run b/tests/idris2/interactive012/run index 979cbf422..f53032af6 100755 --- a/tests/idris2/interactive012/run +++ b/tests/idris2/interactive012/run @@ -1,3 +1,3 @@ -$1 --no-banner WithLift.idr < input +$1 --no-color --no-banner WithLift.idr < input rm -rf build diff --git a/tests/idris2/interactive013/run b/tests/idris2/interactive013/run index abb25f9e4..60808465e 100755 --- a/tests/idris2/interactive013/run +++ b/tests/idris2/interactive013/run @@ -1,3 +1,3 @@ -$1 --no-banner Spacing.idr < input +$1 --no-color --no-banner Spacing.idr < input rm -rf build diff --git a/tests/idris2/interactive014/run b/tests/idris2/interactive014/run index c7eb8724f..41dc64380 100755 --- a/tests/idris2/interactive014/run +++ b/tests/idris2/interactive014/run @@ -1,3 +1,3 @@ -$1 --no-banner case.idr < input +$1 --no-color --no-banner case.idr < input rm -rf build diff --git a/tests/idris2/interactive015/run b/tests/idris2/interactive015/run index 95e2e7edc..934c37d57 100755 --- a/tests/idris2/interactive015/run +++ b/tests/idris2/interactive015/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.idr < input +$1 --no-color --no-banner IEdit.idr < input rm -rf build diff --git a/tests/idris2/interface001/run b/tests/idris2/interface001/run index c135dc58b..4ae756f03 100755 --- a/tests/idris2/interface001/run +++ b/tests/idris2/interface001/run @@ -1,4 +1,4 @@ -$1 --no-banner --no-prelude IFace.idr < input -$1 --no-banner --no-prelude IFace1.idr < input1 +$1 --no-color --no-banner --no-prelude IFace.idr < input +$1 --no-color --no-banner --no-prelude IFace1.idr < input1 rm -rf build diff --git a/tests/idris2/interface002/run b/tests/idris2/interface002/run index e66f330e9..e2b8bae8a 100755 --- a/tests/idris2/interface002/run +++ b/tests/idris2/interface002/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude Functor.idr < input +$1 --no-color --no-banner --no-prelude Functor.idr < input rm -rf build diff --git a/tests/idris2/interface003/run b/tests/idris2/interface003/run index e6e1a05b8..d0d5921d8 100755 --- a/tests/idris2/interface003/run +++ b/tests/idris2/interface003/run @@ -1,3 +1,3 @@ -$1 --no-banner Do.idr < input +$1 --no-color --no-banner Do.idr < input rm -rf build diff --git a/tests/idris2/interface004/run b/tests/idris2/interface004/run index e6e1a05b8..d0d5921d8 100755 --- a/tests/idris2/interface004/run +++ b/tests/idris2/interface004/run @@ -1,3 +1,3 @@ -$1 --no-banner Do.idr < input +$1 --no-color --no-banner Do.idr < input rm -rf build diff --git a/tests/idris2/interface005/run b/tests/idris2/interface005/run index 615d6f315..730427bcf 100755 --- a/tests/idris2/interface005/run +++ b/tests/idris2/interface005/run @@ -1,3 +1,3 @@ -$1 --check Deps.idr +$1 --no-color --check Deps.idr rm -rf build diff --git a/tests/idris2/interface006/run b/tests/idris2/interface006/run index 87aeb27c5..1e75a7843 100755 --- a/tests/idris2/interface006/run +++ b/tests/idris2/interface006/run @@ -1,3 +1,3 @@ -$1 --check Bimonad.idr +$1 --no-color --check Bimonad.idr rm -rf build diff --git a/tests/idris2/interface007/run b/tests/idris2/interface007/run index ec5f9873a..3dce8c0e0 100755 --- a/tests/idris2/interface007/run +++ b/tests/idris2/interface007/run @@ -1,3 +1,3 @@ -$1 --debug-elab-check --check A.idr +$1 --no-color --debug-elab-check --check A.idr rm -rf build diff --git a/tests/idris2/interface008/expected b/tests/idris2/interface008/expected index e24244b2e..2f94c41ab 100644 --- a/tests/idris2/interface008/expected +++ b/tests/idris2/interface008/expected @@ -1,6 +1,8 @@ 1/1: Building Deps (Deps.idr) -Deps.idr:18:13--18:14:While processing right hand side -of badcard at Deps.idr:18:3--19:3: -k is not accessible in this context at: +Error: While processing right hand side of badcard. k is not accessible in this context. + +Deps.idr:18:13--18:14 + | 18 | badcard = k - ^ + | ^ + diff --git a/tests/idris2/interface008/run b/tests/idris2/interface008/run index 615d6f315..730427bcf 100755 --- a/tests/idris2/interface008/run +++ b/tests/idris2/interface008/run @@ -1,3 +1,3 @@ -$1 --check Deps.idr +$1 --no-color --check Deps.idr rm -rf build diff --git a/tests/idris2/interface009/run b/tests/idris2/interface009/run index c5b959577..f6af4ecea 100755 --- a/tests/idris2/interface009/run +++ b/tests/idris2/interface009/run @@ -1,3 +1,3 @@ -$1 --no-banner Odd.idr < input +$1 --no-color --no-banner Odd.idr < input rm -rf build diff --git a/tests/idris2/interface010/run b/tests/idris2/interface010/run index cdaf38595..dcfac1fd6 100755 --- a/tests/idris2/interface010/run +++ b/tests/idris2/interface010/run @@ -1,3 +1,3 @@ -$1 Dep.idr --check +$1 --no-color Dep.idr --check rm -rf build diff --git a/tests/idris2/interface011/run b/tests/idris2/interface011/run index 0cb9799c3..ed9521b96 100755 --- a/tests/idris2/interface011/run +++ b/tests/idris2/interface011/run @@ -1,3 +1,3 @@ -$1 FuncImpl.idr --check +$1 --no-color FuncImpl.idr --check rm -rf build diff --git a/tests/idris2/interface012/run b/tests/idris2/interface012/run index a7e03a618..d10e3559c 100755 --- a/tests/idris2/interface012/run +++ b/tests/idris2/interface012/run @@ -1,3 +1,3 @@ -$1 Defmeth.idr --check +$1 --no-color Defmeth.idr --check rm -rf build diff --git a/tests/idris2/interface013/expected b/tests/idris2/interface013/expected index 3cd08d304..bf92e2461 100644 --- a/tests/idris2/interface013/expected +++ b/tests/idris2/interface013/expected @@ -1,6 +1,8 @@ 1/1: Building TypeInt (TypeInt.idr) -TypeInt.idr:14:25--14:49:While processing -constructor MkRecord at TypeInt.idr:14:3--14:61: -Can't find an implementation for Interface ?s at: +Error: While processing constructor MkRecord. Can't find an implementation for Interface ?s. + +TypeInt.idr:14:25--14:49 + | 14 | MkRecord : Value s -> DependentValue {s} value -> Record s - ^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^^ + diff --git a/tests/idris2/interface013/run b/tests/idris2/interface013/run index 8db9ed5d7..577dc48f2 100755 --- a/tests/idris2/interface013/run +++ b/tests/idris2/interface013/run @@ -1,3 +1,3 @@ -$1 TypeInt.idr --check +$1 --no-color TypeInt.idr --check rm -rf build diff --git a/tests/idris2/interface014/run b/tests/idris2/interface014/run index ae441de2d..f4ba189f8 100755 --- a/tests/idris2/interface014/run +++ b/tests/idris2/interface014/run @@ -1,3 +1,3 @@ -$1 DepInt.idr --check +$1 --no-color DepInt.idr --check rm -rf build diff --git a/tests/idris2/interface015/expected b/tests/idris2/interface015/expected index 85ec6295f..be32148bf 100644 --- a/tests/idris2/interface015/expected +++ b/tests/idris2/interface015/expected @@ -1,26 +1,30 @@ 1/1: Building gnu (gnu.idr) -gnu.idr:47:27--47:32:While processing right hand side -of TestSurprise1 at gnu.idr:47:1--49:1: -Multiple solutions found in search of: +Error: While processing right hand side of TestSurprise1. Multiple solutions found in search of: Gnu -at: + +gnu.idr:47:27--47:32 + | 47 | TestSurprise1 gnu1 gnu2 = Guess - ^^^^^ + | ^^^^^ + Possible correct results: gnu1 gnu2 -gnu.idr:50:21--50:26:While processing right hand side -of TestSurprise2 at gnu.idr:50:1--52:1: -Multiple solutions found in search of: +Error: While processing right hand side of TestSurprise2. Multiple solutions found in search of: Gnu -at: + +gnu.idr:50:21--50:26 + | 50 | TestSurprise2 f g = Guess - ^^^^^ + | ^^^^^ + Possible correct results: f () g () -gnu.idr:53:19--53:24:While processing right hand side -of TestSurprise3 at gnu.idr:53:1--54:1: -Can't find an implementation for Gnu at: +Error: While processing right hand side of TestSurprise3. Can't find an implementation for Gnu. + +gnu.idr:53:19--53:24 + | 53 | TestSurprise3 f = Guess - ^^^^^ + | ^^^^^ + diff --git a/tests/idris2/interface015/run b/tests/idris2/interface015/run index f76d54406..4da6e569a 100755 --- a/tests/idris2/interface015/run +++ b/tests/idris2/interface015/run @@ -1,3 +1,3 @@ -$1 gnu.idr --check +$1 --no-color gnu.idr --check rm -rf build diff --git a/tests/idris2/interface016/expected b/tests/idris2/interface016/expected index 9480b0381..602d19bde 100644 --- a/tests/idris2/interface016/expected +++ b/tests/idris2/interface016/expected @@ -1,12 +1,13 @@ 1/1: Building TwoNum (TwoNum.idr) -TwoNum.idr:4:7--4:8:While processing right hand side -of f at TwoNum.idr:2:1--5:1: -While processing right hand side of f,g at TwoNum.idr:4:3--5:1: -Multiple solutions found in search of: +Error: While processing right hand side of f. While processing right hand side of f,g. Multiple solutions found in +search of: Num a -at: + +TwoNum.idr:4:7--4:8 + | 4 | g = 0 - ^ + | ^ + Possible correct results: conArg conArg diff --git a/tests/idris2/interface016/run b/tests/idris2/interface016/run index aea59e70c..b144e4d53 100755 --- a/tests/idris2/interface016/run +++ b/tests/idris2/interface016/run @@ -1,3 +1,3 @@ -$1 TwoNum.idr --check +$1 --no-color TwoNum.idr --check rm -rf build diff --git a/tests/idris2/interpreter001/run b/tests/idris2/interpreter001/run index eb0755dd7..a584b8ab1 100755 --- a/tests/idris2/interpreter001/run +++ b/tests/idris2/interpreter001/run @@ -1 +1 @@ -$1 --no-banner < input +$1 --no-color --no-banner < input diff --git a/tests/idris2/interpreter002/run b/tests/idris2/interpreter002/run index b153002c6..83ae49207 100755 --- a/tests/idris2/interpreter002/run +++ b/tests/idris2/interpreter002/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude < input +$1 --no-color --no-banner --no-prelude < input rm -rf build diff --git a/tests/idris2/interpreter003/expected b/tests/idris2/interpreter003/expected index 5f0449b41..9d6db772f 100644 --- a/tests/idris2/interpreter003/expected +++ b/tests/idris2/interpreter003/expected @@ -1,6 +1,10 @@ -Main> (interactive):1:1--1:25:Undefined name fromMaybe at: +Main> Error: Undefined name fromMaybe. + +(interactive):1:1--1:25 + | 1 | fromMaybe "test" Nothing - ^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^^ + Main> Imported module Data.Maybe Main> "test" Main> Imported module Data.Strings diff --git a/tests/idris2/interpreter003/run b/tests/idris2/interpreter003/run index eb0755dd7..a584b8ab1 100755 --- a/tests/idris2/interpreter003/run +++ b/tests/idris2/interpreter003/run @@ -1 +1 @@ -$1 --no-banner < input +$1 --no-color --no-banner < input diff --git a/tests/idris2/lazy001/run b/tests/idris2/lazy001/run index 40a1fe1e4..640b17afe 100755 --- a/tests/idris2/lazy001/run +++ b/tests/idris2/lazy001/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude Lazy.idr < input +$1 --no-color --no-banner --no-prelude Lazy.idr < input rm -rf build diff --git a/tests/idris2/linear001/run b/tests/idris2/linear001/run index 99b5d29b8..b2872ca28 100755 --- a/tests/idris2/linear001/run +++ b/tests/idris2/linear001/run @@ -1,3 +1,3 @@ -echo ':q' | $1 --no-banner --no-prelude Door.idr +echo ':q' | $1 --no-color --no-banner --no-prelude Door.idr rm -rf build diff --git a/tests/idris2/linear002/run b/tests/idris2/linear002/run index bc3214816..2771b4fca 100755 --- a/tests/idris2/linear002/run +++ b/tests/idris2/linear002/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude Door.idr < input +$1 --no-color --no-banner --no-prelude Door.idr < input rm -rf build diff --git a/tests/idris2/linear003/run b/tests/idris2/linear003/run index 76a7c74a8..86f9c0370 100755 --- a/tests/idris2/linear003/run +++ b/tests/idris2/linear003/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude Linear.idr < input +$1 --no-color --no-banner --no-prelude Linear.idr < input rm -rf build diff --git a/tests/idris2/linear004/expected b/tests/idris2/linear004/expected index 04a6f751d..4df8edfb5 100644 --- a/tests/idris2/linear004/expected +++ b/tests/idris2/linear004/expected @@ -3,39 +3,44 @@ Main> S Z Main> S (S Z) Main> S Z -Main> (interactive):1:15--1:16:x is not accessible in this context at: +Main> Error: x is not accessible in this context. + +(interactive):1:15--1:16 + | 1 | efn (\x, y => x) -- Bad - ^ -Main> (interactive):1:5--1:9:When -unifying Nat -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat -Mismatch between: - Nat -> Nat -> Nat -and - (0 _ : Nat) -> Nat -> Nat -at: + | ^ + +Main> Error: When unifying Nat -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat. +Mismatch between: Nat -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat. + +(interactive):1:5--1:9 + | 1 | efn plus -- Bad - ^^^^ -Main> (interactive):1:5--1:8:When -unifying (1 _ : Nat) -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat -Mismatch between: - (1 _ : Nat) -> Nat -> Nat -and - (0 _ : Nat) -> Nat -> Nat -at: + | ^^^^ + +Main> Error: When unifying (1 _ : Nat) -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat. +Mismatch between: (1 _ : Nat) -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat. + +(interactive):1:5--1:8 + | 1 | efn lin -- Bad - ^^^ -Main> (interactive):1:20--1:21:x is not accessible in this context at: + | ^^^ + +Main> Error: x is not accessible in this context. + +(interactive):1:20--1:21 + | 1 | efn (\x, y => plus x y) -- Bad - ^ + | ^ + Main> S (S Z) Main> S (S Z) -Main> (interactive):1:6--1:12:When -unifying (0 _ : Nat) -> Nat -> Nat and Nat -> Nat -> Nat -Mismatch between: - (0 _ : Nat) -> Nat -> Nat -and - Nat -> Nat -> Nat -at: +Main> Error: When unifying (0 _ : Nat) -> Nat -> Nat and Nat -> Nat -> Nat. +Mismatch between: (0 _ : Nat) -> Nat -> Nat and Nat -> Nat -> Nat. + +(interactive):1:6--1:12 + | 1 | okfn ignore -- Bad - ^^^^^^ + | ^^^^^^ + Main> Bye for now! diff --git a/tests/idris2/linear004/run b/tests/idris2/linear004/run index 42c827f7a..e6aed4db5 100755 --- a/tests/idris2/linear004/run +++ b/tests/idris2/linear004/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude Erase.idr < input +$1 --no-color --no-banner --no-prelude Erase.idr < input rm -rf build diff --git a/tests/idris2/linear005/run b/tests/idris2/linear005/run index 9d8c8cf20..f99859bb6 100755 --- a/tests/idris2/linear005/run +++ b/tests/idris2/linear005/run @@ -1,3 +1,3 @@ -$1 --no-banner Door.idr < input +$1 --no-color --no-banner Door.idr < input rm -rf build diff --git a/tests/idris2/linear006/expected b/tests/idris2/linear006/expected index 06a5e80a9..e831fc956 100644 --- a/tests/idris2/linear006/expected +++ b/tests/idris2/linear006/expected @@ -1,8 +1,10 @@ 1/1: Building ZFun (ZFun.idr) -ZFun.idr:13:7--13:15:While processing right hand side -of bar at ZFun.idr:13:1--15:1: -Main.test is not accessible in this context at: +Error: While processing right hand side of bar. Main.test is not accessible in this context. + +ZFun.idr:13:7--13:15 + | 13 | bar = test foo -- bad! - ^^^^^^^^ + | ^^^^^^^^ + Main> [tc] Main> 10 [tc] Main> Bye for now! diff --git a/tests/idris2/linear006/run b/tests/idris2/linear006/run index 03adf3bf3..3d65e9c54 100755 --- a/tests/idris2/linear006/run +++ b/tests/idris2/linear006/run @@ -1,3 +1,3 @@ -$1 --no-banner ZFun.idr < input +$1 --no-color --no-banner ZFun.idr < input rm -rf build diff --git a/tests/idris2/linear007/expected b/tests/idris2/linear007/expected index 30aaa71d9..6dc86bf1f 100644 --- a/tests/idris2/linear007/expected +++ b/tests/idris2/linear007/expected @@ -1,8 +1,9 @@ 1/1: Building LCase (LCase.idr) -LCase.idr:7:11--10:13:While processing right hand side -of foo at LCase.idr:6:1--12:1: -There are 0 uses of linear name y at: +Error: While processing right hand side of foo. There are 0 uses of linear name y. + +LCase.idr:7:11--10:13 07 | = let 1 test = the Nat $ case z of 08 | Z => Z 09 | (S k) => S z 10 | in + diff --git a/tests/idris2/linear007/run b/tests/idris2/linear007/run index 53d121a42..e10ed2fba 100755 --- a/tests/idris2/linear007/run +++ b/tests/idris2/linear007/run @@ -1,3 +1,3 @@ -$1 --check LCase.idr +$1 --no-color --check LCase.idr rm -rf build diff --git a/tests/idris2/linear008/run b/tests/idris2/linear008/run index 454b6a5df..bd3f81e85 100644 --- a/tests/idris2/linear008/run +++ b/tests/idris2/linear008/run @@ -1,3 +1,3 @@ -$1 --check Door.idr +$1 --no-color --check Door.idr rm -rf build diff --git a/tests/idris2/linear009/run b/tests/idris2/linear009/run index 38d7bafe9..15d4bd5d4 100644 --- a/tests/idris2/linear009/run +++ b/tests/idris2/linear009/run @@ -1,3 +1,3 @@ -$1 --no-banner qtt.idr < input +$1 --no-color --no-banner qtt.idr < input rm -rf build diff --git a/tests/idris2/linear010/run b/tests/idris2/linear010/run index 3e2ba516a..813a30dc9 100644 --- a/tests/idris2/linear010/run +++ b/tests/idris2/linear010/run @@ -1,3 +1,3 @@ -$1 --check Door.idr -p contrib +$1 --no-color --check Door.idr -p contrib rm -rf build diff --git a/tests/idris2/linear011/run b/tests/idris2/linear011/run index f1a4cddfe..380c8b767 100644 --- a/tests/idris2/linear011/run +++ b/tests/idris2/linear011/run @@ -1,3 +1,3 @@ -$1 --no-banner Network.idr -p contrib -p network < input +$1 --no-color --no-banner Network.idr -p contrib -p network < input rm -rf build diff --git a/tests/idris2/linear012/run b/tests/idris2/linear012/run index 154b12194..fb7b69b17 100644 --- a/tests/idris2/linear012/run +++ b/tests/idris2/linear012/run @@ -1,3 +1,3 @@ -$1 --no-banner linholes.idr < input +$1 --no-color --no-banner linholes.idr < input rm -rf build diff --git a/tests/idris2/literate001/run b/tests/idris2/literate001/run index 717ad4fc6..3f498dff1 100755 --- a/tests/idris2/literate001/run +++ b/tests/idris2/literate001/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.lidr < input +$1 --no-color --no-banner IEdit.lidr < input rm -rf build diff --git a/tests/idris2/literate002/run b/tests/idris2/literate002/run index f84e3d8a7..4dfd4e14c 100755 --- a/tests/idris2/literate002/run +++ b/tests/idris2/literate002/run @@ -1,4 +1,4 @@ -$1 --no-banner IEdit.lidr < input -$1 --no-banner IEdit2.lidr < input2 +$1 --no-color --no-banner IEdit.lidr < input +$1 --no-color --no-banner IEdit2.lidr < input2 rm -rf build diff --git a/tests/idris2/literate003/run b/tests/idris2/literate003/run index 717ad4fc6..3f498dff1 100755 --- a/tests/idris2/literate003/run +++ b/tests/idris2/literate003/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.lidr < input +$1 --no-color --no-banner IEdit.lidr < input rm -rf build diff --git a/tests/idris2/literate004/run b/tests/idris2/literate004/run index 717ad4fc6..3f498dff1 100755 --- a/tests/idris2/literate004/run +++ b/tests/idris2/literate004/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.lidr < input +$1 --no-color --no-banner IEdit.lidr < input rm -rf build diff --git a/tests/idris2/literate005/run b/tests/idris2/literate005/run index 717ad4fc6..3f498dff1 100755 --- a/tests/idris2/literate005/run +++ b/tests/idris2/literate005/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.lidr < input +$1 --no-color --no-banner IEdit.lidr < input rm -rf build diff --git a/tests/idris2/literate006/run b/tests/idris2/literate006/run index df706ce86..b5c5ca3c1 100755 --- a/tests/idris2/literate006/run +++ b/tests/idris2/literate006/run @@ -1,3 +1,3 @@ -$1 --no-banner Door.lidr < input +$1 --no-color --no-banner Door.lidr < input rm -rf build diff --git a/tests/idris2/literate007/run b/tests/idris2/literate007/run index 69139e7cc..20b8f2761 100755 --- a/tests/idris2/literate007/run +++ b/tests/idris2/literate007/run @@ -1,4 +1,4 @@ -$1 --no-banner IEdit.lidr < input -$1 --no-banner IEditOrg.org < input2 +$1 --no-color --no-banner IEdit.lidr < input +$1 --no-color --no-banner IEditOrg.org < input2 rm -rf build diff --git a/tests/idris2/literate008/run b/tests/idris2/literate008/run index 717ad4fc6..3f498dff1 100755 --- a/tests/idris2/literate008/run +++ b/tests/idris2/literate008/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.lidr < input +$1 --no-color --no-banner IEdit.lidr < input rm -rf build diff --git a/tests/idris2/literate009/run b/tests/idris2/literate009/run index 7d52e4ac3..a8d401436 100755 --- a/tests/idris2/literate009/run +++ b/tests/idris2/literate009/run @@ -1,3 +1,3 @@ -$1 --no-banner WithLift.lidr < input +$1 --no-color --no-banner WithLift.lidr < input rm -rf build diff --git a/tests/idris2/literate010/run b/tests/idris2/literate010/run index 5579eb335..65361c53b 100755 --- a/tests/idris2/literate010/run +++ b/tests/idris2/literate010/run @@ -1,3 +1,3 @@ -$1 --check --no-banner MyFirstIdrisProgram.org +$1 --no-color --check --no-banner MyFirstIdrisProgram.org rm -rf build diff --git a/tests/idris2/literate011/run b/tests/idris2/literate011/run index fd3507cc0..dcbd95b93 100755 --- a/tests/idris2/literate011/run +++ b/tests/idris2/literate011/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.md < input +$1 --no-color --no-banner IEdit.md < input rm -rf build diff --git a/tests/idris2/literate012/run b/tests/idris2/literate012/run index 9a0e0b008..c1707d512 100755 --- a/tests/idris2/literate012/run +++ b/tests/idris2/literate012/run @@ -1,3 +1,3 @@ -$1 --no-banner IEdit.org < input +$1 --no-color --no-banner IEdit.org < input rm -rf build diff --git a/tests/idris2/literate013/run b/tests/idris2/literate013/run index 7f2c43e56..c834620e5 100755 --- a/tests/idris2/literate013/run +++ b/tests/idris2/literate013/run @@ -1,3 +1,3 @@ -$1 --no-banner --check Lit.lidr +$1 --no-color --no-banner --check Lit.lidr rm -rf build diff --git a/tests/idris2/literate014/run b/tests/idris2/literate014/run index a7845bb47..83ef9eaeb 100755 --- a/tests/idris2/literate014/run +++ b/tests/idris2/literate014/run @@ -1,3 +1,3 @@ -$1 --no-banner with.lidr < input +$1 --no-color --no-banner with.lidr < input rm -rf build diff --git a/tests/idris2/literate015/run b/tests/idris2/literate015/run index ddebcef41..a60364e92 100755 --- a/tests/idris2/literate015/run +++ b/tests/idris2/literate015/run @@ -1,3 +1,3 @@ -$1 --no-banner case.lidr < input +$1 --no-color --no-banner case.lidr < input rm -rf build diff --git a/tests/idris2/namespace001/expected b/tests/idris2/namespace001/expected index 38afb1f69..99710e1f0 100644 --- a/tests/idris2/namespace001/expected +++ b/tests/idris2/namespace001/expected @@ -1,5 +1,10 @@ 1/1: Building Dup (Dup.idr) -Dup.idr:13:1--15:1:Main.Test is already defined +Error: Main.Test is already defined. + +Dup.idr:13:1--15:1 + 13 | private + 14 | data Test = A | B + Main> Bye for now! 1/1: Building Scope (Scope.idr) Main> Main.Test : Type diff --git a/tests/idris2/namespace001/run b/tests/idris2/namespace001/run index e1f12ff00..10eafb5be 100644 --- a/tests/idris2/namespace001/run +++ b/tests/idris2/namespace001/run @@ -1,4 +1,4 @@ -echo ':q' | $1 --no-banner Dup.idr -echo ':t Test' | $1 --no-banner Scope.idr +echo ':q' | $1 --no-color --no-banner Dup.idr +echo ':t Test' | $1 --no-color --no-banner Scope.idr rm -rf build diff --git a/tests/idris2/params001/expected b/tests/idris2/params001/expected index bdeb77402..fa40bfae2 100644 --- a/tests/idris2/params001/expected +++ b/tests/idris2/params001/expected @@ -1,7 +1,9 @@ 1/1: Building param (param.idr) 1/1: Building parambad (parambad.idr) -parambad.idr:7:7--7:10:While processing right hand side -of U at parambad.idr:7:3--8:1: -Name Main.X.foo is private at: +Error: While processing right hand side of U. Name Main.X.foo is private. + +parambad.idr:7:7--7:10 + | 7 | U = foo - ^^^ + | ^^^ + diff --git a/tests/idris2/params001/run b/tests/idris2/params001/run index 44952c647..ce212d9fa 100755 --- a/tests/idris2/params001/run +++ b/tests/idris2/params001/run @@ -1,4 +1,4 @@ -$1 --no-banner --check param.idr -$1 --no-banner --check parambad.idr +$1 --no-color --no-banner --check param.idr +$1 --no-color --no-banner --check parambad.idr rm -rf build diff --git a/tests/idris2/perf001/run b/tests/idris2/perf001/run index 140253135..bcd6e9565 100755 --- a/tests/idris2/perf001/run +++ b/tests/idris2/perf001/run @@ -1,3 +1,3 @@ -$1 --check Big.idr +$1 --no-color --check Big.idr rm -rf build diff --git a/tests/idris2/perf002/run b/tests/idris2/perf002/run index 140253135..bcd6e9565 100755 --- a/tests/idris2/perf002/run +++ b/tests/idris2/perf002/run @@ -1,3 +1,3 @@ -$1 --check Big.idr +$1 --no-color --check Big.idr rm -rf build diff --git a/tests/idris2/perf003/run b/tests/idris2/perf003/run index 3318fddf5..a3f2f59c6 100755 --- a/tests/idris2/perf003/run +++ b/tests/idris2/perf003/run @@ -1,3 +1,3 @@ -$1 --check Auto.idr +$1 --no-color --check Auto.idr rm -rf build diff --git a/tests/idris2/perf004/run b/tests/idris2/perf004/run index cd690a38e..05c67f983 100755 --- a/tests/idris2/perf004/run +++ b/tests/idris2/perf004/run @@ -1,3 +1,3 @@ -$1 --check bigdpair.idr +$1 --no-color --check bigdpair.idr rm -rf build diff --git a/tests/idris2/perror001/expected b/tests/idris2/perror001/expected index 6edaaa2bf..b4b9e1e04 100644 --- a/tests/idris2/perror001/expected +++ b/tests/idris2/perror001/expected @@ -1,2 +1,2 @@ 1/1: Building PError (PError.idr) -PError.idr:5:1--5:1:Parse error: Expected ')' (next tokens: [identifier bar, identifier x, symbol =, let, identifier y, symbol =, literal 42, in, identifier y, symbol +]) +Error: Parse error: Expected ')' (next tokens: [identifier bar, identifier x, symbol =, let, identifier y, symbol =, literal 42, in, identifier y, symbol +]) diff --git a/tests/idris2/perror001/run b/tests/idris2/perror001/run index 53a7590b6..b650e1d4a 100755 --- a/tests/idris2/perror001/run +++ b/tests/idris2/perror001/run @@ -1,3 +1,3 @@ -$1 --check PError.idr +$1 --no-color --check PError.idr rm -rf build diff --git a/tests/idris2/perror002/expected b/tests/idris2/perror002/expected index 80e85eef7..d31ba5955 100644 --- a/tests/idris2/perror002/expected +++ b/tests/idris2/perror002/expected @@ -1,2 +1,2 @@ 1/1: Building PError (PError.idr) -PError.idr:7:1--7:1:Parse error: Expected ')' (next tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end of input]) +Error: Parse error: Expected ')' (next tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end of input]) diff --git a/tests/idris2/perror002/run b/tests/idris2/perror002/run index 53a7590b6..b650e1d4a 100755 --- a/tests/idris2/perror002/run +++ b/tests/idris2/perror002/run @@ -1,3 +1,3 @@ -$1 --check PError.idr +$1 --no-color --check PError.idr rm -rf build diff --git a/tests/idris2/perror003/expected b/tests/idris2/perror003/expected index 5f85ebe52..df177afbb 100644 --- a/tests/idris2/perror003/expected +++ b/tests/idris2/perror003/expected @@ -1,2 +1,2 @@ 1/1: Building PError (PError.idr) -PError.idr:5:17--5:17:Parse error: Expected 'case', 'if', 'do', application or operator expression (next tokens: [symbol (, literal 42, in, identifier y, symbol +, identifier x, identifier baz, symbol :, identifier Int, symbol ->]) +Error: Parse error: Expected 'case', 'if', 'do', application or operator expression (next tokens: [symbol (, literal 42, in, identifier y, symbol +, identifier x, identifier baz, symbol :, identifier Int, symbol ->]) diff --git a/tests/idris2/perror003/run b/tests/idris2/perror003/run index 53a7590b6..b650e1d4a 100755 --- a/tests/idris2/perror003/run +++ b/tests/idris2/perror003/run @@ -1,3 +1,3 @@ -$1 --check PError.idr +$1 --no-color --check PError.idr rm -rf build diff --git a/tests/idris2/perror004/expected b/tests/idris2/perror004/expected index 94d1203dd..4551e85ae 100644 --- a/tests/idris2/perror004/expected +++ b/tests/idris2/perror004/expected @@ -1,2 +1,2 @@ 1/1: Building PError (PError.idr) -PError.idr:4:33--4:33:Parse error: Wrong number of 'with' arguments (next tokens: [symbol =, identifier x, identifier foo, identifier x, identifier y, symbol |, identifier True, symbol |, identifier True, symbol =]) +Error: Parse error: Wrong number of 'with' arguments (next tokens: [symbol =, identifier x, identifier foo, identifier x, identifier y, symbol |, identifier True, symbol |, identifier True, symbol =]) diff --git a/tests/idris2/perror004/run b/tests/idris2/perror004/run index 53a7590b6..b650e1d4a 100755 --- a/tests/idris2/perror004/run +++ b/tests/idris2/perror004/run @@ -1,3 +1,3 @@ -$1 --check PError.idr +$1 --no-color --check PError.idr rm -rf build diff --git a/tests/idris2/perror005/expected b/tests/idris2/perror005/expected index 58d1a53e4..f38e45aac 100644 --- a/tests/idris2/perror005/expected +++ b/tests/idris2/perror005/expected @@ -1,2 +1,2 @@ 1/1: Building PError (PError.idr) -PError.idr:7:1--7:1:Parse error: Expected 'in' (next tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end of input]) +Error: Parse error: Expected 'in' (next tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end of input]) diff --git a/tests/idris2/perror005/run b/tests/idris2/perror005/run index 53a7590b6..b650e1d4a 100755 --- a/tests/idris2/perror005/run +++ b/tests/idris2/perror005/run @@ -1,3 +1,3 @@ -$1 --check PError.idr +$1 --no-color --check PError.idr rm -rf build diff --git a/tests/idris2/perror006/expected b/tests/idris2/perror006/expected index e3ea6a3be..bb8094433 100644 --- a/tests/idris2/perror006/expected +++ b/tests/idris2/perror006/expected @@ -1,2 +1,2 @@ 1/1: Building PError (PError.idr) -PError.idr:7:1--7:1:Parse error: Expected 'else' (next tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end of input]) +Error: Parse error: Expected 'else' (next tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end of input]) diff --git a/tests/idris2/perror006/run b/tests/idris2/perror006/run index 53a7590b6..b650e1d4a 100755 --- a/tests/idris2/perror006/run +++ b/tests/idris2/perror006/run @@ -1,3 +1,3 @@ -$1 --check PError.idr +$1 --no-color --check PError.idr rm -rf build diff --git a/tests/idris2/pkg001/dummy.ipkg b/tests/idris2/pkg001/dummy.ipkg index fe45e2c77..18ac2e05a 100644 --- a/tests/idris2/pkg001/dummy.ipkg +++ b/tests/idris2/pkg001/dummy.ipkg @@ -7,3 +7,4 @@ brief = "This is a dummy package." readme = "README.md" modules = Dummy +opts = "--no-color" diff --git a/tests/idris2/pkg002/dummy.ipkg b/tests/idris2/pkg002/dummy.ipkg index 4b8ce80a7..38f8d45af 100644 --- a/tests/idris2/pkg002/dummy.ipkg +++ b/tests/idris2/pkg002/dummy.ipkg @@ -8,3 +8,4 @@ readme = "README.md" modules = Top.Dummy sourcedir = "src" +opts = "--no-color" diff --git a/tests/idris2/pkg003/testpkg.ipkg b/tests/idris2/pkg003/testpkg.ipkg index e6ee82015..3a12cd5f1 100644 --- a/tests/idris2/pkg003/testpkg.ipkg +++ b/tests/idris2/pkg003/testpkg.ipkg @@ -9,3 +9,4 @@ readme = "README.md" main = Main modules = Main +opts = "--no-color" diff --git a/tests/idris2/pkg004/dummy.ipkg b/tests/idris2/pkg004/dummy.ipkg index fe45e2c77..18ac2e05a 100644 --- a/tests/idris2/pkg004/dummy.ipkg +++ b/tests/idris2/pkg004/dummy.ipkg @@ -7,3 +7,4 @@ brief = "This is a dummy package." readme = "README.md" modules = Dummy +opts = "--no-color" diff --git a/tests/idris2/pkg004/expected b/tests/idris2/pkg004/expected index 3164f08bd..b500b1b9a 100644 --- a/tests/idris2/pkg004/expected +++ b/tests/idris2/pkg004/expected @@ -1,7 +1,11 @@ 1/1: Building Dummy (Dummy.idr) -Dummy> (interactive):1:4--1:13:Undefined name undefined at: +Dummy> Error: Undefined name undefined. + +(interactive):1:4--1:13 + | 1 | :t undefined - ^^^^^^^^^ + | ^^^^^^^^^ + Dummy> Dummy.something : String Dummy> "Something something" Dummy> Dummy.Proxy : Type -> Type diff --git a/tests/idris2/pkg005/foo.ipkg b/tests/idris2/pkg005/foo.ipkg index f9996d63c..e0d5680e0 100644 --- a/tests/idris2/pkg005/foo.ipkg +++ b/tests/idris2/pkg005/foo.ipkg @@ -3,3 +3,4 @@ package foo modules = Foo main = Foo +opts = "--no-color" diff --git a/tests/idris2/real001/run b/tests/idris2/real001/run index bb248b95a..2ebc5b71b 100644 --- a/tests/idris2/real001/run +++ b/tests/idris2/real001/run @@ -1,4 +1,4 @@ -$1 --check TestProto.idr -$1 --check MakeChans.idr +$1 --no-color --check TestProto.idr +$1 --no-color --check MakeChans.idr rm -rf build diff --git a/tests/idris2/real002/run b/tests/idris2/real002/run index 124276f22..1478fc98d 100644 --- a/tests/idris2/real002/run +++ b/tests/idris2/real002/run @@ -1,4 +1,4 @@ -$1 --check Store.idr -$1 --check StoreL.idr +$1 --no-color --check Store.idr +$1 --no-color --check StoreL.idr rm -rf build diff --git a/tests/idris2/record001/run b/tests/idris2/record001/run index dab71a3ff..534a24b9f 100755 --- a/tests/idris2/record001/run +++ b/tests/idris2/record001/run @@ -1,3 +1,3 @@ -$1 --no-banner Record.idr < input +$1 --no-color --no-banner Record.idr < input rm -rf build diff --git a/tests/idris2/record002/run b/tests/idris2/record002/run index dab71a3ff..534a24b9f 100755 --- a/tests/idris2/record002/run +++ b/tests/idris2/record002/run @@ -1,3 +1,3 @@ -$1 --no-banner Record.idr < input +$1 --no-color --no-banner Record.idr < input rm -rf build diff --git a/tests/idris2/record003/run b/tests/idris2/record003/run index f3d663ae0..48ef4cad6 100755 --- a/tests/idris2/record003/run +++ b/tests/idris2/record003/run @@ -1,3 +1,3 @@ -$1 -c --no-banner Record.idr +$1 -c --no-color --no-banner Record.idr rm -rf build diff --git a/tests/idris2/record004/expected b/tests/idris2/record004/expected index d55a9589b..4c9867389 100644 --- a/tests/idris2/record004/expected +++ b/tests/idris2/record004/expected @@ -1,25 +1,32 @@ 1/1: Building Main (Main.idr) -Main.idr:41:5--43:1:complex postfix projections require %language PostfixProjections at: +Error: complex postfix projections require %language PostfixProjections + +Main.idr:41:5--43:1 41 | + rect.(x . topLeft) -- disallowed without %language PostfixProjections 42 | 43 | bad2 : Double -Main.idr:44:9--44:24:postfix projection sections require %language PostfixProjections at: + +Error: postfix projection sections require %language PostfixProjections + +Main.idr:44:9--44:24 + | 44 | bad2 = (.oopFoldl 0 (+)) -- disallowed without %language PostfixProjections - ^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^ + Main> 4.2 Main> 4.2 Main> 10.8 Main> 4.2 Main> 4.2 Main> [1.1, 4.2] -Main> (interactive):1:1--1:4:When unifying (?a -> ?b) -> ?f ?a -> ?f ?b and Point -Mismatch between: - (?a -> ?b) -> ?f ?a -> ?f ?b -and - Point -at: +Main> Error: When unifying (?a -> ?b) -> ?f ?a -> ?f ?b and Point. +Mismatch between: (?a -> ?b) -> ?f ?a -> ?f ?b and Point. + +(interactive):1:1--1:4 + | 1 | map .x [MkPoint 1 2, MkPoint 3 4] - ^^^ + | ^^^ + Main> [2.5, 2.5] Main> 8.1 Main> [8.1, 8.1] diff --git a/tests/idris2/record004/run b/tests/idris2/record004/run index fe350f886..66364c742 100755 --- a/tests/idris2/record004/run +++ b/tests/idris2/record004/run @@ -1,3 +1,3 @@ -$1 --no-banner Main.idr < input +$1 --no-color --no-banner Main.idr < input rm -rf build diff --git a/tests/idris2/record005/run b/tests/idris2/record005/run index 2b392bc6c..2f71d2a16 100755 --- a/tests/idris2/record005/run +++ b/tests/idris2/record005/run @@ -1,3 +1,3 @@ -$1 --no-banner Fld.idr < input +$1 --no-color --no-banner Fld.idr < input rm -rf build diff --git a/tests/idris2/reflection001/expected b/tests/idris2/reflection001/expected index 909f9a7ce..dfccfbfa1 100644 --- a/tests/idris2/reflection001/expected +++ b/tests/idris2/reflection001/expected @@ -1,14 +1,12 @@ 1/1: Building quote (quote.idr) -quote.idr:25:19--25:22:While processing right hand side -of bad at quote.idr:22:1--27:1: -When unifying Int and TTImp -Mismatch between: - Int -and - TTImp -at: +Error: While processing right hand side of bad. When unifying Int and TTImp. +Mismatch between: Int and TTImp. + +quote.idr:25:19--25:22 + | 25 | xfn ~(val)) - ^^^ + | ^^^ + Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IApp (MkFC "quote.idr" (6, 13) (6, 14)) (IVar (MkFC "quote.idr" (6, 13) (6, 14)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (6, 13) (6, 14)) (BI 3)))) (IApp (MkFC "quote.idr" (6, 18) (6, 19)) (IVar (MkFC "quote.idr" (6, 18) (6, 19)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (6, 18) (6, 19)) (BI 4))) Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IVar (MkFC "(interactive)" (0, 6) (0, 10)) (UN "True"))) (IVar (MkFC "(interactive)" (0, 14) (0, 19)) (UN "False")) Main> ILocal (MkFC "quote.idr" (10, 8) (12, 22)) [IClaim (MkFC "quote.idr" (10, 12) (10, 28)) MW Private [] (MkTy (MkFC "quote.idr" (10, 12) (10, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (10, 18) (10, 28)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (10, 18) (10, 21)) IntType) (IPrimVal (MkFC "quote.idr" (10, 25) (10, 28)) IntType))), IDef (MkFC "quote.idr" (11, 12) (11, 30)) (UN "xfn") [PatClause (MkFC "quote.idr" (11, 12) (11, 30)) (IApp (MkFC "quote.idr" (11, 12) (11, 19)) (IVar (MkFC "quote.idr" (11, 12) (11, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (11, 16) (11, 19)) "var")) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IVar (MkFC "quote.idr" (11, 22) (11, 29)) (UN "*")) (IVar (MkFC "quote.idr" (11, 22) (11, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (11, 28) (11, 29)) (IVar (MkFC "quote.idr" (11, 28) (11, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (12, 12) (12, 22)) (IVar (MkFC "quote.idr" (12, 12) (12, 15)) (UN "xfn")) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IVar (MkFC "(interactive)" (0, 9) (0, 12)) (UN "the")) (IPrimVal (MkFC "(interactive)" (0, 13) (0, 16)) IntType)) (IApp (MkFC "(interactive)" (0, 17) (0, 22)) (IVar (MkFC "(interactive)" (0, 17) (0, 22)) (UN "fromInteger")) (IPrimVal (MkFC "(interactive)" (0, 17) (0, 22)) (BI 99994))))) diff --git a/tests/idris2/reflection001/run b/tests/idris2/reflection001/run index 2a502e2b9..775054e50 100755 --- a/tests/idris2/reflection001/run +++ b/tests/idris2/reflection001/run @@ -1,3 +1,3 @@ -$1 --no-banner quote.idr < input +$1 --no-color --no-banner quote.idr < input rm -rf build diff --git a/tests/idris2/reflection002/run b/tests/idris2/reflection002/run index 258e4fb34..7f1deff1f 100755 --- a/tests/idris2/reflection002/run +++ b/tests/idris2/reflection002/run @@ -1,3 +1,3 @@ -$1 --no-banner power.idr < input +$1 --no-color --no-banner power.idr < input rm -rf build diff --git a/tests/idris2/reflection003/expected b/tests/idris2/reflection003/expected index 9def3dc4d..389e8903c 100644 --- a/tests/idris2/reflection003/expected +++ b/tests/idris2/reflection003/expected @@ -5,23 +5,31 @@ LOG 0: Name: Prelude.Types.Strings.++ LOG 0: Type: (%pi Rig1 Explicit (Just x) String (%pi Rig1 Explicit (Just y) String String)) LOG 0: Resolved name: Prelude.Types.Nat LOG 0: Constructors: [Prelude.Types.Z, Prelude.Types.S] -refprims.idr:43:10--43:27:While processing right hand side -of dummy1 at refprims.idr:43:1--45:1: -Error during reflection: Not really trying at: +Error: While processing right hand side of dummy1. Error during reflection: Not really trying + +refprims.idr:43:10--43:27 + | 43 | dummy1 = %runElab logPrims - ^^^^^^^^^^^^^^^^^ -refprims.idr:46:10--46:30:While processing right hand side -of dummy2 at refprims.idr:46:1--48:1: -Error during reflection: Still not trying at: + | ^^^^^^^^^^^^^^^^^ + +Error: While processing right hand side of dummy2. Error during reflection: Still not trying + +refprims.idr:46:10--46:30 + | 46 | dummy2 = %runElab logDataCons - ^^^^^^^^^^^^^^^^^^^^ -refprims.idr:49:10--49:25:While processing right hand side -of dummy3 at refprims.idr:49:1--51:1: -Error during reflection: Undefined name at: + | ^^^^^^^^^^^^^^^^^^^^ + +Error: While processing right hand side of dummy3. Error during reflection: Undefined name + +refprims.idr:49:10--49:25 + | 49 | dummy3 = %runElab logBad - ^^^^^^^^^^^^^^^ -refprims.idr:52:10--52:28:While processing right hand side -of dummy4 at refprims.idr:52:1--54:1: -Error during reflection: failed after generating Main.{plus:XXXX} at: + | ^^^^^^^^^^^^^^^ + +Error: While processing right hand side of dummy4. Error during reflection: failed after generating Main.{plus:XXXX} + +refprims.idr:52:10--52:28 + | 52 | dummy4 = %runElab tryGenSym - ^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^ + diff --git a/tests/idris2/reflection003/run b/tests/idris2/reflection003/run index 223173a47..248aa9b4c 100755 --- a/tests/idris2/reflection003/run +++ b/tests/idris2/reflection003/run @@ -1,3 +1,3 @@ -$1 refprims.idr --check +$1 --no-color refprims.idr --check rm -rf build diff --git a/tests/idris2/reflection004/run b/tests/idris2/reflection004/run index facaa98e2..96decd491 100755 --- a/tests/idris2/reflection004/run +++ b/tests/idris2/reflection004/run @@ -1,3 +1,3 @@ -$1 --no-banner refdecl.idr < input +$1 --no-color --no-banner refdecl.idr < input rm -rf build diff --git a/tests/idris2/reflection005/expected b/tests/idris2/reflection005/expected index f93f64a45..1ec589c83 100644 --- a/tests/idris2/reflection005/expected +++ b/tests/idris2/reflection005/expected @@ -1,13 +1,11 @@ 1/1: Building refdecl (refdecl.idr) -refdecl.idr:13:16--13:29:While processing right hand side -of bad at refdecl.idr:13:1--14:1: -When unifying Elab () and Elab a -Mismatch between: - () -and - a -at: +Error: While processing right hand side of bad. When unifying Elab () and Elab a. +Mismatch between: () and a. + +refdecl.idr:13:16--13:29 + | 13 | bad = %runElab mkDecls `(94) - ^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^ + Main> 9400 Main> Bye for now! diff --git a/tests/idris2/reflection005/run b/tests/idris2/reflection005/run index facaa98e2..96decd491 100755 --- a/tests/idris2/reflection005/run +++ b/tests/idris2/reflection005/run @@ -1,3 +1,3 @@ -$1 --no-banner refdecl.idr < input +$1 --no-color --no-banner refdecl.idr < input rm -rf build diff --git a/tests/idris2/reflection006/expected b/tests/idris2/reflection006/expected index dd7e6f7e3..daab6248e 100644 --- a/tests/idris2/reflection006/expected +++ b/tests/idris2/reflection006/expected @@ -2,8 +2,10 @@ LOG 0: [x, y] LOG 0: Left: ((Prelude.Types.plus x) y) LOG 0: Right: ((Prelude.Types.plus y) x) -refleq.idr:24:16--24:21:While processing right hand side -of commutes at refleq.idr:24:1--25:1: -Error during reflection: Not done at: +Error: While processing right hand side of commutes. Error during reflection: Not done + +refleq.idr:24:16--24:21 + | 24 | commutes x y = prove - ^^^^^ + | ^^^^^ + diff --git a/tests/idris2/reflection006/run b/tests/idris2/reflection006/run index 27bfc8dff..53021b4fe 100755 --- a/tests/idris2/reflection006/run +++ b/tests/idris2/reflection006/run @@ -1,3 +1,3 @@ -$1 --check refleq.idr +$1 --no-color --check refleq.idr rm -rf build diff --git a/tests/idris2/reflection007/run b/tests/idris2/reflection007/run index f6b020a4a..f6f550708 100755 --- a/tests/idris2/reflection007/run +++ b/tests/idris2/reflection007/run @@ -1,3 +1,3 @@ -$1 --no-banner NatExpr.idr < input +$1 --no-color --no-banner NatExpr.idr < input rm -rf build diff --git a/tests/idris2/reflection008/run b/tests/idris2/reflection008/run index f9eed9800..8076bf7a4 100755 --- a/tests/idris2/reflection008/run +++ b/tests/idris2/reflection008/run @@ -1,3 +1,3 @@ -$1 --no-banner Interp.idr < input +$1 --no-color --no-banner Interp.idr < input rm -rf build diff --git a/tests/idris2/reflection009/run b/tests/idris2/reflection009/run index 2e60ba8e0..965edca45 100755 --- a/tests/idris2/reflection009/run +++ b/tests/idris2/reflection009/run @@ -1,3 +1,3 @@ -$1 --check perf.idr +$1 --no-color --check perf.idr rm -rf build diff --git a/tests/idris2/reg001/run b/tests/idris2/reg001/run index cbb0f7e24..6610b35b7 100755 --- a/tests/idris2/reg001/run +++ b/tests/idris2/reg001/run @@ -1,3 +1,3 @@ -$1 --check D.idr +$1 --no-color --check D.idr rm -rf build diff --git a/tests/idris2/reg002/run b/tests/idris2/reg002/run index 9dcacfd25..bdac4f5c3 100755 --- a/tests/idris2/reg002/run +++ b/tests/idris2/reg002/run @@ -1,3 +1,3 @@ -$1 --check linm.idr +$1 --no-color --check linm.idr rm -rf build diff --git a/tests/idris2/reg003/expected b/tests/idris2/reg003/expected index f2814dc36..9eebb233a 100644 --- a/tests/idris2/reg003/expected +++ b/tests/idris2/reg003/expected @@ -1,31 +1,58 @@ 1/1: Building Holes (Holes.idr) -Holes.idr:4:64--4:85:While processing type of Vect_ext at Holes.idr:4:1--5:11: -Undefined name ~=~ at: +Error: While processing type of Vect_ext. Undefined name ~=~. + +Holes.idr:4:64--4:85 + | 4 | Vect_ext : (v : Vect n a) -> (w : Vect n a) -> ((i : Fin n) -> index i v = index i w) - ^^^^^^^^^^^^^^^^^^^^^ -Holes.idr:7:26--7:31:While processing type of Weird at Holes.idr:7:1--7:31: -Undefined name ~=~ at: + | ^^^^^^^^^^^^^^^^^^^^^ + +Error: While processing type of Weird. Undefined name ~=~. + +Holes.idr:7:26--7:31 + | 7 | Weird : (v: Vect n a) -> v = v - ^^^^^ -Holes.idr:8:1--10:1:No type declaration for Main.Weird at: + | ^^^^^ + +Error: No type declaration for Main.Weird. + +Holes.idr:8:1--10:1 08 | Weird v = Vect_ext ?hole0 ?hole1 ?hole2 09 | 10 | f : Bool -> Nat -Holes.idr:10:5--10:9:While processing type of f at Holes.idr:10:1--10:16: -Undefined name Bool at: + +Error: While processing type of f. Undefined name Bool. + +Holes.idr:10:5--10:9 + | 10 | f : Bool -> Nat - ^^^^ -Holes.idr:11:1--12:1:No type declaration for Main.f at: + | ^^^^ + +Error: No type declaration for Main.f. + +Holes.idr:11:1--12:1 11 | f True = 0 12 | f True = ?help -Main> (interactive):1:4--1:8:Undefined name help at: + +Main> Error: Undefined name help. + +(interactive):1:4--1:8 + | 1 | :t help - ^^^^ -Main> (interactive):1:4--1:9:Undefined name hole0 at: + | ^^^^ + +Main> Error: Undefined name hole0. + +(interactive):1:4--1:9 + | 1 | :t hole0 - ^^^^^ -Main> (interactive):1:4--1:9:Undefined name hole1 at: + | ^^^^^ + +Main> Error: Undefined name hole1. + +(interactive):1:4--1:9 + | 1 | :t hole1 - ^^^^^ + | ^^^^^ + Main> Unknown name hole1 Main> Bye for now! diff --git a/tests/idris2/reg003/run b/tests/idris2/reg003/run index 598f75c53..9cf175ecc 100755 --- a/tests/idris2/reg003/run +++ b/tests/idris2/reg003/run @@ -1,3 +1,3 @@ -$1 --no-banner --no-prelude Holes.idr < input +$1 --no-color --no-banner --no-prelude Holes.idr < input rm -rf build diff --git a/tests/idris2/reg004/run b/tests/idris2/reg004/run index 0f5749002..f691c0f3a 100755 --- a/tests/idris2/reg004/run +++ b/tests/idris2/reg004/run @@ -1,3 +1,3 @@ -$1 --check ambig.idr +$1 --no-color --check ambig.idr rm -rf build diff --git a/tests/idris2/reg005/expected b/tests/idris2/reg005/expected index 7089e3a9d..f6ae9680e 100644 --- a/tests/idris2/reg005/expected +++ b/tests/idris2/reg005/expected @@ -1,10 +1,10 @@ 1/1: Building iftype (iftype.idr) -iftype.idr:15:15--15:19:While processing right hand side -of isInListBad at iftype.idr:15:1--16:1: -Can't solve constraint between: - if c then "Foo" else "Baz" -and - if c then "Foo" else "Bar" -at: +Error: While processing right hand side of isInListBad. Can't solve constraint between: if c then "Foo" + else "Baz" and if c then "Foo" + else "Bar". + +iftype.idr:15:15--15:19 + | 15 | isInListBad = Here - ^^^^ + | ^^^^ + diff --git a/tests/idris2/reg005/run b/tests/idris2/reg005/run index 71958949b..69df7c6c9 100755 --- a/tests/idris2/reg005/run +++ b/tests/idris2/reg005/run @@ -1,3 +1,3 @@ -$1 --check iftype.idr +$1 --no-color --check iftype.idr rm -rf build diff --git a/tests/idris2/reg006/run b/tests/idris2/reg006/run index 272df49e6..e0b23330b 100755 --- a/tests/idris2/reg006/run +++ b/tests/idris2/reg006/run @@ -1,3 +1,3 @@ -$1 --check Cmd.idr +$1 --no-color --check Cmd.idr rm -rf build diff --git a/tests/idris2/reg007/expected b/tests/idris2/reg007/expected index 917edd1c3..6175f526f 100644 --- a/tests/idris2/reg007/expected +++ b/tests/idris2/reg007/expected @@ -1,11 +1,9 @@ 1/1: Building Main (Main.idr) -Main.idr:27:26--27:72:While processing right hand side -of dpairWithExtraInfoBad at Main.idr:27:1--28:1: -When unifying [MN 0, MN 0] and [MN 0] -Mismatch between: - [MN 0] -and - [] -at: +Error: While processing right hand side of dpairWithExtraInfoBad. When unifying [MN 0, MN 0] and [MN 0]. +Mismatch between: [MN 0] and []. + +Main.idr:27:26--27:72 + | 27 | dpairWithExtraInfoBad = [([MN 0] ** CLocal {x=MN 0} (First {ns=[MN 0]}))] - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + diff --git a/tests/idris2/reg007/run b/tests/idris2/reg007/run index 237d05676..0078acb82 100755 --- a/tests/idris2/reg007/run +++ b/tests/idris2/reg007/run @@ -1,3 +1,3 @@ -$1 --check Main.idr +$1 --no-color --check Main.idr rm -rf build diff --git a/tests/idris2/reg008/run b/tests/idris2/reg008/run index d901ad1ba..8ab5c5dc4 100755 --- a/tests/idris2/reg008/run +++ b/tests/idris2/reg008/run @@ -1,3 +1,3 @@ -$1 Vending.idr --no-banner --debug-elab-check < input +$1 --no-color Vending.idr --no-banner --debug-elab-check < input rm -rf build diff --git a/tests/idris2/reg009/run b/tests/idris2/reg009/run index 7fe374bb1..5ff95ec9f 100755 --- a/tests/idris2/reg009/run +++ b/tests/idris2/reg009/run @@ -1,3 +1,3 @@ -$1 Case.idr --check +$1 --no-color Case.idr --check rm -rf build diff --git a/tests/idris2/reg010/run b/tests/idris2/reg010/run index 46053502d..a8b60fbf0 100755 --- a/tests/idris2/reg010/run +++ b/tests/idris2/reg010/run @@ -1,3 +1,3 @@ -$1 Recordname.idr --check +$1 --no-color Recordname.idr --check rm -rf build diff --git a/tests/idris2/reg011/run b/tests/idris2/reg011/run index cd5fdfe13..eb263bad6 100755 --- a/tests/idris2/reg011/run +++ b/tests/idris2/reg011/run @@ -1,3 +1,3 @@ -$1 mut.idr --check +$1 --no-color mut.idr --check rm -rf build diff --git a/tests/idris2/reg012/run b/tests/idris2/reg012/run index f69f1ffee..c70f51cda 100755 --- a/tests/idris2/reg012/run +++ b/tests/idris2/reg012/run @@ -1,3 +1,3 @@ -$1 Foo.idr --check +$1 --no-color Foo.idr --check rm -rf build diff --git a/tests/idris2/reg013/expected b/tests/idris2/reg013/expected index 8850110f1..27292d8ff 100644 --- a/tests/idris2/reg013/expected +++ b/tests/idris2/reg013/expected @@ -1,19 +1,29 @@ 1/1: Building UnboundImplicits (UnboundImplicits.idr) -UnboundImplicits.idr:6:22--6:23:While processing -constructor Foo at UnboundImplicits.idr:6:1--9:1: -Undefined name n at: +Error: While processing constructor Foo. Undefined name n. + +UnboundImplicits.idr:6:22--6:23 + | 6 | record Foo (x : Vect n Nat) where - ^ -UnboundImplicits.idr:9:24--9:25:Undefined name n at: + | ^ + +Error: Undefined name n. + +UnboundImplicits.idr:9:24--9:25 + | 9 | parameters (Foo : Vect n Nat) - ^ -UnboundImplicits.idr:14:25--14:26:While processing -constructor Foo at UnboundImplicits.idr:14:1--15:12: -Undefined name n at: + | ^ + +Error: While processing constructor Foo. Undefined name n. + +UnboundImplicits.idr:14:25--14:26 + | 14 | interface Foo (a : Vect n Nat) where - ^ -UnboundImplicits.idr:17:30--17:31:While processing type -of Functor implementation at UnboundImplicits.idr:17:1--18:1 at UnboundImplicits.idr:17:1--18:1: -Undefined name n at: + | ^ + +Error: While processing type of Functor implementation at UnboundImplicits.idr:17:1--18:1. Undefined name n. + +UnboundImplicits.idr:17:30--17:31 + | 17 | implementation Functor (Vect n) where - ^ + | ^ + diff --git a/tests/idris2/reg013/run b/tests/idris2/reg013/run index b2255afc4..1fc923c5b 100755 --- a/tests/idris2/reg013/run +++ b/tests/idris2/reg013/run @@ -1,3 +1,3 @@ -$1 UnboundImplicits.idr --check +$1 --no-color UnboundImplicits.idr --check rm -rf build diff --git a/tests/idris2/reg014/run b/tests/idris2/reg014/run index a4f26feb7..67c9ded5f 100755 --- a/tests/idris2/reg014/run +++ b/tests/idris2/reg014/run @@ -1,3 +1,3 @@ -$1 casecase.idr --check --debug-elab-check +$1 --no-color casecase.idr --check --debug-elab-check rm -rf build diff --git a/tests/idris2/reg015/expected b/tests/idris2/reg015/expected index 19e8a1d46..42294f84a 100644 --- a/tests/idris2/reg015/expected +++ b/tests/idris2/reg015/expected @@ -1,5 +1,9 @@ 1/1: Building anyfail (anyfail.idr) -anyfail.idr:21:1--21:48:showing (MkEvenMoreComplicated (MkMoreComplicated (MkComplicated (PtrAndSize addr len)))) SomethingVeryComplicatedIs is -not a valid impossible case at: +Error: showing (MkEvenMoreComplicated (MkMoreComplicated (MkComplicated (PtrAndSize addr len)))) SomethingVeryComplicatedIs is +not a valid impossible case. + +anyfail.idr:21:1--21:48 + | 21 | showing _ SomethingVeryComplicatedIs impossible - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + diff --git a/tests/idris2/reg015/run b/tests/idris2/reg015/run index 148bfc1b5..daaa8dd65 100755 --- a/tests/idris2/reg015/run +++ b/tests/idris2/reg015/run @@ -1,3 +1,3 @@ -$1 anyfail.idr --check +$1 --no-color anyfail.idr --check rm -rf build diff --git a/tests/idris2/reg016/run b/tests/idris2/reg016/run index 6bb835bc2..2fdca635e 100755 --- a/tests/idris2/reg016/run +++ b/tests/idris2/reg016/run @@ -1,3 +1,3 @@ -$1 Using.idr --check +$1 --no-color Using.idr --check rm -rf build diff --git a/tests/idris2/reg017/expected b/tests/idris2/reg017/expected index a88cf5b44..ea8716528 100644 --- a/tests/idris2/reg017/expected +++ b/tests/idris2/reg017/expected @@ -1,11 +1,9 @@ 1/1: Building lammult (lammult.idr) -lammult.idr:2:15--2:24:While processing right hand side -of badmap at lammult.idr:2:1--3:1: -When unifying (0 _ : ?a) -> ?b and ?a -> ?b -Mismatch between: - (0 _ : ?a) -> ?b -and - ?a -> ?b -at: +Error: While processing right hand side of badmap. When unifying (0 _ : ?a) -> ?b and ?a -> ?b. +Mismatch between: (0 _ : ?a) -> ?b and ?a -> ?b. + +lammult.idr:2:15--2:24 + | 2 | badmap = map (\0 x => 2) - ^^^^^^^^^ + | ^^^^^^^^^ + diff --git a/tests/idris2/reg017/run b/tests/idris2/reg017/run index 2dd460dab..597601d33 100755 --- a/tests/idris2/reg017/run +++ b/tests/idris2/reg017/run @@ -1,3 +1,3 @@ -$1 lammult.idr --check +$1 --no-color lammult.idr --check rm -rf build diff --git a/tests/idris2/reg018/run b/tests/idris2/reg018/run index 5249995d7..ecf6dd474 100755 --- a/tests/idris2/reg018/run +++ b/tests/idris2/reg018/run @@ -1,3 +1,3 @@ -$1 cycle.idr --check +$1 --no-color cycle.idr --check rm -rf build diff --git a/tests/idris2/reg019/expected b/tests/idris2/reg019/expected index 1e29de383..68211dc22 100644 --- a/tests/idris2/reg019/expected +++ b/tests/idris2/reg019/expected @@ -1,28 +1,22 @@ 1/1: Building lazybug (lazybug.idr) -lazybug.idr:5:22--5:34:While processing right hand side -of main at lazybug.idr:5:1--7:1: -Can't solve constraint between: - Bool -and - Lazy Bool -at: +Error: While processing right hand side of main. Can't solve constraint between: Bool and Lazy Bool. + +lazybug.idr:5:22--5:34 + | 5 | main = printLn $ or (map id bools) - ^^^^^^^^^^^^ -lazybug.idr:8:23--8:42:While processing right hand side -of main2 at lazybug.idr:8:1--10:1: -Can't solve constraint between: - Bool -and - Lazy Bool -at: + | ^^^^^^^^^^^^ + +Error: While processing right hand side of main2. Can't solve constraint between: Bool and Lazy Bool. + +lazybug.idr:8:23--8:42 + | 8 | main2 = printLn $ or (map (\x => x) bools) - ^^^^^^^^^^^^^^^^^^^ -lazybug.idr:14:22--14:27:While processing right hand side -of main4 at lazybug.idr:14:1--15:1: -Can't solve constraint between: - Bool -and - Lazy Bool -at: + | ^^^^^^^^^^^^^^^^^^^ + +Error: While processing right hand side of main4. Can't solve constraint between: Bool and Lazy Bool. + +lazybug.idr:14:22--14:27 + | 14 | main4 = printLn $ or bools - ^^^^^ + | ^^^^^ + diff --git a/tests/idris2/reg019/run b/tests/idris2/reg019/run index 826202cb7..437e32de9 100755 --- a/tests/idris2/reg019/run +++ b/tests/idris2/reg019/run @@ -1,3 +1,3 @@ -$1 lazybug.idr --check +$1 --no-color lazybug.idr --check rm -rf build diff --git a/tests/idris2/reg020/run b/tests/idris2/reg020/run index 8271feabd..61bf112fd 100755 --- a/tests/idris2/reg020/run +++ b/tests/idris2/reg020/run @@ -1,3 +1,3 @@ -$1 matchlits.idr --no-banner < input +$1 --no-color matchlits.idr --no-banner < input rm -rf build diff --git a/tests/idris2/reg021/run b/tests/idris2/reg021/run index ef745c03d..4f6414b4e 100755 --- a/tests/idris2/reg021/run +++ b/tests/idris2/reg021/run @@ -1,3 +1,3 @@ -$1 --check case.idr +$1 --no-color --check case.idr rm -rf build diff --git a/tests/idris2/reg022/run b/tests/idris2/reg022/run index ef745c03d..4f6414b4e 100755 --- a/tests/idris2/reg022/run +++ b/tests/idris2/reg022/run @@ -1,3 +1,3 @@ -$1 --check case.idr +$1 --no-color --check case.idr rm -rf build diff --git a/tests/idris2/reg023/expected b/tests/idris2/reg023/expected index af85a5f63..bc31dbfa6 100644 --- a/tests/idris2/reg023/expected +++ b/tests/idris2/reg023/expected @@ -1,10 +1,9 @@ 1/1: Building boom (boom.idr) -boom.idr:23:42--23:66:While processing right hand side -of with block in eraseVar at boom.idr:23:3--24:3: -Can't solve constraint between: - S (countGreater thr xs) -and - countGreater thr xs -at: +Error: While processing right hand side of with block in eraseVar. Can't solve constraint +between: S (countGreater thr xs) and countGreater thr xs. + +boom.idr:23:42--23:66 + | 23 | eraseVar thr (x :: xs) (FS i) | True = FS <$> eraseVar thr xs i - ^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^^ + diff --git a/tests/idris2/reg023/run b/tests/idris2/reg023/run index 46c2764e0..fa3e94cf9 100755 --- a/tests/idris2/reg023/run +++ b/tests/idris2/reg023/run @@ -1,3 +1,3 @@ -$1 --check boom.idr +$1 --no-color --check boom.idr rm -rf build diff --git a/tests/idris2/reg024/run b/tests/idris2/reg024/run index 4d9fc04bc..703310845 100755 --- a/tests/idris2/reg024/run +++ b/tests/idris2/reg024/run @@ -1,3 +1,3 @@ -$1 --no-banner split.idr < input +$1 --no-color --no-banner split.idr < input rm -rf build diff --git a/tests/idris2/reg025/run b/tests/idris2/reg025/run index 7c1b9ab7f..11144d375 100755 --- a/tests/idris2/reg025/run +++ b/tests/idris2/reg025/run @@ -1,3 +1,3 @@ -$1 --no-banner lift.idr < input +$1 --no-color --no-banner lift.idr < input rm -rf build diff --git a/tests/idris2/reg026/run b/tests/idris2/reg026/run index 70fce489c..d04a5bd20 100755 --- a/tests/idris2/reg026/run +++ b/tests/idris2/reg026/run @@ -1,3 +1,3 @@ -$1 --check Meh.idr +$1 --no-color --check Meh.idr rm -rf build diff --git a/tests/idris2/reg027/run b/tests/idris2/reg027/run index be3044582..dbfd739e6 100755 --- a/tests/idris2/reg027/run +++ b/tests/idris2/reg027/run @@ -1,3 +1,3 @@ -$1 --check pwhere.idr +$1 --no-color --check pwhere.idr rm -rf build diff --git a/tests/idris2/reg028/run b/tests/idris2/reg028/run index ad0ea8fa4..0ad6beb70 100755 --- a/tests/idris2/reg028/run +++ b/tests/idris2/reg028/run @@ -1,3 +1,3 @@ -$1 --check Test.idr +$1 --no-color --check Test.idr rm -rf build diff --git a/tests/idris2/reg029/run b/tests/idris2/reg029/run index 601cf940e..4cbc8417d 100755 --- a/tests/idris2/reg029/run +++ b/tests/idris2/reg029/run @@ -1,3 +1,3 @@ -$1 --check lqueue.idr +$1 --no-color --check lqueue.idr rm -rf build diff --git a/tests/idris2/reg030/run b/tests/idris2/reg030/run index 56109e9d2..66fab662c 100755 --- a/tests/idris2/reg030/run +++ b/tests/idris2/reg030/run @@ -1,3 +1,3 @@ -$1 --check A.idr +$1 --no-color --check A.idr rm -rf build diff --git a/tests/idris2/reg031/run b/tests/idris2/reg031/run index f92ab8432..5af484fa2 100755 --- a/tests/idris2/reg031/run +++ b/tests/idris2/reg031/run @@ -1,3 +1,3 @@ -$1 --check dpair.idr +$1 --no-color --check dpair.idr rm -rf build diff --git a/tests/idris2/reg032/run b/tests/idris2/reg032/run index 7295e347c..7f8faa178 100755 --- a/tests/idris2/reg032/run +++ b/tests/idris2/reg032/run @@ -1,3 +1,3 @@ -$1 --check recupdate.idr +$1 --no-color --check recupdate.idr rm -rf build diff --git a/tests/idris2/reg033/run b/tests/idris2/reg033/run index 7efc3e9ef..c331788be 100755 --- a/tests/idris2/reg033/run +++ b/tests/idris2/reg033/run @@ -1,3 +1,3 @@ -$1 --check test.idr +$1 --no-color --check test.idr rm -rf build diff --git a/tests/idris2/total001/run b/tests/idris2/total001/run index be8b6c9a1..7b4861c3b 100755 --- a/tests/idris2/total001/run +++ b/tests/idris2/total001/run @@ -1,3 +1,3 @@ -$1 --no-banner Total.idr < input +$1 --no-color --no-banner Total.idr < input rm -rf build diff --git a/tests/idris2/total002/run b/tests/idris2/total002/run index be8b6c9a1..7b4861c3b 100755 --- a/tests/idris2/total002/run +++ b/tests/idris2/total002/run @@ -1,3 +1,3 @@ -$1 --no-banner Total.idr < input +$1 --no-color --no-banner Total.idr < input rm -rf build diff --git a/tests/idris2/total003/run b/tests/idris2/total003/run index be8b6c9a1..7b4861c3b 100755 --- a/tests/idris2/total003/run +++ b/tests/idris2/total003/run @@ -1,3 +1,3 @@ -$1 --no-banner Total.idr < input +$1 --no-color --no-banner Total.idr < input rm -rf build diff --git a/tests/idris2/total004/run b/tests/idris2/total004/run index be8b6c9a1..7b4861c3b 100755 --- a/tests/idris2/total004/run +++ b/tests/idris2/total004/run @@ -1,3 +1,3 @@ -$1 --no-banner Total.idr < input +$1 --no-color --no-banner Total.idr < input rm -rf build diff --git a/tests/idris2/total005/run b/tests/idris2/total005/run index be8b6c9a1..7b4861c3b 100755 --- a/tests/idris2/total005/run +++ b/tests/idris2/total005/run @@ -1,3 +1,3 @@ -$1 --no-banner Total.idr < input +$1 --no-color --no-banner Total.idr < input rm -rf build diff --git a/tests/idris2/total006/run b/tests/idris2/total006/run index be8b6c9a1..7b4861c3b 100755 --- a/tests/idris2/total006/run +++ b/tests/idris2/total006/run @@ -1,3 +1,3 @@ -$1 --no-banner Total.idr < input +$1 --no-color --no-banner Total.idr < input rm -rf build diff --git a/tests/idris2/total007/expected b/tests/idris2/total007/expected index 7a9d1fd82..3dc5782dc 100644 --- a/tests/idris2/total007/expected +++ b/tests/idris2/total007/expected @@ -1,11 +1,16 @@ 1/1: Building partial (partial.idr) -partial.idr:5:1--6:19:foo is not covering at: +Error: foo is not covering. + +partial.idr:5:1--6:19 5 | total 6 | foo : Maybe a -> a + Missing cases: foo Nothing -partial.idr:13:1--14:37:qsortBad is not total: -possibly not terminating due to recursive path Main.qsortBad -> Main.qsortBad -> Main.qsortBad -at: +Error: qsortBad is not total, possibly not terminating due to recursive +path Main.qsortBad -> Main.qsortBad -> Main.qsortBad + +partial.idr:13:1--14:37 13 | total 14 | qsortBad : Ord a => List a -> List a + diff --git a/tests/idris2/total007/run b/tests/idris2/total007/run index 0c4efcfe7..f17606a8b 100755 --- a/tests/idris2/total007/run +++ b/tests/idris2/total007/run @@ -1,3 +1,3 @@ -$1 --no-banner partial.idr --check +$1 --no-color --no-banner partial.idr --check rm -rf build diff --git a/tests/idris2/total008/expected b/tests/idris2/total008/expected index 37dfc354d..f04926c99 100644 --- a/tests/idris2/total008/expected +++ b/tests/idris2/total008/expected @@ -1,6 +1,9 @@ 1/1: Building partial (partial.idr) -partial.idr:11:1--13:1:foo is not covering at: +Error: foo is not covering. + +partial.idr:11:1--13:1 11 | Foo (Maybe Int) where 12 | foo Nothing = () + Missing cases: foo (Just _) diff --git a/tests/idris2/total008/run b/tests/idris2/total008/run index 0c4efcfe7..f17606a8b 100755 --- a/tests/idris2/total008/run +++ b/tests/idris2/total008/run @@ -1,3 +1,3 @@ -$1 --no-banner partial.idr --check +$1 --no-color --no-banner partial.idr --check rm -rf build diff --git a/tests/idris2/total009/run b/tests/idris2/total009/run index 3a3cd3da1..78d3fc8ed 100755 --- a/tests/idris2/total009/run +++ b/tests/idris2/total009/run @@ -1,3 +1,3 @@ -$1 tree.idr --check +$1 --no-color tree.idr --check rm -rf build diff --git a/tests/idris2/with001/run b/tests/idris2/with001/run index 2f5386681..ae907e9d4 100755 --- a/tests/idris2/with001/run +++ b/tests/idris2/with001/run @@ -1,3 +1,3 @@ -$1 --check Temp.idr +$1 --no-color --check Temp.idr rm -rf build diff --git a/tests/idris2/with002/run b/tests/idris2/with002/run index 2f5386681..ae907e9d4 100755 --- a/tests/idris2/with002/run +++ b/tests/idris2/with002/run @@ -1,3 +1,3 @@ -$1 --check Temp.idr +$1 --no-color --check Temp.idr rm -rf build diff --git a/tests/idris2/with003/expected b/tests/idris2/with003/expected index a47b5f330..72f861297 100644 --- a/tests/idris2/with003/expected +++ b/tests/idris2/with003/expected @@ -1,77 +1,75 @@ 1/1: Building Main (Main.idr) -Main> (interactive):1:66--1:81:Sorry, I can't find any elaboration which works. All -errors: +Main> Error: Sorry, I can't find any elaboration which works. All errors: If Prelude.>>=: Sorry, I can't find any elaboration which works. All errors: -If Prelude.>>=: When unifying ?_ -> IO () and IO ?b -Mismatch between: - ?_ -> IO () -and - IO ?b -at: - 1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" - ^^^^^^^^^^^^^^^ +If Prelude.>>=: When unifying ?_ -> IO () and IO ?b. +Mismatch between: ?_ -> IO () and IO ?b. -If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b -Mismatch between: - ?_ -> IO () -and - IO ?b -at: +(interactive):1:66--1:81 + | 1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" - ^^^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^ +If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b. +Mismatch between: ?_ -> IO () and IO ?b. + +(interactive):1:38--1:64 + | + 1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors: -If Prelude.>>=: When unifying ?_ -> IO () and IO ?b -Mismatch between: - ?_ -> IO () -and - IO ?b -at: +If Prelude.>>=: When unifying ?_ -> IO () and IO ?b. +Mismatch between: ?_ -> IO () and IO ?b. + +(interactive):1:38--1:64 + | 1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" - ^^^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors: -If Prelude.>>=: When unifying ?_ -> IO () and IO ?b -Mismatch between: - ?_ -> IO () -and - IO ?b -at: +If Prelude.>>=: When unifying ?_ -> IO () and IO ?b. +Mismatch between: ?_ -> IO () and IO ?b. + +(interactive):1:66--1:81 + | 1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" - ^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^ -If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b -Mismatch between: - ?_ -> IO () -and - IO ?b -at: +If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b. +Mismatch between: ?_ -> IO () and IO ?b. + +(interactive):1:38--1:64 + | 1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" - ^^^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ +Main> Error: Can't find an implementation for Num (). - -Main> (interactive):1:61--1:66:Can't find an implementation for Num () at: +(interactive):1:61--1:66 + | 1 | with Prelude.(>>=) do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" - ^^^^^ -Main> (interactive):1:4--1:6:Ambiguous elaboration at: - 1 | :t [] - ^^ -Possible correct results: + | ^^^^^ + +Main> Error: Ambiguous elaboration. Possible results: PrimIO.Nil Prelude.Nil Data.Vect.Nil + +(interactive):1:4--1:6 + | + 1 | :t [] + | ^^ + Main> [] : Vect 0 ?elem Main> [] : List ?a -Main> (interactive):1:34--1:41:When unifying Vect 0 ?elem and List ?a -Mismatch between: - Vect 0 ?elem -and - List ?a -at: +Main> Error: When unifying Vect 0 ?elem and List ?a. +Mismatch between: Vect 0 ?elem and List ?a. + +(interactive):1:34--1:41 + | 1 | :t with [Vect.Nil, Prelude.(::)] [1,2,3] - ^^^^^^^ -Main> the (Maybe Integer) (pure 4) : Maybe Integer + | ^^^^^^^ + +Main> the (Maybe Int) (pure 4) : Maybe Int Main> Parse error: Unrecognised command (next tokens: [identifier t, with, symbol [, symbol ], literal 4, end of input]) Main> Bye for now! diff --git a/tests/idris2/with003/run b/tests/idris2/with003/run index fe350f886..66364c742 100755 --- a/tests/idris2/with003/run +++ b/tests/idris2/with003/run @@ -1,3 +1,3 @@ -$1 --no-banner Main.idr < input +$1 --no-color --no-banner Main.idr < input rm -rf build diff --git a/tests/node/node001/run b/tests/node/node001/run index 36b78967b..3b74e7f04 100755 --- a/tests/node/node001/run +++ b/tests/node/node001/run @@ -1,3 +1,3 @@ -$1 --cg node --no-banner Total.idr < input +$1 --no-color --cg node --no-banner Total.idr < input rm -rf build diff --git a/tests/node/node002/run b/tests/node/node002/run index 4b2d4cc5a..3be6ed4e3 100755 --- a/tests/node/node002/run +++ b/tests/node/node002/run @@ -1,2 +1,2 @@ -$1 --cg node --no-banner Pythag.idr < input +$1 --no-color --cg node --no-banner Pythag.idr < input rm -rf build diff --git a/tests/node/node003/run b/tests/node/node003/run index 1917cdfb5..8f4b31d25 100755 --- a/tests/node/node003/run +++ b/tests/node/node003/run @@ -1,2 +1,2 @@ -$1 --cg node --no-banner IORef.idr < input +$1 --no-color --cg node --no-banner IORef.idr < input rm -rf build diff --git a/tests/node/node004/run b/tests/node/node004/run index de18df5c0..0e297293f 100755 --- a/tests/node/node004/run +++ b/tests/node/node004/run @@ -1,2 +1,2 @@ -$1 --cg node --no-banner Buffer.idr < input +$1 --no-color --cg node --no-banner Buffer.idr < input rm -rf build test.buf diff --git a/tests/node/node005/run b/tests/node/node005/run index 9bf1f7f18..e149eb83f 100755 --- a/tests/node/node005/run +++ b/tests/node/node005/run @@ -1,3 +1,3 @@ -$1 --cg node --no-banner Filter.idr < input +$1 --no-color --cg node --no-banner Filter.idr < input rm -rf build diff --git a/tests/node/node006/expected b/tests/node/node006/expected index 09d6bf97f..268ec12cd 100644 --- a/tests/node/node006/expected +++ b/tests/node/node006/expected @@ -15,13 +15,17 @@ Main> Main.strangeId': strangeId' _ Main> Bye for now! 1/1: Building TypeCase2 (TypeCase2.idr) -TypeCase2.idr:5:14--5:17:While processing left hand side -of strangeId at TypeCase2.idr:5:1--6:1: -Can't match on Nat (Erased argument) at: +Error: While processing left hand side of strangeId. Can't match on Nat (Erased argument). + +TypeCase2.idr:5:14--5:17 + | 5 | strangeId {a=Nat} x = x+1 - ^^^ -TypeCase2.idr:9:5--9:8:While processing left hand side -of foo at TypeCase2.idr:9:1--10:1: -Can't match on Nat (Erased argument) at: + | ^^^ + +Error: While processing left hand side of foo. Can't match on Nat (Erased argument). + +TypeCase2.idr:9:5--9:8 + | 9 | foo Nat = "Nat" - ^^^ + | ^^^ + diff --git a/tests/node/node006/run b/tests/node/node006/run index 63a3817bc..ec268e945 100755 --- a/tests/node/node006/run +++ b/tests/node/node006/run @@ -1,4 +1,4 @@ -$1 --cg node --no-banner TypeCase.idr < input -$1 --cg node --no-banner TypeCase2.idr --check +$1 --no-color --cg node --no-banner TypeCase.idr < input +$1 --no-color --cg node --no-banner TypeCase2.idr --check rm -rf build diff --git a/tests/node/node007/run b/tests/node/node007/run index adc812558..2f706267b 100755 --- a/tests/node/node007/run +++ b/tests/node/node007/run @@ -1,3 +1,3 @@ -$1 --cg node --no-banner TypeCase.idr < input +$1 --no-color --cg node --no-banner TypeCase.idr < input rm -rf build diff --git a/tests/node/node008/run b/tests/node/node008/run index 36d4a1139..ac68f2138 100755 --- a/tests/node/node008/run +++ b/tests/node/node008/run @@ -1,3 +1,3 @@ -$1 --cg node --no-banner Nat.idr < input +$1 --no-color --cg node --no-banner Nat.idr < input rm -rf build diff --git a/tests/node/node009/run b/tests/node/node009/run index b1a33028d..49b5eb10d 100755 --- a/tests/node/node009/run +++ b/tests/node/node009/run @@ -1,3 +1,3 @@ -$1 --cg node --no-banner uni.idr < input +$1 --no-color --cg node --no-banner uni.idr < input rm -rf build diff --git a/tests/node/node011/run b/tests/node/node011/run index d46ee7e63..b1171cb1d 100644 --- a/tests/node/node011/run +++ b/tests/node/node011/run @@ -1,3 +1,3 @@ -$1 --cg node --no-banner bangs.idr < input +$1 --no-color --cg node --no-banner bangs.idr < input rm -rf build diff --git a/tests/node/node012/run b/tests/node/node012/run index 0d88d47c9..b5e4f4cc2 100755 --- a/tests/node/node012/run +++ b/tests/node/node012/run @@ -1,2 +1,2 @@ -$1 --cg node --no-banner array.idr < input +$1 --no-color --cg node --no-banner array.idr < input rm -rf build diff --git a/tests/node/node014/run b/tests/node/node014/run index e7505f39a..b3174f331 100755 --- a/tests/node/node014/run +++ b/tests/node/node014/run @@ -1,3 +1,3 @@ -$1 --cg node --no-banner -p network Echo.idr < input +$1 --no-color --cg node --no-banner -p network Echo.idr < input rm -rf build diff --git a/tests/node/node015/run b/tests/node/node015/run index c9bfe42cc..27ec34872 100755 --- a/tests/node/node015/run +++ b/tests/node/node015/run @@ -1,3 +1,3 @@ -$1 --cg node --no-banner Numbers.idr < input +$1 --no-color --cg node --no-banner Numbers.idr < input rm -rf build diff --git a/tests/node/node017/run b/tests/node/node017/run index c32e6ec92..f5ee815ac 100755 --- a/tests/node/node017/run +++ b/tests/node/node017/run @@ -1,4 +1,4 @@ ./gen_expected.sh -$1 --cg node --no-banner dir.idr < input +$1 --no-color --cg node --no-banner dir.idr < input cat testdir/test.txt rm -rf build testdir diff --git a/tests/node/node018/run b/tests/node/node018/run index 13cb0aab8..348c32324 100755 --- a/tests/node/node018/run +++ b/tests/node/node018/run @@ -1,3 +1,3 @@ -$1 --cg node --no-banner File.idr < input +$1 --no-color --cg node --no-banner File.idr < input rm -rf build testout.txt diff --git a/tests/node/node019/run b/tests/node/node019/run index a7b815b32..ba9736ab7 100755 --- a/tests/node/node019/run +++ b/tests/node/node019/run @@ -1,3 +1,3 @@ -$1 --cg node --no-banner partial.idr < input +$1 --no-color --cg node --no-banner partial.idr < input rm -rf build diff --git a/tests/node/node020/run b/tests/node/node020/run index cc2b6663e..83c18813f 100644 --- a/tests/node/node020/run +++ b/tests/node/node020/run @@ -1,3 +1,3 @@ -POPEN_CMD="$1 --version" $1 --cg node --no-banner Popen.idr < input +POPEN_CMD="$1 --version" $1 --no-color --cg node --no-banner Popen.idr < input rm -rf build diff --git a/tests/node/node021/run b/tests/node/node021/run index ec06ec009..2957595ae 100644 --- a/tests/node/node021/run +++ b/tests/node/node021/run @@ -1,3 +1,3 @@ -$1 --cg node --no-banner Bits.idr < input +$1 --no-color --cg node --no-banner Bits.idr < input rm -rf build diff --git a/tests/node/reg001/run b/tests/node/reg001/run index 367ca66b4..6344ee878 100755 --- a/tests/node/reg001/run +++ b/tests/node/reg001/run @@ -1,3 +1,3 @@ -$1 --cg node numbers.idr -x main +$1 --no-color --cg node numbers.idr -x main rm -rf build diff --git a/tests/node/syntax001/run b/tests/node/syntax001/run index 9bdd3cff9..9b16a6e28 100644 --- a/tests/node/syntax001/run +++ b/tests/node/syntax001/run @@ -1,3 +1,3 @@ -$1 --cg node caseBlock.idr -x main +$1 --no-color --cg node caseBlock.idr -x main rm -rf build diff --git a/tests/node/tailrec001/run b/tests/node/tailrec001/run index 17c13dde5..7f2cd55b1 100755 --- a/tests/node/tailrec001/run +++ b/tests/node/tailrec001/run @@ -1,3 +1,3 @@ -$1 --cg node tailrec.idr -x main +$1 --no-color --cg node tailrec.idr -x main rm -rf build diff --git a/tests/typedd-book/chapter01/run b/tests/typedd-book/chapter01/run index 3c16189a8..0ffc17574 100755 --- a/tests/typedd-book/chapter01/run +++ b/tests/typedd-book/chapter01/run @@ -1,4 +1,4 @@ -$1 All.idr --check -$1 --no-banner HoleFix.idr < input +$1 --no-color All.idr --check +$1 --no-color --no-banner HoleFix.idr < input rm -rf build diff --git a/tests/typedd-book/chapter02/run b/tests/typedd-book/chapter02/run index a6d7cb19e..d4c7b98c0 100755 --- a/tests/typedd-book/chapter02/run +++ b/tests/typedd-book/chapter02/run @@ -1,3 +1,3 @@ -$1 All.idr --check +$1 --no-color All.idr --check rm -rf build diff --git a/tests/typedd-book/chapter03/run b/tests/typedd-book/chapter03/run index a6d7cb19e..d4c7b98c0 100755 --- a/tests/typedd-book/chapter03/run +++ b/tests/typedd-book/chapter03/run @@ -1,3 +1,3 @@ -$1 All.idr --check +$1 --no-color All.idr --check rm -rf build diff --git a/tests/typedd-book/chapter04/run b/tests/typedd-book/chapter04/run index a6d7cb19e..d4c7b98c0 100755 --- a/tests/typedd-book/chapter04/run +++ b/tests/typedd-book/chapter04/run @@ -1,3 +1,3 @@ -$1 All.idr --check +$1 --no-color All.idr --check rm -rf build diff --git a/tests/typedd-book/chapter05/run b/tests/typedd-book/chapter05/run index a6d7cb19e..d4c7b98c0 100755 --- a/tests/typedd-book/chapter05/run +++ b/tests/typedd-book/chapter05/run @@ -1,3 +1,3 @@ -$1 All.idr --check +$1 --no-color All.idr --check rm -rf build diff --git a/tests/typedd-book/chapter06/run b/tests/typedd-book/chapter06/run index a6d7cb19e..d4c7b98c0 100755 --- a/tests/typedd-book/chapter06/run +++ b/tests/typedd-book/chapter06/run @@ -1,3 +1,3 @@ -$1 All.idr --check +$1 --no-color All.idr --check rm -rf build diff --git a/tests/typedd-book/chapter07/run b/tests/typedd-book/chapter07/run index a6d7cb19e..d4c7b98c0 100755 --- a/tests/typedd-book/chapter07/run +++ b/tests/typedd-book/chapter07/run @@ -1,3 +1,3 @@ -$1 All.idr --check +$1 --no-color All.idr --check rm -rf build diff --git a/tests/typedd-book/chapter08/run b/tests/typedd-book/chapter08/run index a6d7cb19e..d4c7b98c0 100755 --- a/tests/typedd-book/chapter08/run +++ b/tests/typedd-book/chapter08/run @@ -1,3 +1,3 @@ -$1 All.idr --check +$1 --no-color All.idr --check rm -rf build diff --git a/tests/typedd-book/chapter09/run b/tests/typedd-book/chapter09/run index a6d7cb19e..d4c7b98c0 100755 --- a/tests/typedd-book/chapter09/run +++ b/tests/typedd-book/chapter09/run @@ -1,3 +1,3 @@ -$1 All.idr --check +$1 --no-color All.idr --check rm -rf build diff --git a/tests/typedd-book/chapter10/expected b/tests/typedd-book/chapter10/expected index 62f5bbec5..57aaef005 100644 --- a/tests/typedd-book/chapter10/expected +++ b/tests/typedd-book/chapter10/expected @@ -1,9 +1,12 @@ 1/1: Building DLFail (DLFail.idr) -DLFail.idr:3:20--3:29:While processing left hand side -of describe_list_end at DLFail.idr:3:1--4:1: -Can't match on ?xs ++ [?x] (Not a constructor application or primitive) at: +Error: While processing left hand side of describe_list_end. Can't match on ?xs ++ [?x] (Not a constructor application +or primitive). + +DLFail.idr:3:20--3:29 + | 3 | describe_list_end (xs ++ [x]) = "Non-empty, initial portion = " ++ show xs - ^^^^^^^^^ + | ^^^^^^^^^ + 1/13: Building DataStore (DataStore.idr) 2/13: Building DescribeList (DescribeList.idr) 3/13: Building DescribeList2 (DescribeList2.idr) diff --git a/tests/typedd-book/chapter10/run b/tests/typedd-book/chapter10/run index e6e6eee42..e65e4fba8 100755 --- a/tests/typedd-book/chapter10/run +++ b/tests/typedd-book/chapter10/run @@ -1,4 +1,4 @@ -$1 DLFail.idr --check -$1 All.idr --check +$1 --no-color DLFail.idr --check +$1 --no-color All.idr --check rm -rf build diff --git a/tests/typedd-book/chapter11/run b/tests/typedd-book/chapter11/run index a6d7cb19e..d4c7b98c0 100755 --- a/tests/typedd-book/chapter11/run +++ b/tests/typedd-book/chapter11/run @@ -1,3 +1,3 @@ -$1 All.idr --check +$1 --no-color All.idr --check rm -rf build diff --git a/tests/typedd-book/chapter12/run b/tests/typedd-book/chapter12/run index a6d7cb19e..d4c7b98c0 100755 --- a/tests/typedd-book/chapter12/run +++ b/tests/typedd-book/chapter12/run @@ -1,3 +1,3 @@ -$1 All.idr --check +$1 --no-color All.idr --check rm -rf build diff --git a/tests/typedd-book/chapter13/run b/tests/typedd-book/chapter13/run index a6d7cb19e..d4c7b98c0 100755 --- a/tests/typedd-book/chapter13/run +++ b/tests/typedd-book/chapter13/run @@ -1,3 +1,3 @@ -$1 All.idr --check +$1 --no-color All.idr --check rm -rf build diff --git a/tests/typedd-book/chapter14/run b/tests/typedd-book/chapter14/run index a6d7cb19e..d4c7b98c0 100755 --- a/tests/typedd-book/chapter14/run +++ b/tests/typedd-book/chapter14/run @@ -1,3 +1,3 @@ -$1 All.idr --check +$1 --no-color All.idr --check rm -rf build