add warning when a package with only bad TTC versions installed is en…

…countered

src/Idris/Driver.idr

@@ -182,7 +182,7 @@ stMain cgs opts
               | False => pure ()
 
            -- If there's a --build or --install, just do that then quit
-           done <- processPackageOpts opts
+           done <- flip catch quitWithError $ processPackageOpts opts
 
            when (not done) $ flip catch quitWithError $
               do when (checkVerbose opts) $ -- override Quiet if implicitly set

src/Idris/Package.idr

@@ -379,7 +379,8 @@ addDeps :
     Core ()
 addDeps pkg = do
   Resolved allPkgs <- getTransitiveDeps pkg.depends empty
-    | Failed errs => throw $ GenericMsg EmptyFC (printErrs pkg errs)
+    | Failed errs => do
+        throw $ GenericMsg EmptyFC (printErrs pkg errs)
   log "package.depends" 10 $ "all depends: \{show allPkgs}"
   traverse_ addPackageDir allPkgs
   traverse_ addDataDir ((</> "data") <$> allPkgs)
@@ -914,14 +915,24 @@ localPackageFile Nothing
          [] => throw $ UserError "No .ipkg file supplied and none could be found in the working directory."
          _ => throw $ UserError "No .ipkg file supplied and the working directory contains more than one."
 
+withWarnings : Ref Ctxt Defs =>
+               Ref Syn SyntaxInfo =>
+               Ref ROpts REPLOpts =>
+               Core a -> Core a
+withWarnings op = do o <- catch op $ \err =>
+                           do ignore emitWarnings
+                              throw err
+                     ignore emitWarnings
+                     pure o
+
 processPackage : {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->
                  {auto o : Ref ROpts REPLOpts} ->
                  List CLOpt ->
                  (PkgCommand, Maybe String) ->
                  Core ()
 processPackage opts (cmd, mfile)
-    = withCtxt . withSyn . withROpts $ case cmd of
+    = withCtxt . withWarnings . withSyn . withROpts $ case cmd of
         Init =>
           do Just pkg <- coreLift interactive
                | Nothing => coreLift (exitWith (ExitFailure 1))

src/Idris/SetOptions.idr

@@ -89,20 +89,50 @@ getPackageDirs dname = do
 ||| Only package's with build artifacts for the correct TTC version for the
 ||| compiler will be considered.
 export
-candidateDirs : String -> String -> PkgVersionBounds ->
-                IO (List (String, Maybe PkgVersion))
-candidateDirs dname pkg bounds =
-  mapMaybe (checkBounds <=< checkTTCVersion) <$> getPackageDirs dname
-
-  where checkBounds : PkgDir -> Maybe (String, Maybe PkgVersion)
-        checkBounds (MkPkgDir dirName pkgName ver _) =
-          do guard (pkgName == pkg && inBounds ver bounds)
-             pure ((dname </> dirName), ver)
+candidateDirs :
+    Ref Ctxt Defs =>
+    String -> String -> PkgVersionBounds ->
+    Core (List (String, Maybe PkgVersion))
+candidateDirs dname pkgName bounds = do
+  dirs <- coreLift (getPackageDirs dname)
+  checkedDirs <- traverse check dirs
+  pure (catMaybes checkedDirs)
 
-        checkTTCVersion : PkgDir -> Maybe PkgDir
-        checkTTCVersion pkg = if ttcVersion `elem` pkg.ttcVersions
-                                 then Just pkg
-                                 else Nothing
+  where
+    data CandidateError = OutOfBounds | TTCMismatch
+
+    checkNameAndBounds : PkgDir -> Either CandidateError PkgDir
+    checkNameAndBounds pkg =
+      if pkg.pkgName == pkgName && inBounds pkg.version bounds
+         then Right pkg
+         else Left OutOfBounds
+
+    checkTTCVersion : PkgDir -> Either CandidateError PkgDir
+    checkTTCVersion pkg =
+      if ttcVersion `elem` pkg.ttcVersions
+         then Right pkg
+         else Left TTCMismatch
+
+    unpack : PkgDir -> (String, Maybe PkgVersion)
+    unpack (MkPkgDir dirName pkgName ver _) =
+      ((dname </> dirName), ver)
+
+    check : PkgDir -> Core (Maybe (String, Maybe PkgVersion))
+    check pkg =
+      let checkedPkg = checkNameAndBounds pkg >>= checkTTCVersion
+      in
+      case checkedPkg of
+        Right pkg'       => pure . Just $ unpack pkg'
+        Left OutOfBounds => pure Nothing
+        Left TTCMismatch => do
+          let pkgVersion = maybe "unversioned" (\v => "version \{show v} of") pkg.version
+          recordWarning $ GenericWarn EmptyFC $
+                 """
+                 Found \{pkgVersion} package \{pkg.pkgName} installed with no compatible binaries for the current Idris2 compiler.
+
+                 Reinstall \{pkg.pkgName} with the current Idris2 compiler to resolve the issue.
+                 """
+          pure Nothing
 
 ||| Find all package directories (plus version) matching
 ||| the given package name and version bounds. Results
@@ -123,10 +153,10 @@ findPkgDirs p bounds = do
   localdir <- pkgLocalDirectory
 
   -- Get candidate directories from the local package directory
-  locFiles <- coreLift $ candidateDirs localdir p bounds
+  locFiles <- candidateDirs localdir p bounds
   -- Look in all the package paths too
   d <- getDirs
-  pkgFiles <- coreLift $ traverse (\d => candidateDirs d p bounds) d.package_search_paths
+  pkgFiles <- traverse (\d => candidateDirs d p bounds) d.package_search_paths
 
   -- If there's anything locally, use that and ignore the global ones
   let allFiles = if isNil locFiles