[fix] Package Search Paths (#3214)

* differentiate between search paths and package directories.

* fix :package repl command

* fix typo that caused Idris to look for library files in the wrong place when testing.

* Add to the changelog

CHANGELOG_NEXT.md

@@ -40,6 +40,14 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 ### Compiler changes
 
+* The compiler now differentiates between "package search path" and "package
+  directories." Previously both were combined (as seen in the `idris2 --paths`
+  output for "Package Directories"). Now entries in the search path will be
+  printed under an "Package Search Paths" entry and package directories will
+  continue to be printed under "Package Directories." The `IDRIS2_PACKAGE_PATH`
+  environment variable adds to the "Package Search Paths." Functionally this is
+  not a breaking change.
+
 #### RefC Backend
 
 * Fix invalid memory read onf strSubStr.

src/Core/Context.idr

@@ -2144,6 +2144,10 @@ export
 addPackageDir: {auto c : Ref Ctxt Defs} -> String -> Core ()
 addPackageDir dir = update Ctxt { options->dirs->package_dirs $= ((::) dir) . filter (/= dir) }
 
+export
+addPackageSearchPath: {auto c : Ref Ctxt Defs} -> String -> Core ()
+addPackageSearchPath dir = update Ctxt { options->dirs->package_search_paths $= ((::) dir) . filter (/= dir) }
+
 export
 addDataDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
 addDataDir dir = update Ctxt { options->dirs->data_dirs $= (++ [dir]) }

src/Core/Options.idr

@@ -24,7 +24,8 @@ 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_dirs : List String -- places to look for packages
+  package_search_paths : List String -- 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
 
@@ -38,7 +39,7 @@ outputDirWithDefault d = fromMaybe (build_dir d </> "exec") (output_dir d)
 
 public export
 toString : Dirs -> String
-toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs pdirs ldirs ddirs) = """
+toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs ppaths pdirs ldirs ddirs) = """
   + Working Directory      :: \{ show wdir }
   + Source Directory       :: \{ show sdir }
   + Build Directory        :: \{ show bdir }
@@ -46,6 +47,7 @@ toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs pdirs ldirs ddirs) = """
   + Output Directory       :: \{ show $ outputDirWithDefault d }
   + Installation Prefix    :: \{ show dfix }
   + Extra Directories      :: \{ show edirs }
+  + Package Search Paths   :: \{ show ppaths }
   + Package Directories    :: \{ show pdirs }
   + CG Library Directories :: \{ show ldirs }
   + Data Directories       :: \{ show ddirs }
@@ -214,7 +216,7 @@ getCG o cg = lookup (toLower cg) (availableCGs o)
 
 defaultDirs : Dirs
 defaultDirs = MkDirs "." Nothing "build" "depends" Nothing
-                     "/usr/local" ["."] [] [] []
+                     "/usr/local" ["."] [] [] [] []
 
 defaultPPrint : PPrinter
 defaultPPrint = MkPPOpts False False True False

src/Idris/Driver.idr

@@ -62,7 +62,7 @@ updateEnv
          blibs <- coreLift $ idrisGetEnv "IDRIS2_LIBS"
          whenJust blibs $ traverseList1_ addLibDir . splitPaths
          pdirs <- coreLift $ idrisGetEnv "IDRIS2_PACKAGE_PATH"
-         whenJust pdirs $ traverseList1_ addPackageDir . splitPaths
+         whenJust pdirs $ traverseList1_ addPackageSearchPath . splitPaths
          cg <- coreLift $ idrisGetEnv "IDRIS2_CG"
          whenJust cg $ \ e => case getCG (options defs) e of
            Just cg => setCG cg
@@ -76,6 +76,9 @@ updateEnv
          -- for the tests means they test the local version not the installed
          -- version
          defs <- get Ctxt
+         -- add global package path to the package search paths (after those
+         -- added by the user with IDRIS2_PACKAGE_PATH)
+         addPackageSearchPath !pkgGlobalDirectory
          -- These might fail while bootstrapping
          catch (addPkgDir "prelude" anyBounds) (const (pure ()))
          catch (addPkgDir "base" anyBounds) (const (pure ()))

src/Idris/REPL.idr

@@ -1080,7 +1080,7 @@ process (ImportPackage package) = do
   defs <- get Ctxt
   searchDirs <- extraSearchDirectories
   let Just packageDir = find
-        (\d => isInfixOf package (fromMaybe d (fileName d)))
+        (\d => isInfixOf package (fromMaybe d $ fileName =<< parent d))
         searchDirs
     | _ => pure (REPLError "Package not found in the known search directories")
   let packageDirPath = parse packageDir

src/Idris/SetOptions.idr

@@ -80,6 +80,9 @@ candidateDirs dname pkg bounds =
 ||| Find all package directories (plus version) matching
 ||| the given package name and version bounds. Results
 ||| will be sorted with the latest package version first.
+|||
+||| All package _search paths_ will be searched for package
+||| _directories_ that fit the requested critera.
 export
 findPkgDirs :
     Ref Ctxt Defs =>
@@ -87,20 +90,17 @@ findPkgDirs :
     PkgVersionBounds ->
     Core (List (String, Maybe PkgVersion))
 findPkgDirs p bounds = do
-  globaldir <- pkgGlobalDirectory
   localdir <- pkgLocalDirectory
 
-  -- Get candidate directories from the global install location,
-  -- and the local package directory
+  -- Get candidate directories from the local package directory
   locFiles <- coreLift $ candidateDirs localdir p bounds
-  globFiles <- coreLift $ candidateDirs globaldir p bounds
   -- Look in all the package paths too
   d <- getDirs
-  pkgFiles <- coreLift $ traverse (\d => candidateDirs d p bounds) (package_dirs d)
+  pkgFiles <- coreLift $ 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
-                    then globFiles ++ concat pkgFiles
+                    then concat pkgFiles
                     else locFiles
   -- Sort in reverse order of version number
   pure $ sortBy (\x, y => compare (snd y) (snd x)) allFiles
@@ -122,6 +122,8 @@ findPkgDir p bounds = do
      then pure Nothing
      else throw (CantFindPackage (p ++ " (" ++ show bounds ++ ")"))
 
+||| Attempt to find and add a package with the given name and bounds
+||| in one of the known package paths.
 export
 addPkgDir : {auto c : Ref Ctxt Defs} ->
             String -> PkgVersionBounds -> Core ()
@@ -143,14 +145,11 @@ visiblePackages dir = filter viable <$> getPackageDirs dir
 
 findPackages : {auto c : Ref Ctxt Defs} -> Core (List PkgDir)
 findPackages
-    = do -- global packages
-         globalPkgs <- coreLift $ visiblePackages !pkgGlobalDirectory
-         -- additional packages in directories specified
-         d <- getDirs
-         additionalPkgs <- coreLift $ traverse (\d => visiblePackages d) (package_dirs d)
+    = do d <- getDirs
+         pkgPathPkgs <- coreLift $ traverse (\d => visiblePackages d) d.package_search_paths
          -- local packages
          localPkgs <- coreLift $ visiblePackages !pkgLocalDirectory
-         pure $ globalPkgs ++ join additionalPkgs ++ localPkgs
+         pure $ localPkgs ++ join pkgPathPkgs
 
 listPackages : {auto c : Ref Ctxt Defs} ->
                {auto o : Ref ROpts REPLOpts} ->

tests/testutils.sh

@@ -99,7 +99,7 @@ if [ -z "$PREFIX_CHANGED" ] && [ -n "$IDRIS2_PREFIX" ]; then
     export IDRIS2_PACKAGE_PATH="$OLD_PP$SEP$NEW_PP"
     # Use TEST_IDRIS2_LIBS and TEST_IDRIS2_DATA to pass locations for
     # prebuilt libidris2_support and its DATA files.
-    export IDRIS2_LIBS="$OLD_PP/libs$SEP$NEW_PP/libs$SEP$TEST_IDRIS2_LIBS"
+    export IDRIS2_LIBS="$OLD_PP/lib$SEP$NEW_PP/lib$SEP$TEST_IDRIS2_LIBS"
     export IDRIS2_DATA="$OLD_PP/support$SEP$NEW_PP/support$SEP$TEST_IDRIS2_DATA"
 
     # Set where to install stuff