Error Message Potpourri (#3429)

CHANGELOG_NEXT.md

@@ -27,6 +27,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Remove reference to column number parameter in help menu for `refine` command.
 
+* CLI errors will now be printed to `stderr` instead of `stdout`.
+
 ### Building/Packaging changes
 
 * The Nix flake's `buildIdris` function now returns a set with `executable` and

src/Idris/CommandLine.idr

@@ -2,6 +2,9 @@ module Idris.CommandLine
 
 import Idris.Env
 import Idris.Version
+import Idris.Doc.Display
+import Idris.Doc.String
+import Idris.Pretty
 
 import Core.Options
 
@@ -507,13 +510,36 @@ export
 getOpts : List String -> Either String (List CLOpt)
 getOpts opts = parseOpts options opts
 
-
 export covering
 getCmdOpts : IO (Either String (List CLOpt))
 getCmdOpts = do (_ :: opts) <- getArgs
                     | _ => pure (Left "Invalid command line")
                 pure $ getOpts opts
 
+||| Find an opt that would have matched if only the user had prefixed it with
+||| double-dashes. It is common to see the user error of specifying a command
+||| like "idris2 repl ..." when they mean to write "idris2 --repl ..."
+export
+findNearMatchOpt : String -> Maybe String
+findNearMatchOpt arg =
+  let argWithDashes = "--\{arg}"
+  in
+  case (getOpts [argWithDashes]) of
+       Right [(InputFile _)] => Nothing
+       Right [_] => Just argWithDashes
+       _ => Nothing
+
+||| Suggest an opt that would have matched if only the user had prefixed it with
+||| double-dashes. It is common to see the user error of specifying a command
+||| like "idris2 repl ..." when they mean to write "idris2 --repl ..."
+export
+nearMatchOptSuggestion : String -> Maybe (Doc IdrisAnn)
+nearMatchOptSuggestion arg =
+    findNearMatchOpt arg <&>
+      \opt =>
+        (reflow "Did you mean to type" <++>
+          (dquotes . meta $ pretty0 opt) <+> "?")
+
 ||| List of all command line option flags.
 export
 optionFlags : List String

src/Idris/Driver.idr

@@ -37,10 +37,12 @@ import Yaffle.Main
 
 %default covering
 
-findInput : List CLOpt -> Maybe String
-findInput [] = Nothing
-findInput (InputFile f :: fs) = Just f
-findInput (_ :: fs) = findInput fs
+findInputs : List CLOpt -> Maybe (List1 String)
+findInputs [] = Nothing
+findInputs (InputFile f :: fs) =
+  let rest = maybe [] toList (findInputs fs)
+  in  Just (f ::: rest)
+findInputs (_ :: fs) = findInputs fs
 
 splitPaths : String -> List1 String
 splitPaths = map trim . split (==pathSeparator)
@@ -157,9 +159,20 @@ stMain cgs opts
          let ide = ideMode opts
          let ideSocket = ideModeSocket opts
          let outmode = if ide then IDEMode 0 stdin stdout else REPL InfoLvl
-         let fname = findInput opts
-         o <- newRef ROpts (REPL.Opts.defaultOpts fname outmode cgs)
+         o <- newRef ROpts (REPL.Opts.defaultOpts Nothing outmode cgs)
          updateEnv
+         fname <- case (findInputs opts) of
+                       Just (fname ::: Nil) => pure $ Just fname
+                       Nothing => pure Nothing
+                       Just (fname1 ::: fnames) => do
+                         let suggestion = nearMatchOptSuggestion fname1
+                         renderedSuggestion <- maybe (pure "") render suggestion
+                         quitWithError $
+                           UserError """
+                                     Expected at most one input file but was given: \{joinBy ", " (fname1 :: fnames)}
+                                     \{renderedSuggestion}
+                                     """
+         update ROpts { mainfile := fname }
 
          finish <- showInfo opts
          when (not finish) $ do
@@ -171,7 +184,7 @@ stMain cgs opts
            -- If there's a --build or --install, just do that then quit
            done <- processPackageOpts opts
 
-           when (not done) $ flip catch renderError $
+           when (not done) $ flip catch quitWithError $
               do when (checkVerbose opts) $ -- override Quiet if implicitly set
                      setOutput (REPL InfoLvl)
                  u <- newRef UST initUState
@@ -197,7 +210,7 @@ stMain cgs opts
                                    pure Done
                       Just f => logTime 1 "Loading main file" $ do
                                   res <- loadMainFile f
-                                  displayErrors res
+                                  displayStartupErrors res
                                   pure res
 
                  doRepl <- catch (postOptions result opts)
@@ -231,14 +244,14 @@ stMain cgs opts
 
   where
 
-  renderError : {auto c : Ref Ctxt Defs} ->
+  quitWithError : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 {auto o : Ref ROpts REPLOpts} ->
-                Error -> Core ()
-  renderError err = do
-    doc <- perror err
+                Error -> Core a
+  quitWithError err = do
+    doc <- display err
     msg <- render doc
-    throw (UserError msg)
+    coreLift (die msg)
 
 -- Run any options (such as --version or --help) which imply printing a
 -- message then exiting. Returns wheter the program should continue

src/Idris/Error.idr

@@ -747,7 +747,7 @@ perrorRaw (CyclicImports ns)
         <++> concatWith (surround " -> ") (pretty0 <$> ns)
 perrorRaw ForceNeeded = pure $ errorDesc (reflow "Internal error when resolving implicit laziness")
 perrorRaw (InternalError str) = pure $ errorDesc (reflow "INTERNAL ERROR" <+> colon) <++> pretty0 str
-perrorRaw (UserError str) = pure $ errorDesc ("Error" <+> colon) <++> pretty0 str
+perrorRaw (UserError str) = pure . errorDesc $ pretty0 str
 perrorRaw (NoForeignCC fc specs) = do
     let cgs = fst <$> availableCGs (options !(get Ctxt))
     let res = vsep [ errorDesc (reflow ("The given specifier '" ++ show specs ++ "' was not accepted by any backend. Available backends") <+> colon)

src/Idris/Package.idr

@@ -896,7 +896,7 @@ runRepl fname = do
       Nothing => pure ()
       Just fn => do
         errs <- loadMainFile fn
-        displayErrors errs
+        displayStartupErrors errs
   repl {u} {s}
 
 ||| If the user did not provide a package file we can look in the working

src/Idris/REPL.idr

@@ -26,6 +26,7 @@ import Core.SchemeEval
 
 import Parser.Unlit
 
+import Idris.CommandLine
 import Idris.Desugar
 import Idris.Doc.Display
 import Idris.Doc.String
@@ -1226,6 +1227,17 @@ mutual
   handleResult Exited = iputStrLn (reflow "Bye for now!")
   handleResult other = do { displayResult other ; repl }
 
+  fileLoadingError : (fname : String) -> (err : FileError) -> (suggestion : Maybe (Doc IdrisAnn)) -> Doc IdrisAnn
+  fileLoadingError fname err suggestion =
+    let suggestion = maybe "" (hardline <+>) suggestion
+    in
+    hardline <+>
+    (indent 2 $
+      error ((reflow "Error loading file") <++> (dquotes $ pretty0 fname) <+> colon) <++>
+        pretty0 (show err) <+>
+      suggestion) <+>
+    hardline
+
   export
   displayResult : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
@@ -1243,7 +1255,7 @@ mutual
   displayResult (ErrorLoadingModule x err)
     = printResult (reflow "Error loading module" <++> pretty0 x <+> colon <++> !(perror err))
   displayResult (ErrorLoadingFile x err)
-    = printResult (reflow "Error loading file" <++> pretty0 x <+> colon <++> pretty0 (show err))
+    = printResult (fileLoadingError x err Nothing)
   displayResult (ErrorsBuildingFile x errs)
     = printResult (reflow "Error(s) building file" <++> pretty0 x) -- messages already displayed while building
   displayResult NoFileLoaded = printResult (reflow "No file can be reloaded")
@@ -1295,12 +1307,21 @@ mutual
       cmdInfo : (List String, CmdArg, String) -> String
       cmdInfo (cmds, args, text) = " " ++ col 18 36 (showSep " " cmds) (show args) text
 
+  ||| Display errors that may occur when starting the REPL.
+  ||| Does not force the REPL to exit, just prints the error(s).
+  |||
+  ||| NOTE: functionally the only reason to consider this function specialized
+  ||| to "startup" is that it will provide suggestions to the user under the
+  ||| assumption that the user has just entered the REPL via CLI arguments that
+  ||| they may have used incorrectly.
   export
-  displayErrors : {auto c : Ref Ctxt Defs} ->
+  displayStartupErrors : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto m : Ref MD Metadata} ->
          {auto o : Ref ROpts REPLOpts} -> REPLResult -> Core ()
-  displayErrors (ErrorLoadingFile x err)
-    = printError (reflow "File error in" <++> pretty0 x <+> colon <++> pretty0 (show err))
-  displayErrors _ = pure ()
+  displayStartupErrors (ErrorLoadingFile x err) =
+    let suggestion = nearMatchOptSuggestion x
+    in
+      printError (fileLoadingError x err suggestion)
+  displayStartupErrors _ = pure ()

src/Protocol/SExp.idr

@@ -2,13 +2,10 @@ module Protocol.SExp
 
 import Data.List
 import Data.List1
+import Data.String
 
 %default total
 
--- should be in base somewhere!
-join : String -> List String -> String
-join sep xs = concat $ intersperse sep xs
-
 public export
 data SExp = SExpList (List SExp)
           | StringAtom String
@@ -26,7 +23,7 @@ escape = pack . concatMap escapeChar . unpack
 
 export
 Show SExp where
-  show (SExpList xs) = assert_total $ "(" ++ join " " (map show xs) ++ ")"
+  show (SExpList xs) = assert_total $ "(" ++ joinBy " " (map show xs) ++ ")"
   show (StringAtom str) = "\"" ++ escape str ++ "\""
   show (BoolAtom b) = ":" ++ show b
   show (IntegerAtom i) = show i

tests/idris2/error/error008/expected

@@ -1,2 +1,4 @@
-File error in DoesntExist.idr: File Not Found
+
+  Error loading file "DoesntExist.idr": File Not Found
+
 Main> Bye for now!

tests/idris2/error/error012/expected

@@ -1 +1,3 @@
-File error in nothere.idr: File Not Found
+
+  Error loading file "nothere.idr": File Not Found
+

tests/idris2/error/error032/expected

@@ -0,0 +1,2 @@
+Error: Expected at most one input file but was given: repl, pkg.ipkg
+Did you mean to type "--repl"?

tests/idris2/error/error032/run

@@ -0,0 +1,5 @@
+. ../../../testutils.sh
+
+# it is common to hear about folks doing this by accident when they mean
+# to do `idris2 --repl pkg.ipkg`.
+idris2 repl pkg.ipkg 2>&1

tests/idris2/error/perror008/expected

@@ -57,13 +57,13 @@ Issue710f:2:15--2:19
  2 |   constructor cons
                    ^^^^
 ... (1 others)
-Uncaught error: Error: Expected a capitalised identifier, got: ggg.
+Error: Expected a capitalised identifier, got: ggg.
 
 Issue1224a:1:8--1:11
  1 | module ggg
             ^^^
 
-Uncaught error: Error: Expected a capitalised identifier, got: ggg.
+Error: Expected a capitalised identifier, got: ggg.
 
 Issue1224b:1:8--1:11
  1 | import ggg

tests/idris2/error/perror008/run

@@ -1,11 +1,11 @@
 . ../../../testutils.sh
 
-check Issue710a.idr || true
-check Issue710b.idr || true
-check Issue710c.idr || true
-check Issue710d.idr || true
-check Issue710e.idr || true
-check Issue710f.idr || true
+check Issue710a.idr 2>&1 || true
+check Issue710b.idr 2>&1 || true
+check Issue710c.idr 2>&1 || true
+check Issue710d.idr 2>&1 || true
+check Issue710e.idr 2>&1 || true
+check Issue710f.idr 2>&1 || true
 
-check Issue1224a.idr || true
-check Issue1224b.idr || true
+check Issue1224a.idr 2>&1 || true
+check Issue1224b.idr 2>&1 || true

tests/idris2/error/perror011/expected

@@ -1,11 +1,11 @@
-Uncaught error: Error: Bracket is not properly closed.
+Error: Bracket is not properly closed.
 
 Issue1345:2:1--2:2
  1 | infixr 0 -->
  2 | (-->) : (Type -> Type) -> (Type -> Type) -> Type
      ^
 
-Uncaught error: Error: Bracket is not properly closed.
+Error: Bracket is not properly closed.
 
 Issue1496-1:5:24--5:25
  1 | module Main
@@ -15,7 +15,7 @@ Issue1496-1:5:24--5:25
  5 |   show (Really err) =  ["RR"
                             ^
 
-Uncaught error: Error: Bracket is not properly closed.
+Error: Bracket is not properly closed.
 
 Issue1496-2:2:1--2:2
  1 | module X

tests/idris2/error/perror011/run

@@ -1,6 +1,6 @@
 . ../../../testutils.sh
 
-check Issue1345.idr || true
-check Issue1496-1.idr || true
-check Issue1496-2.idr || true
+check Issue1345.idr 2>&1 || true
+check Issue1496-1.idr 2>&1 || true
+check Issue1496-2.idr 2>&1 || true
 idris2 --build foo.ipkg

tests/idris2/misc/import004/expected

@@ -1,2 +1,2 @@
-Uncaught error: Error: Module imports form a cycle: Cycle2 -> Cycle1 -> Cycle1
-Uncaught error: Error: Module imports form a cycle: Loop -> Loop
+Error: Module imports form a cycle: Cycle2 -> Cycle1 -> Cycle1
+Error: Module imports form a cycle: Loop -> Loop

tests/idris2/misc/import004/run

@@ -1,4 +1,4 @@
 . ../../../testutils.sh
 
-idris2 Cycle1.idr
-idris2 Loop.idr
+idris2 2>&1 Cycle1.idr
+idris2 2>&1 Loop.idr