Improve package dependency error (#3445)

src/Core/Context.idr

@@ -12,6 +12,7 @@ import public Core.Options.Log
 import public Core.TT
 
 import Libraries.Utils.Binary
+import Libraries.Utils.Path
 import Libraries.Utils.Scheme
 import Libraries.Text.PrettyPrint.Prettyprinter
 
@@ -2160,7 +2161,9 @@ addPackageDir dir = update Ctxt { options->dirs->package_dirs $= ((::) dir) . fi
 
 export
 addPackageSearchPath: {auto c : Ref Ctxt Defs} -> String -> Core ()
-addPackageSearchPath dir = update Ctxt { options->dirs->package_search_paths $= ((::) dir) . filter (/= dir) }
+addPackageSearchPath dir =
+  let newPath = parse dir
+   in update Ctxt { options->dirs->package_search_paths $= ((::) newPath) . filter (/= newPath) }
 
 export
 addDataDir : {auto c : Ref Ctxt Defs} -> String -> Core ()

src/Core/Options.idr

@@ -24,7 +24,7 @@ record Dirs where
   output_dir : Maybe String -- output directory, relative to working directory
   prefix_dir : String -- installation prefix, for finding data files (e.g. run time support)
   extra_dirs : List String -- places to look for import files
-  package_search_paths : List String -- paths at which to look for packages
+  package_search_paths : List Path -- paths at which to look for packages
   package_dirs : List String -- places where specific needed packages at required versions are located
   lib_dirs : List String -- places to look for libraries (for code generation)
   data_dirs : List String -- places to look for data file

src/Idris/Package.idr

@@ -332,16 +332,19 @@ prepend : Candidate -> ResolutionError -> ResolutionError
 prepend p = { decisions $= (p ::)}
 
 reason : Maybe PkgVersion -> String
-reason Nothing  = "no matching version is installed"
-reason (Just x) = "assigned version \{show x} which is out of bounds"
-
+reason Nothing  = "no matching version is installed."
+reason (Just x) = "only found version \{show x} which is out of bounds."
 
 printResolutionError : ResolutionError -> String
 printResolutionError (MkRE ds d v) = go [<] ds
   where go : SnocList String -> List Candidate -> String
         go ss []        =
-          let pre    := "required \{d.pkgname} \{show d.pkgbounds} but"
-           in fastConcat . intersperse "; " $ ss <>> ["\{pre} \{reason v}"]
+          let pre        := "Required \{d.pkgname} \{show d.pkgbounds} but"
+              failure    := "\{pre} \{reason v}"
+              candidates := case ss of
+                               [<] => ""
+                               ss  => " Resolved transitive dependencies: " ++ (fastConcat $ intersperse "; " $ cast ss) ++ "."
+           in failure ++ candidates
         go ss (c :: cs) =
           let v := fromMaybe defaultVersion c.version
            in go (ss :< "\{c.name}-\{show v}") cs
@@ -350,10 +353,17 @@ data ResolutionRes : Type where
   Resolved : List String -> ResolutionRes
   Failed   : List ResolutionError -> ResolutionRes
 
-printErrs : PkgDesc -> List ResolutionError -> String
-printErrs x es =
-  unlines $  "Failed to resolve the dependencies for \{x.name}:"
-          :: map (indent 2 . printResolutionError) es
+printErrs : (pkgDirs : List String) -> PkgDesc -> List ResolutionError -> String
+printErrs pkgDirs x es =
+  let errors := unlines $ "Failed to resolve the dependencies for \{x.name}:"
+                          :: map (indent 2 . printResolutionError) es
+      dirs   := unlines $ "Searched for packages in:"
+                          :: map (indent 2) pkgDirs
+  in """
+     \{errors}
+     \{dirs}
+     For more details on what packages Idris2 can locate, run `idris2 --list-packages`
+     """
 
 -- try all possible resolution paths, keeping the first
 -- that works
@@ -369,6 +379,14 @@ tryAll ps f = go [<] ps
           Failed errs <- f x | Resolved res => pure (Resolved res)
           go (se <>< map (prepend x) errs) xs
 
+pkgDirs :
+    {auto c : Ref Ctxt Defs} ->
+    Core (List String)
+pkgDirs = do
+  localdir <- pkgLocalDirectory
+  d <- getDirs
+  pure (localdir ::  (show <$> d.package_search_paths))
+
 ||| Add all dependencies (transitively) from the given package file into the
 ||| context so modules from each is accessible during compilation.
 addDeps :
@@ -379,7 +397,7 @@ addDeps :
     Core ()
 addDeps pkg = do
   Resolved allPkgs <- getTransitiveDeps pkg.depends empty
-    | Failed errs => throw $ GenericMsg EmptyFC (printErrs pkg errs)
+    | Failed errs => throw $ GenericMsg EmptyFC (printErrs !pkgDirs pkg errs)
   log "package.depends" 10 $ "all depends: \{show allPkgs}"
   traverse_ addPackageDir allPkgs
   traverse_ addDataDir ((</> "data") <$> allPkgs)

src/Idris/SetOptions.idr

@@ -156,7 +156,7 @@ findPkgDirs p bounds = do
   locFiles <- candidateDirs localdir p bounds
   -- Look in all the package paths too
   d <- getDirs
-  pkgFiles <- traverse (\d => candidateDirs d p bounds) d.package_search_paths
+  pkgFiles <- traverse (\d => candidateDirs (show d) p bounds) d.package_search_paths
 
   -- If there's anything locally, use that and ignore the global ones
   let allFiles = if isNil locFiles
@@ -206,7 +206,7 @@ visiblePackages dir = map (MkQualifiedPkgDir dir) <$> filter viable <$> getPacka
 findPackages : {auto c : Ref Ctxt Defs} -> Core (List QualifiedPkgDir)
 findPackages
     = do d <- getDirs
-         pkgPathPkgs <- coreLift $ traverse (\d => visiblePackages d) d.package_search_paths
+         pkgPathPkgs <- coreLift $ traverse (\d => visiblePackages $ show d) d.package_search_paths
          -- local packages
          localPkgs <- coreLift $ visiblePackages !pkgLocalDirectory
          pure $ localPkgs ++ join pkgPathPkgs
@@ -228,14 +228,14 @@ listPackages
     pkgTTCVersions (MkPkgDir _ _ _ ttcVersions) =
       pretty0 "├ TTC Versions:" <++> prettyTTCVersions
       where
-        colorize : Int -> Doc IdrisAnn
-        colorize version =
+        annotate : Int -> Doc IdrisAnn
+        annotate version =
           if version == ttcVersion
              then pretty0 $ show version
-             else warning (pretty0 $ show version)
+             else warning ((pretty0 $ show version) <++> (parens "incompatible"))
 
         prettyTTCVersions : Doc IdrisAnn
-        prettyTTCVersions = (concatWith (\x,y => x <+> "," <++> y)) $ colorize <$> sort ttcVersions
+        prettyTTCVersions = (concatWith (\x,y => x <+> "," <++> y)) $ annotate <$> sort ttcVersions
 
     pkgPath : String -> Doc IdrisAnn
     pkgPath path = pretty0 "└ \{path}"

tests/idris2/pkg/pkg006/expected

@@ -1,7 +1,21 @@
 Error: Failed to resolve the dependencies for test3:
-  required foo >= 0.4 && < 0.5 but no matching version is installed
+  Required foo >= 0.4 && < 0.5 but no matching version is installed.
+
+Searched for packages in:
+  [...]/tests/idris2/pkg/pkg006/depends
+  [...]/tests/idris2/pkg/pkg006/prefix/idris2-0.7.0
+  [...]/build/env/idris2-0.7.0
+
+For more details on what packages Idris2 can locate, run `idris2 --list-packages`
 
 Error: Failed to resolve the dependencies for test4:
-  required baz any but no matching version is installed
+  Required baz any but no matching version is installed.
+
+Searched for packages in:
+  [...]/tests/idris2/pkg/pkg006/depends
+  [...]/tests/idris2/pkg/pkg006/prefix/idris2-0.7.0
+  [...]/build/env/idris2-0.7.0
+
+For more details on what packages Idris2 can locate, run `idris2 --list-packages`
 
 Warning: Deprecation warning: version numbers must now be of the form x.y.z

tests/idris2/pkg/pkg006/run

@@ -7,11 +7,17 @@ for folder in ./depends/*; do
   mkdir -p "${folder}/${TTC_VERSION}"
 done
 
-idris2 --build test1.ipkg 2>&1
-idris2 --build test2.ipkg 2>&1
-idris2 --build test3.ipkg 2>&1
-idris2 --build test4.ipkg 2>&1
-idris2 --build test5.ipkg 2>&1
+TEST_FOLDER_PREFIX="$(cd ../../../.. && pwd | windows_path_tweaks | sed "s#/d#D:#g")"
+
+fix_path() {
+  windows_path_tweaks | sed "s#$TEST_FOLDER_PREFIX#[...]#g"
+}
+
+idris2 --build test1.ipkg 2>&1 | fix_path
+idris2 --build test2.ipkg 2>&1 | fix_path
+idris2 --build test3.ipkg 2>&1 | fix_path
+idris2 --build test4.ipkg 2>&1 | fix_path
+idris2 --build test5.ipkg 2>&1 | fix_path
 
 for folder in ./depends/*; do
   rmdir "${folder}/${TTC_VERSION}"

tests/idris2/pkg/pkg015/expected

@@ -1,6 +1,13 @@
 Error: Failed to resolve the dependencies for test:
-  foo-0.2.0; baz-0.3.0; required quux any but no matching version is installed
-  foo-0.2.0; baz-0.2.0; bar-0.1.1; required baz < 0.2.0 but assigned version 0.2.0 which is out of bounds
-  foo-0.2.0; baz-0.2.0; bar-0.1.0; required prz > 0.1.0 but no matching version is installed
-  foo-0.1.0; required baz < 0.1.0 but no matching version is installed
+  Required quux any but no matching version is installed. Resolved transitive dependencies: foo-0.2.0; baz-0.3.0.
+  Required baz < 0.2.0 but only found version 0.2.0 which is out of bounds. Resolved transitive dependencies: foo-0.2.0; baz-0.2.0; bar-0.1.1.
+  Required prz > 0.1.0 but no matching version is installed. Resolved transitive dependencies: foo-0.2.0; baz-0.2.0; bar-0.1.0.
+  Required baz < 0.1.0 but no matching version is installed. Resolved transitive dependencies: foo-0.1.0.
+
+Searched for packages in:
+  [...]/tests/idris2/pkg/pkg015/depends
+  [...]/tests/idris2/pkg/pkg015/prefix/idris2-0.7.0
+  [...]/build/env/idris2-0.7.0
+
+For more details on what packages Idris2 can locate, run `idris2 --list-packages`
 

tests/idris2/pkg/pkg015/run

@@ -7,7 +7,13 @@ for folder in ./depends/*; do
   mkdir -p "${folder}/${TTC_VERSION}"
 done
 
-idris2 --build test.ipkg --log package.depends:10 2>&1
+TEST_FOLDER_PREFIX="$(cd ../../../.. && pwd | windows_path_tweaks | sed "s#/d#D:#g")"
+
+fix_path() {
+  windows_path_tweaks | sed "s#$TEST_FOLDER_PREFIX#[...]#g"
+}
+
+idris2 --build test.ipkg --log package.depends:10 2>&1 | fix_path
 
 for folder in ./depends/*; do
   rmdir "${folder}/${TTC_VERSION}"

tests/idris2/pkg/pkg020/run

@@ -1,14 +1,10 @@
 . ../../../testutils.sh
 
-windows_tweaks() {
-  sed 's#C:.msys64##' | sed 's#\\#/#g'
-}
-
 # pretend Idris2 is installed at root for reproducible
 # installdirs:
 IDRIS2_PREFIX=/ idris2 --dump-installdir test.ipkg \
-  | windows_tweaks
+  | windows_path_tweaks
 
 # by contrast, the location containing all installed packages:
 IDRIS2_PREFIX=/ idris2 --libdir \
-  | windows_tweaks
+  | windows_path_tweaks

tests/testutils.sh

@@ -40,6 +40,10 @@ sed_literal() {
     printf '%s\n' "$1" | sed -e 's/[]\/$*.^[]/\\&/g'
 }
 
+windows_path_tweaks() {
+    sed 's#C:.msys64##' | sed 's#\\#/#g'
+}
+
 # used below to normalise machine names
 # shellcheck disable=SC2016
 _awk_clean_name='