Merge pull request #1137 from edwinb/packagepath

Add IDRIS2_PACKAGE_PATH environment variable

CHANGELOG.md

@@ -15,6 +15,8 @@ Other changes:
   dots (e.g. `1.0`, `0.3.0`, `3.1.4.1.5` etc)
 * Idris now looks in the current working directory, under a subdirectory
   `depends` for local installations of packages before looking globally.
+* Added an environment variable `IDRIS2_PACKAGE_PATH` for extending where to
+  look for packages.
 
 Changes since Idris 2 v0.2.1
 ----------------------------

docs/source/reference/envvars.rst

@@ -6,4 +6,29 @@ Environment Variables
 
 .. todo::
 
-   Fill in the environment variables recognised by Idris 2
+Idris 2 recognises a number of environment variables, to decide where to look
+for packages, external libraries, code generators, etc. It currently recognises,
+in approximately the order you're likely to need them:
+
+* ``EDITOR`` - Sets the editor used in REPL :e command
+* ``IDRIS2_CG`` - Sets which code generator to use when compiling programs
+* ``IDRIS2_PACKAGE_PATH`` - Lists the directories where Idris2 looks for packages,
+  in addition to the defaults (which are under the ``IDRIS2_PREFIX`` and in the
+  ``depends`` subdirectory of the current working directory).
+  Directories are separated by a ``:``, or a ``;`` on Windows
+* ``IDRIS2_PATH`` - Places Idris2 looks for import files, in addition to the
+  imports in packages
+* ``IDRIS2_DATA`` - Places Idris2 looks for its data files. These are typically
+  support code for code generators.
+* ``IDRIS2_LIBS`` - Places Idris2 looks for libraries used by code generators.
+* ``IDRIS2_PREFIX`` - Gives the Idris2 installation prefix
+* ``CHEZ`` - Sets the location of the ``chez`` executable used in Chez codegen
+* ``RACKET`` - Sets the location of the ``racket`` executable used in Racket codegen
+* ``RACKET_RACO`` - Sets the location of the ``raco`` executable used in Racket codegen
+* ``GAMBIT_GSI`` - Sets the location of the ``gsi`` executable used in Gambit codegen
+* ``GAMBIT_GSC`` - Sets the location of the ``gsc`` executable used in Gambit codegen
+* ``GAMBIT_GSC_BACKEND`` - Sets the ``gsc`` executable backend argument
+* ``IDRIS2_CC`` - Sets the location of the C compiler executable used in RefC codegen
+* ``CC`` - Sets the location of the C compiler executable used in RefC codegen
+* ``NODE`` - Sets the location of the ``node`` executable used in Node codegen
+* ``PATH`` - used to search for executables in certain codegens

src/Core/Context.idr

@@ -2017,6 +2017,12 @@ addExtraDir dir
     = do defs <- get Ctxt
          put Ctxt (record { options->dirs->extra_dirs $= (++ [dir]) } defs)
 
+export
+addPackageDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
+addPackageDir dir
+    = do defs <- get Ctxt
+         put Ctxt (record { options->dirs->package_dirs $= (++ [dir]) } defs)
+
 export
 addDataDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
 addDataDir dir

src/Core/Options.idr

@@ -25,6 +25,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_dirs : List String -- places to look for packages
   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 ldirs ddirs) =
+toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs pdirs ldirs ddirs) =
   unlines [ "+ 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 ldirs ddirs) =
           , "+ Output Directory       :: " ++ show (outputDirWithDefault d)
           , "+ Installation Prefix    :: " ++ show dfix
           , "+ Extra Directories      :: " ++ show edirs
+          , "+ Package Directories    :: " ++ show pdirs
           , "+ CG Library Directories :: " ++ show ldirs
           , "+ Data Directories       :: " ++ show ddirs]
 
@@ -181,7 +183,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 True False

src/Idris/Driver.idr

@@ -62,6 +62,10 @@ updateEnv
          the (Core ()) $ case blibs of
               Just path => do traverseList1_ addLibDir (map trim (split (==pathSeparator) path))
               Nothing => pure ()
+         pdirs <- coreLift $ idrisGetEnv "IDRIS2_PACKAGE_PATH"
+         the (Core ()) $ case pdirs of
+              Just path => do traverseList1_ addPackageDir (map trim (split (==pathSeparator) path))
+              Nothing => pure ()
          cg <- coreLift $ idrisGetEnv "IDRIS2_CG"
          the (Core ()) $ case cg of
               Just e => case getCG (options defs) e of

src/Idris/Env.idr

@@ -21,6 +21,7 @@ envs = [
          MkEnvDesc "EDITOR"        "Editor used in REPL :e command",
          MkEnvDesc "IDRIS2_PREFIX" "Idris2 installation prefix",
          MkEnvDesc "IDRIS2_PATH"   "Places Idris2 looks for import files",
+         MkEnvDesc "IDRIS2_PACKAGE_PATH" "Places Idris2 looks for packages",
          MkEnvDesc "IDRIS2_DATA"   "Places Idris2 looks for data files",
          MkEnvDesc "IDRIS2_LIBS"   "Places Idris2 looks for libraries (for code generation)",
          MkEnvDesc "IDRIS2_CG"     "Codegen backend",

src/Idris/SetOptions.idr

@@ -81,10 +81,13 @@ addPkgDir p bounds
          -- and the local package directory
          locFiles <- coreLift $ candidateDirs localdir p bounds
          globFiles <- coreLift $ candidateDirs globaldir p bounds
+         -- Look in all the package paths too
+         let pkgdirs = (options defs).dirs.package_dirs
+         pkgFiles <- coreLift $ traverse (\d => candidateDirs d p bounds) pkgdirs
 
          -- If there's anything locally, use that and ignore the global ones
          let allFiles = if isNil locFiles
-                           then globFiles
+                           then globFiles ++ concat pkgFiles
                            else locFiles
          -- Sort in reverse order of version number
          let sorted = sortBy (\x, y => compare (snd y) (snd x)) allFiles