Allow absolute paths in --find-ipkg

Otherwise they need to be relative to know where the root of the module
tree is, so report an error with absolute paths in other cases.

src/Core/Core.idr

@@ -126,6 +126,7 @@ data Error : Type where
      CyclicImports : List (List String) -> Error
      ForceNeeded : Error
      InternalError : String -> Error
+     UserError : String -> Error
 
      InType : FC -> Name -> Error -> Error
      InCon : FC -> Name -> Error -> Error
@@ -290,6 +291,7 @@ Show Error where
       showMod ns = showSep "." (reverse ns)
   show ForceNeeded = "Internal error when resolving implicit laziness"
   show (InternalError str) = "INTERNAL ERROR: " ++ str
+  show (UserError str) = "Error: " ++ str
 
   show (InType fc n err)
        = show fc ++ ":When elaborating type of " ++ show n ++ ":\n" ++
@@ -363,6 +365,7 @@ getErrorLoc (ModuleNotFound loc _) = Just loc
 getErrorLoc (CyclicImports _) = Nothing
 getErrorLoc ForceNeeded = Nothing
 getErrorLoc (InternalError _) = Nothing
+getErrorLoc (UserError _) = Nothing
 getErrorLoc (InType _ _ err) = getErrorLoc err
 getErrorLoc (InCon _ _ err) = getErrorLoc err
 getErrorLoc (InLHS _ _ err) = getErrorLoc err

src/Idris/Error.idr

@@ -245,6 +245,7 @@ perror (CyclicImports ns)
     showMod ns = showSep "." (reverse ns)
 perror ForceNeeded = pure "Internal error when resolving implicit laziness"
 perror (InternalError str) = pure $ "INTERNAL ERROR: " ++ str
+perror (UserError str) = pure $ "Error: " ++ str
 
 perror (InType fc n err)
     = pure $ "While processing type of " ++ !(prettyName n) ++

src/Idris/Main.idr

@@ -122,6 +122,13 @@ checkVerbose [] = False
 checkVerbose (Verbose :: _) = True
 checkVerbose (_ :: xs) = checkVerbose xs
 
+checkRelative : Maybe String -> Core (Maybe String)
+checkRelative Nothing = pure Nothing
+checkRelative (Just str)
+    = if isAbsolute str
+         then throw (InternalError "Absolute paths only allowed with --find-ipkg")
+         else pure (Just str)
+
 stMain : List CLOpt -> Core ()
 stMain opts
     = do False <- tryYaffle opts
@@ -163,7 +170,8 @@ stMain opts
                    iputStrLn banner
                  fname <- if findipkg session
                              then findIpkg fname
-                             else pure fname
+                             else checkRelative fname
+                 setMainFile fname
                  the (Core ()) $ case fname of
                       Nothing => logTime "Loading prelude" $
                                    when (not $ noprelude session) $

src/Idris/Package.idr

@@ -550,7 +550,9 @@ findIpkg : {auto c : Ref Ctxt Defs} ->
            Maybe String -> Core (Maybe String)
 findIpkg fname
    = do Just (dir, ipkgn, up) <- coreLift findIpkgFile
-             | Nothing => pure fname
+             | Nothing => case fname of
+                               Nothing => pure Nothing
+                               Just srcpath => pure (fileName srcpath)
         coreLift $ changeDir dir
         Right (pname, fs) <- coreLift $ parseFile ipkgn
                                  (do desc <- parsePkgDesc ipkgn
@@ -564,8 +566,10 @@ findIpkg fname
         loadDependencies (depends pkg)
         case fname of
              Nothing => pure Nothing
-             Just src =>
-                do let src' = up </> src
+             Just srcpath =>
+                do let Just src = fileName srcpath
+                       | _ => pure (Just srcpath)
+                   let src' = up </> src
                    setSource src'
                    opts <- get ROpts
                    put ROpts (record { mainfile = Just src' } opts)

src/Idris/REPLOpts.idr

@@ -47,6 +47,13 @@ getOutput : {auto o : Ref ROpts REPLOpts} -> Core OutputMode
 getOutput = do opts <- get ROpts
                pure (idemode opts)
 
+export
+setMainFile : {auto o : Ref ROpts REPLOpts} ->
+              Maybe String -> Core ()
+setMainFile src
+    = do opts <- get ROpts
+         put ROpts (record { mainfile = src } opts)
+
 export
 setSource : {auto o : Ref ROpts REPLOpts} ->
             String -> Core ()