[ new ] idris2 --init (#1299)

idris2api.ipkg

@@ -71,7 +71,11 @@ modules =
     Idris.Driver,
     Idris.Error,
     Idris.ModTree,
+
     Idris.Package,
+    Idris.Package.Init,
+    Idris.Package.Types,
+
     Idris.Parser,
     Idris.Parser.Let,
     Idris.Pretty,
@@ -119,6 +123,8 @@ modules =
     Libraries.Data.StringMap,
     Libraries.Data.StringTrie,
 
+    Libraries.System.Directory.Tree,
+
     Libraries.Text.Bounded,
     Libraries.Text.Distance.Levenshtein,
     Libraries.Text.Lexer,

libs/contrib/System/Directory/Tree.idr

@@ -0,0 +1,169 @@
+module System.Directory.Tree
+
+import Data.DPair
+import Data.List
+import Data.Nat
+import Data.Strings
+import System.Directory
+import System.Path
+
+%default total
+
+------------------------------------------------------------------------------
+-- Filenames
+
+||| A `Filename root` is  anchored in `root`.
+||| We use a `data` type so that Idris can easily infer `root` when passing
+||| a `FileName` around. We do not use a `record` because we do not want to
+||| allow users to manufacture their own `FileName`.
+||| To get an absolute path, we need to append said filename to the root.
+export
+data FileName : Path -> Type where
+  MkFileName : String -> FileName root
+
+||| Project the string out of a `FileName`.
+export
+fileName : FileName root -> String
+fileName (MkFileName str) = str
+
+||| Convert a filename anchored in `root` to a filepath by appending the name
+||| to the root path.
+export
+toFilePath : {root : Path} -> FileName root -> String
+toFilePath file = show (root /> fileName file)
+
+export
+directoryExists : {root : Path} -> FileName root -> IO Bool
+directoryExists fp = do
+  Right dir <- openDir (toFilePath fp)
+    | Left _ => pure False
+  closeDir dir
+  pure True
+
+------------------------------------------------------------------------------
+-- Directory trees
+
+||| A `Tree root` is the representation of a directory tree anchored in `root`.
+||| Each directory contains a list of files and a list of subtrees waiting to be
+||| explored. The fact these subtrees are IO-bound means the subtrees will be
+||| lazily constructed on demand.
+public export
+SubTree : Path -> Type
+
+public export
+record Tree (root : Path) where
+  constructor MkTree
+  files    : List (FileName root)
+  subTrees : List (SubTree root)
+
+SubTree root = (dir : FileName root ** IO (Tree (root /> fileName dir)))
+
+||| An empty tree contains no files and has no sub-directories.
+export
+emptyTree : Tree root
+emptyTree = MkTree [] []
+
+||| Filter out files and directories that do not satisfy a given predicate.
+export
+filter : (filePred, dirPred : {root : _} -> FileName root -> Bool) ->
+         {root : _} -> Tree root -> Tree root
+filter filePred dirPred (MkTree files dirs) = MkTree files' dirs' where
+
+  files' : List (FileName root)
+  files' = filter filePred files
+
+  dirs' : List (SubTree root)
+  dirs' = flip mapMaybe dirs $ \ (dname ** iot) => do
+            guard (dirPred dname)
+            pure (dname ** map (assert_total (filter filePred dirPred)) iot)
+
+||| Sort the lists of files and directories using the given comparison functions
+export
+sortBy : (fileCmp, dirCmp : {root : _} -> FileName root -> FileName root -> Ordering) ->
+         {root : _} -> Tree root -> Tree root
+sortBy fileCmp dirCmp (MkTree files dirs) = MkTree files' dirs' where
+
+  files' : List (FileName root)
+  files' = sortBy fileCmp files
+
+  dirs' : List (SubTree root)
+  dirs' = sortBy (\ d1, d2 => dirCmp (fst d1) (fst d2))
+        $ flip map dirs $ \ (dname ** iot) =>
+          (dname ** map (assert_total (sortBy fileCmp dirCmp)) iot)
+
+||| Sort the list of files and directories alphabetically
+export
+sort : {root : _} -> Tree root -> Tree root
+sort = sortBy cmp cmp where
+
+  cmp : {root : _} -> FileName root -> FileName root -> Ordering
+  cmp a b = compare (fileName a) (fileName b)
+
+
+||| Exploring a filesystem from a given root to produce a tree
+export
+explore : (root : Path) -> IO (Tree root)
+
+go : {root : Path} -> Directory -> Tree root -> IO (Tree root)
+
+explore root = do
+  Right dir <- openDir (show root)
+    | Left err => pure emptyTree
+  assert_total (go dir emptyTree)
+
+go dir acc = case !(dirEntry dir) of
+  -- If there is no next entry then we are done and can return the accumulator.
+  Left err => acc <$ closeDir dir
+  -- Otherwise we have an entry and need to categorise it
+  Right entry => do
+    -- ignore aliases for current and parent directories
+    let False = elem entry [".", ".."]
+         | _ => assert_total (go dir acc)
+    -- if the entry is a directory, add it to the (lazily explored)
+    -- list of subdirectories
+    let entry : FileName root = MkFileName entry
+    let acc = if !(directoryExists entry)
+                then { subTrees $= ((entry ** explore _) ::) } acc
+                else { files    $= (entry                ::) } acc
+    assert_total (go dir acc)
+
+
+||| Display a tree by printing it procedurally. Note that because directory
+||| trees contain suspended computations corresponding to their subtrees this
+||| has to be an `IO` function. We make it return Unit rather than a String
+||| because we do not want to assume that the tree is finite.
+export
+covering
+print : Tree root -> IO ()
+print t = go [([], ".", Evidence root (pure t))] where
+
+  -- This implementation is unadulterated black magic.
+  -- Do NOT touch it if nothing is broken.
+
+  padding : Bool -> List Bool -> String
+  padding isDir = fastConcat . go [] where
+
+    go : List String -> List Bool -> List String
+    go acc [] = acc
+    go acc (b :: bs) = go (hd :: acc) bs where
+      hd : String
+      hd = if isDir && isNil acc
+           then if b then " ├ " else " └ "
+           else if b then " │"  else "  "
+
+  prefixes : Nat -> List Bool
+  prefixes n = snoc (replicate (pred n) True) False
+
+  covering
+  go : List (List Bool, String, Exists (IO . Tree)) -> IO ()
+  go [] = pure ()
+  go ((bs, fn, Evidence _ iot) :: iots) = do
+    t <- iot
+    putStrLn (padding True bs ++ fn)
+    let pad = padding False bs
+    let pads = prefixes (length t.files + length t.subTrees)
+    for_ (zip pads t.files) $ \ (b, fp) =>
+      putStrLn (pad ++ (if b then " ├ " else " └ ") ++ fileName fp)
+    let bss = map (:: bs) (prefixes (length t.subTrees))
+    go (zipWith (\ bs, (dir ** iot) => (bs, fileName dir, Evidence _ iot)) bss t.subTrees)
+    go iots

libs/contrib/System/Path.idr

@@ -13,7 +13,7 @@ import Text.Quantity
 
 import System.Info
 
-infixr 5 </>
+infixr 5 </>, />
 infixr 7 <.>
 
 
@@ -344,6 +344,7 @@ setFileName' name path =
   else
     append' path (parse name)
 
+export
 splitFileName : String -> (String, String)
 splitFileName name =
   case break (== '.') $ reverse $ unpack name of
@@ -373,6 +374,23 @@ export
 isRelative : String -> Bool
 isRelative = not . isAbsolute
 
+||| Appends the right path to the left path.
+|||
+||| If the path on the right is absolute, it replaces the left path.
+|||
+||| On Windows:
+|||
+||| - If the right path has a root but no volume (e.g., `\windows`), it replaces
+|||   everything except for the volume (if any) of left.
+||| - If the right path has a volume but no root, it replaces left.
+|||
+||| ```idris example
+||| parse "/usr" /> "local/etc" == "/usr/local/etc"
+||| ```
+export
+(/>) : (left : Path) -> (right : String) -> Path
+(/>) left right = append' left (parse right)
+
 ||| Appends the right path to the left path.
 |||
 ||| If the path on the right is absolute, it replaces the left path.
@@ -388,7 +406,7 @@ isRelative = not . isAbsolute
 ||| ```
 export
 (</>) : (left : String) -> (right : String) -> String
-(</>) left right = show $ append' (parse left) (parse right)
+(</>) left right = show $ parse left /> right
 
 ||| Joins path components into one.
 |||
@@ -397,7 +415,7 @@ export
 ||| ```
 export
 joinPath : List String -> String
-joinPath xs = foldl (</>) "" xs
+joinPath xs = show $ foldl (/>) (parse "") xs
 
 ||| Splits path into components.
 |||

libs/contrib/contrib.ipkg

@@ -145,6 +145,7 @@ modules = Control.ANSI,
           Syntax.PreorderReasoning.Generic,
 
           System.Console.GetOpt,
+          System.Directory.Tree,
           System.Future,
           System.Random,
           System.Path,

src/Idris/CommandLine.idr

@@ -9,6 +9,7 @@ import Core.Name.Namespace
 import Core.Options
 
 import Data.List
+import Data.List1
 import Data.Maybe
 import Data.Strings
 import Data.Either
@@ -24,6 +25,7 @@ data PkgCommand
       | Typecheck
       | Clean
       | REPL
+      | Init
 
 export
 Show PkgCommand where
@@ -32,6 +34,7 @@ Show PkgCommand where
   show Typecheck = "--typecheck"
   show Clean = "--clean"
   show REPL = "--repl"
+  show Init = "--init"
 
 public export
 data DirCommand
@@ -41,62 +44,6 @@ export
 Show DirCommand where
   show LibDir = "--libdir"
 
-public export
-data PkgVersion = MkPkgVersion (List Nat)
-
-export
-Show PkgVersion where
-  show (MkPkgVersion vs) = showSep "." (map show vs)
-
-export
-Eq PkgVersion where
-  MkPkgVersion p == MkPkgVersion q = p == q
-
-export
-Ord PkgVersion where
-  -- list ordering gives us what we want
-  compare (MkPkgVersion p) (MkPkgVersion q) = compare p q
-
--- version must be >= lowerBound and <= upperBound
--- Do we want < and > as well?
-public export
-record PkgVersionBounds where
-  constructor MkPkgVersionBounds
-  lowerBound : Maybe PkgVersion
-  lowerInclusive : Bool -- >= if true
-  upperBound : Maybe PkgVersion
-  upperInclusive : Bool -- <= if true
-
-export
-Show PkgVersionBounds where
-  show p = if noBounds p then "any"
-              else maybe "" (\v => (if p.lowerInclusive then ">= " else "> ")
-                                       ++ show v ++ " ") p.lowerBound ++
-                   maybe "" (\v => (if p.upperInclusive then "<= " else "< ") ++ show v) p.upperBound
-    where
-      noBounds : PkgVersionBounds -> Bool
-      noBounds p = isNothing p.lowerBound && isNothing p.upperBound
-
-export
-anyBounds : PkgVersionBounds
-anyBounds = MkPkgVersionBounds Nothing True Nothing True
-
-export
-current : PkgVersionBounds
-current = let (maj,min,patch) = semVer version
-              version = Just (MkPkgVersion [maj, min, patch]) in
-              MkPkgVersionBounds version True version True
-
-export
-inBounds : PkgVersion -> PkgVersionBounds -> Bool
-inBounds v bounds
-   = maybe True (\v' => if bounds.lowerInclusive
-                           then v >= v'
-                           else v > v') bounds.lowerBound &&
-     maybe True (\v' => if bounds.upperInclusive
-                           then v <= v'
-                           else v < v') bounds.upperBound
-
 ||| CLOpt - possible command line options
 public export
 data CLOpt
@@ -254,6 +201,10 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
               (Just "Show library directory"),
 
            optSeparator,
+           MkOpt ["--init"] [Optional "package file"]
+              (\ f => [Package Init (fromMaybe "" f)])
+              (Just "Interactively initialise a new project"),
+
            MkOpt ["--build"] [Required "package file"] (\f => [Package Build f])
               (Just "Build modules/executable for the given package"),
            MkOpt ["--install"] [Required "package file"] (\f => [Package Install f])

src/Idris/Package.idr

@@ -11,10 +11,7 @@ import Core.Unify
 
 import Data.List
 import Data.Maybe
-import Data.So
-import Libraries.Data.StringMap
 import Data.Strings
-import Libraries.Data.StringTrie
 import Data.These
 
 import Parser.Package
@@ -22,6 +19,8 @@ import System
 import System.Directory
 import System.File
 
+import Libraries.Data.StringMap
+import Libraries.Data.StringTrie
 import Libraries.Text.Parser
 import Libraries.Text.PrettyPrint.Prettyprinter
 import Libraries.Utils.Binary
@@ -39,6 +38,9 @@ import Idris.Syntax
 import Idris.Version
 import IdrisPaths
 
+import public Idris.Package.Types
+import Idris.Package.Init
+
 %hide Data.Strings.lines
 %hide Data.Strings.lines'
 %hide Data.Strings.unlines
@@ -46,81 +48,10 @@ import IdrisPaths
 
 %default covering
 
-public export
-record Depends where
-  constructor MkDepends
-  pkgname : String
-  pkgbounds : PkgVersionBounds
-
-export
-Show Depends where
-  show p = p.pkgname ++ " " ++ show p.pkgbounds
-
-public export
-record PkgDesc where
-  constructor MkPkgDesc
-  name : String
-  version : PkgVersion
-  authors : String
-  maintainers : Maybe String
-  license : Maybe String
-  brief   : Maybe String
-  readme  : Maybe String
-  homepage : Maybe String
-  sourceloc : Maybe String
-  bugtracker : Maybe String
-  depends : List Depends -- packages to add to search path
-  modules : List (ModuleIdent, String) -- modules to install (namespace, filename)
-  mainmod : Maybe (ModuleIdent, String) -- main file (i.e. file to load at REPL)
-  executable : Maybe String -- name of executable
-  options : Maybe (FC, String)
-  sourcedir : Maybe String
-  builddir : Maybe String
-  outputdir : Maybe String
-  prebuild : Maybe (FC, String) -- Script to run before building
-  postbuild : Maybe (FC, String) -- Script to run after building
-  preinstall : Maybe (FC, String) -- Script to run after building, before installing
-  postinstall : Maybe (FC, String) -- Script to run after installing
-  preclean : Maybe (FC, String) -- Script to run before cleaning
-  postclean : Maybe (FC, String) -- Script to run after cleaning
-
 installDir : PkgDesc -> String
-installDir p = name p ++ "-" ++ show (version p)
-
-export
-Show PkgDesc where
-  show pkg = "Package: " ++ name pkg ++ "\n" ++
-             "Version: " ++ show (version pkg) ++ "\n" ++
-             "Authors: " ++ authors pkg ++ "\n" ++
-             maybe "" (\m => "Maintainers: " ++ m ++ "\n") (maintainers pkg) ++
-             maybe "" (\m => "License: "     ++ m ++ "\n") (license pkg)     ++
-             maybe "" (\m => "Brief: "       ++ m ++ "\n") (brief pkg)       ++
-             maybe "" (\m => "ReadMe: "      ++ m ++ "\n") (readme pkg)      ++
-             maybe "" (\m => "HomePage: "    ++ m ++ "\n") (homepage pkg)    ++
-             maybe "" (\m => "SourceLoc: "   ++ m ++ "\n") (sourceloc pkg)   ++
-             maybe "" (\m => "BugTracker: "  ++ m ++ "\n") (bugtracker pkg)  ++
-             "Depends: " ++ show (depends pkg) ++ "\n" ++
-             "Modules: " ++ show (map snd (modules pkg)) ++ "\n" ++
-             maybe "" (\m => "Main: " ++ snd m ++ "\n") (mainmod pkg) ++
-             maybe "" (\m => "Exec: " ++ m ++ "\n") (executable pkg) ++
-             maybe "" (\m => "Opts: " ++ snd m ++ "\n") (options pkg) ++
-             maybe "" (\m => "SourceDir: " ++ m ++ "\n") (sourcedir pkg) ++
-             maybe "" (\m => "BuildDir: " ++ m ++ "\n") (builddir pkg) ++
-             maybe "" (\m => "OutputDir: " ++ m ++ "\n") (outputdir pkg) ++
-             maybe "" (\m => "Prebuild: " ++ snd m ++ "\n") (prebuild pkg) ++
-             maybe "" (\m => "Postbuild: " ++ snd m ++ "\n") (postbuild pkg) ++
-             maybe "" (\m => "Preinstall: " ++ snd m ++ "\n") (preinstall pkg) ++
-             maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg) ++
-             maybe "" (\m => "Preclean: " ++ snd m ++ "\n") (preclean pkg) ++
-             maybe "" (\m => "Postclean: " ++ snd m ++ "\n") (postclean pkg)
-
-initPkgDesc : String -> PkgDesc
-initPkgDesc pname
-    = MkPkgDesc pname (MkPkgVersion [0,0]) "Anonymous" Nothing Nothing
-                Nothing Nothing Nothing Nothing Nothing
-                [] []
-                Nothing Nothing Nothing Nothing Nothing Nothing Nothing Nothing
-                Nothing Nothing Nothing Nothing
+installDir p = name p
+            ++ "-"
+            ++ show (fromMaybe (MkPkgVersion (0 ::: [])) (version p))
 
 data DescField : Type where
   PVersion     : FC -> PkgVersion -> DescField
@@ -175,7 +106,7 @@ field fname
            vs <- sepBy1 dot' integerLit
            end <- location
            pure (PVersion (MkFC fname start end)
-                          (MkPkgVersion (fromInteger <$> forget vs)))
+                          (MkPkgVersion (fromInteger <$> vs)))
     <|> do start <- location
            ignore $ exactProperty "version"
            equals
@@ -210,20 +141,20 @@ field fname
     bound
         = do lte
              vs <- sepBy1 dot' integerLit
-             pure [LT (MkPkgVersion (fromInteger <$> forget vs)) True]
+             pure [LT (MkPkgVersion (fromInteger <$> vs)) True]
       <|> do gte
              vs <- sepBy1 dot' integerLit
-             pure [GT (MkPkgVersion (fromInteger <$> forget vs)) True]
+             pure [GT (MkPkgVersion (fromInteger <$> vs)) True]
       <|> do lt
              vs <- sepBy1 dot' integerLit
-             pure [LT (MkPkgVersion (fromInteger <$> forget vs)) False]
+             pure [LT (MkPkgVersion (fromInteger <$> vs)) False]
       <|> do gt
              vs <- sepBy1 dot' integerLit
-             pure [GT (MkPkgVersion (fromInteger <$> forget vs)) False]
+             pure [GT (MkPkgVersion (fromInteger <$> vs)) False]
       <|> do eqop
              vs <- sepBy1 dot' integerLit
-             pure [LT (MkPkgVersion (fromInteger <$> forget vs)) True,
-                   GT (MkPkgVersion (fromInteger <$> forget vs)) True]
+             pure [LT (MkPkgVersion (fromInteger <$> vs)) True,
+                   GT (MkPkgVersion (fromInteger <$> vs)) True]
 
     mkBound : List Bound -> PkgVersionBounds -> PackageEmptyRule PkgVersionBounds
     mkBound (LT b i :: bs) pkgbs
@@ -271,11 +202,11 @@ addField : {auto c : Ref Ctxt Defs} ->
            {auto p : Ref ParsedMods (List (FC, ModuleIdent))} ->
            {auto m : Ref MainMod (Maybe (FC, ModuleIdent))} ->
            DescField -> PkgDesc -> Core PkgDesc
-addField (PVersion fc n)     pkg = pure $ record { version = n } pkg
+addField (PVersion fc n)     pkg = pure $ record { version = Just n } pkg
 addField (PVersionDep fc n)  pkg
     = do emitWarning (Deprecated "version numbers must now be of the form x.y.z")
          pure pkg
-addField (PAuthors fc a)     pkg = pure $ record { authors = a } pkg
+addField (PAuthors fc a)     pkg = pure $ record { authors = Just a } pkg
 addField (PMaintainers fc a) pkg = pure $ record { maintainers = Just a } pkg
 addField (PLicense fc a)     pkg = pure $ record { license = Just a } pkg
 addField (PBrief fc a)       pkg = pure $ record { brief = Just a } pkg
@@ -595,33 +526,40 @@ processPackage : {auto c : Ref Ctxt Defs} ->
                  (PkgCommand, String) ->
                  Core ()
 processPackage opts (cmd, file)
-    =  if not (isSuffixOf ".ipkg" file)
-         then do coreLift $ putStrLn ("Packages must have an '.ipkg' extension: " ++ show file ++ ".")
-                 coreLift (exitWith (ExitFailure 1))
-         else do Right (pname, fs) <- coreLift $ parseFile file
-                                          (do desc <- parsePkgDesc file
-                                              eoi
-                                              pure desc)
-                    | Left err => throw err
-                 pkg <- addFields fs (initPkgDesc pname)
-                 maybe (pure ()) setBuildDir (builddir pkg)
-                 setOutputDir (outputdir pkg)
-                 case cmd of
-                      Build => do [] <- build pkg opts
-                                     | errs => coreLift (exitWith (ExitFailure 1))
-                                  pure ()
-                      Install => do [] <- build pkg opts
-                                       | errs => coreLift (exitWith (ExitFailure 1))
-                                    install pkg opts
-                      Typecheck => do
-                        [] <- check pkg opts
-                          | errs => coreLift (exitWith (ExitFailure 1))
-                        pure ()
-                      Clean => clean pkg opts
-                      REPL => do
-                        [] <- build pkg opts
-                           | errs => coreLift (exitWith (ExitFailure 1))
-                        runRepl (map snd $ mainmod pkg)
+    = case cmd of
+        Init =>
+          do pkg <- coreLift interactive
+             let fp = if file == "" then pkg.name ++ ".ipkg" else file
+             False <- coreLift (exists fp)
+               | _ => throw (GenericMsg emptyFC ("File " ++ fp ++ " already exists"))
+             Right () <- coreLift $ writeFile fp (show $ the (Doc ()) $ pretty pkg)
+               | Left err => throw (FileErr fp err)
+             pure ()
+        _ =>
+         do let True = isSuffixOf ".ipkg" file
+                 | _ => do coreLift $ putStrLn ("Packages must have an '.ipkg' extension: " ++ show file ++ ".")
+                           coreLift (exitWith (ExitFailure 1))
+            Right (pname, fs) <- coreLift $ parseFile file (parsePkgDesc file <* eoi)
+              | Left err => throw err
+            pkg <- addFields fs (initPkgDesc pname)
+            whenJust (builddir pkg) setBuildDir
+            setOutputDir (outputdir pkg)
+            case cmd of
+              Build => do [] <- build pkg opts
+                            | errs => coreLift (exitWith (ExitFailure 1))
+                          pure ()
+              Install => do [] <- build pkg opts
+                               | errs => coreLift (exitWith (ExitFailure 1))
+                            install pkg opts
+              Typecheck => do [] <- check pkg opts
+                                | errs => coreLift (exitWith (ExitFailure 1))
+                              pure ()
+              Clean => clean pkg opts
+              REPL => do [] <- build pkg opts
+                            | errs => coreLift (exitWith (ExitFailure 1))
+                         runRepl (map snd $ mainmod pkg)
+              Init => pure () -- already handled earlier
+
 
 record PackageOpts where
   constructor MkPFR

src/Idris/Package/Init.idr

@@ -0,0 +1,86 @@
+module Idris.Package.Init
+
+import Core.FC
+import Core.Name.Namespace
+
+import Data.List
+import Data.Maybe
+import Data.Strings
+
+import Idris.Package.Types
+import System.Directory
+
+import Libraries.Utils.Path
+import Libraries.System.Directory.Tree
+import Libraries.Text.PrettyPrint.Prettyprinter
+
+%default total
+
+isModuleIdent : String -> Bool
+isModuleIdent str = case unpack str of
+  [] => False
+  cs@(hd :: _) => isUpper hd && all isAlphaNum cs
+
+packageTree : (root : Path) -> IO (Tree root)
+packageTree root = filter validFile validDirectory <$> explore root where
+
+  validFile : {root : _} -> FileName root -> Bool
+  validFile f
+    = let (fname, fext) = splitFileName (fileName f) in
+      isModuleIdent fname && elem fext ["idr", "lidr"]
+
+  validDirectory : {root : _} -> FileName root -> Bool
+  validDirectory = isModuleIdent . fileName
+
+covering
+findModules : (start : Maybe String) -> IO (List (ModuleIdent, String))
+findModules start = do
+  let prfx = fromMaybe "" start
+  Just dir <- maybe currentDir (pure . Just) start
+    | Nothing => pure []
+  let root = parse dir
+  tree <- packageTree root
+  mods <- go [] [([], (root ** pure tree))]
+  pure (sortBy (\ a, b => compare (snd a) (snd b)) mods)
+
+  where
+
+    go : List (ModuleIdent, String) ->
+         List (List String, (root : Path ** IO (Tree root))) ->
+         IO (List (ModuleIdent, String))
+    go acc [] = pure acc
+    go acc ((path, (root ** iot)) :: iots) = do
+      t <- liftIO iot
+      let mods = flip map t.files $ \ entry =>
+                   let fname = fst (splitFileName (fileName entry)) in
+                   let mod = unsafeFoldModuleIdent (fname :: path) in
+                   let fp  = toFilePath entry in
+                   (mod, fp)
+      let dirs = flip map t.subTrees $ \ (dir ** iot) =>
+                   (fileName dir :: path, (_ ** iot))
+      go (mods ++ acc) (dirs ++ iots)
+
+export
+covering
+interactive : IO PkgDesc
+interactive = do
+  pname    <- putStr "Package name: " *> getLine
+  pauthors <- putStr "Package authors: " *> getLine
+  poptions <- putStr "Package options: " *> getLine
+  psource  <- putStr "Source directory: " *> getLine
+  let sourcedir = mstring psource
+  modules  <- findModules sourcedir
+  let pkg : PkgDesc =
+        { authors   := mstring pauthors
+        , options   := (emptyFC,) <$> mstring poptions
+        , modules   := modules
+        , sourcedir := sourcedir
+        } (initPkgDesc (fromMaybe "project" (mstring pname)))
+  pure pkg
+
+  where
+
+    mstring : String -> Maybe String
+    mstring str = case trim str of
+      "" => Nothing
+      str => Just str

src/Idris/Package/Types.idr

@@ -0,0 +1,245 @@
+module Idris.Package.Types
+
+import Core.FC
+import Core.Name.Namespace
+import Data.Maybe
+import Data.Strings
+import Idris.CommandLine
+import Idris.Version
+import Libraries.Text.PrettyPrint.Prettyprinter
+import Libraries.Text.PrettyPrint.Prettyprinter.Util
+
+%default total
+
+------------------------------------------------------------------------------
+-- Versions
+
+public export
+data PkgVersion = MkPkgVersion (List1 Nat)
+
+export
+Show PkgVersion where
+  show (MkPkgVersion vs) = showSep "." (map show (forget vs))
+
+export
+Pretty PkgVersion where
+  pretty = pretty . show
+
+export
+Eq PkgVersion where
+  MkPkgVersion p == MkPkgVersion q = p == q
+
+export
+Ord PkgVersion where
+  -- list ordering gives us what we want
+  compare (MkPkgVersion p) (MkPkgVersion q) = compare p q
+
+------------------------------------------------------------------------------
+-- Version Bounds
+
+-- version must be >= lowerBound and <= upperBound
+-- Do we want < and > as well?
+public export
+record PkgVersionBounds where
+  constructor MkPkgVersionBounds
+  lowerBound : Maybe PkgVersion
+  lowerInclusive : Bool -- >= if true
+  upperBound : Maybe PkgVersion
+  upperInclusive : Bool -- <= if true
+
+export
+Show PkgVersionBounds where
+  show p = if noBounds then "any" else lowerBounds ++ upperBounds
+
+    where
+
+      noBounds : Bool
+      noBounds = isNothing p.lowerBound && isNothing p.upperBound
+
+      lowerBounds : String
+      lowerBounds = case p.lowerBound of
+        Nothing => ""
+        Just v  => (if p.lowerInclusive then ">= " else "> ") ++ show v ++ " "
+
+      upperBounds : String
+      upperBounds = case p.upperBound of
+        Nothing => ""
+        Just v  => (if p.upperInclusive then "<= " else "< ") ++ show v
+
+export
+anyBounds : PkgVersionBounds
+anyBounds = MkPkgVersionBounds Nothing True Nothing True
+
+export
+current : PkgVersionBounds
+current = let (maj,min,patch) = semVer version
+              version = Just (MkPkgVersion (maj ::: [min, patch])) in
+              MkPkgVersionBounds version True version True
+
+export
+inBounds : Maybe PkgVersion -> PkgVersionBounds -> Bool
+inBounds mv bounds
+   = let v = fromMaybe (MkPkgVersion (0 ::: [])) mv in
+     maybe True (\v' => if bounds.lowerInclusive
+                           then v >= v'
+                           else v > v') bounds.lowerBound &&
+     maybe True (\v' => if bounds.upperInclusive
+                           then v <= v'
+                           else v < v') bounds.upperBound
+
+------------------------------------------------------------------------------
+-- Dependencies
+
+public export
+record Depends where
+  constructor MkDepends
+  pkgname : String
+  pkgbounds : PkgVersionBounds
+
+export
+Show Depends where
+  show p = p.pkgname ++ " " ++ show p.pkgbounds
+
+export
+Pretty Depends where
+  pretty = pretty . show
+
+------------------------------------------------------------------------------
+-- Package description
+
+public export
+record PkgDesc where
+  constructor MkPkgDesc
+  name : String
+  version : Maybe PkgVersion
+  authors : Maybe String
+  maintainers : Maybe String
+  license : Maybe String
+  brief   : Maybe String
+  readme  : Maybe String
+  homepage : Maybe String
+  sourceloc : Maybe String
+  bugtracker : Maybe String
+  depends : List Depends -- packages to add to search path
+  modules : List (ModuleIdent, String) -- modules to install (namespace, filename)
+  mainmod : Maybe (ModuleIdent, String) -- main file (i.e. file to load at REPL)
+  executable : Maybe String -- name of executable
+  options : Maybe (FC, String)
+  sourcedir : Maybe String
+  builddir : Maybe String
+  outputdir : Maybe String
+  prebuild : Maybe (FC, String) -- Script to run before building
+  postbuild : Maybe (FC, String) -- Script to run after building
+  preinstall : Maybe (FC, String) -- Script to run after building, before installing
+  postinstall : Maybe (FC, String) -- Script to run after installing
+  preclean : Maybe (FC, String) -- Script to run before cleaning
+  postclean : Maybe (FC, String) -- Script to run after cleaning
+
+export
+initPkgDesc : String -> PkgDesc
+initPkgDesc pname
+    = MkPkgDesc pname Nothing Nothing Nothing Nothing
+                Nothing Nothing Nothing Nothing Nothing
+                [] []
+                Nothing Nothing Nothing Nothing Nothing Nothing Nothing Nothing
+                Nothing Nothing Nothing Nothing
+
+export
+Show PkgDesc where
+  show pkg = "Package: " ++ name pkg ++ "\n" ++
+             maybe "" (\m => "Version: "     ++ m ++ "\n") (show <$> version pkg) ++
+             maybe "" (\m => "Authors: "     ++ m ++ "\n") (authors pkg)     ++
+             maybe "" (\m => "Maintainers: " ++ m ++ "\n") (maintainers pkg) ++
+             maybe "" (\m => "License: "     ++ m ++ "\n") (license pkg)     ++
+             maybe "" (\m => "Brief: "       ++ m ++ "\n") (brief pkg)       ++
+             maybe "" (\m => "ReadMe: "      ++ m ++ "\n") (readme pkg)      ++
+             maybe "" (\m => "HomePage: "    ++ m ++ "\n") (homepage pkg)    ++
+             maybe "" (\m => "SourceLoc: "   ++ m ++ "\n") (sourceloc pkg)   ++
+             maybe "" (\m => "BugTracker: "  ++ m ++ "\n") (bugtracker pkg)  ++
+             "Depends: " ++ show (depends pkg) ++ "\n" ++
+             "Modules: " ++ show (map snd (modules pkg)) ++ "\n" ++
+             maybe "" (\m => "Main: " ++ snd m ++ "\n") (mainmod pkg) ++
+             maybe "" (\m => "Exec: " ++ m ++ "\n") (executable pkg) ++
+             maybe "" (\m => "Opts: " ++ snd m ++ "\n") (options pkg) ++
+             maybe "" (\m => "SourceDir: " ++ m ++ "\n") (sourcedir pkg) ++
+             maybe "" (\m => "BuildDir: " ++ m ++ "\n") (builddir pkg) ++
+             maybe "" (\m => "OutputDir: " ++ m ++ "\n") (outputdir pkg) ++
+             maybe "" (\m => "Prebuild: " ++ snd m ++ "\n") (prebuild pkg) ++
+             maybe "" (\m => "Postbuild: " ++ snd m ++ "\n") (postbuild pkg) ++
+             maybe "" (\m => "Preinstall: " ++ snd m ++ "\n") (preinstall pkg) ++
+             maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg) ++
+             maybe "" (\m => "Preclean: " ++ snd m ++ "\n") (preclean pkg) ++
+             maybe "" (\m => "Postclean: " ++ snd m ++ "\n") (postclean pkg)
+
+export
+Pretty PkgDesc where
+  pretty desc = vcat
+    [ "package" <++> pretty desc.name
+    , verField "version"     desc.version
+    , strField "authors"     desc.authors
+    , strField "maintainers" desc.maintainers
+    , strField "license"     desc.license
+    , strField "brief"       desc.brief
+    , strField "readme"      desc.readme
+    , strField "homepage"    desc.homepage
+    , strField "sourceloc"   desc.sourceloc
+    , strField "bugtracker"  desc.bugtracker
+
+    , comment  "packages to add to search path"
+    , seqField "depends"     desc.depends
+
+    , comment "modules to install"
+    , seqField "modules"     (fst <$> desc.modules)
+
+    , comment "main file (i.e. file to load at REPL)"
+    , field    "main"        (map (pretty . fst) desc.mainmod)
+
+    , comment "name of executable"
+    , strField "executable"  desc.executable
+    , strField "opts"        (snd <$> desc.options)
+    , strField "sourcedir"   desc.sourcedir
+    , strField "builddir"    desc.builddir
+    , strField "outputdir"   desc.outputdir
+
+    , comment "script to run before building"
+    , strField "prebuild"    (snd <$> desc.prebuild)
+
+    , comment "script to run after building"
+    , strField "postbuild"   (snd <$> desc.postbuild)
+
+    , comment "script to run after building, before installing"
+    , strField "preinstall"  (snd <$> desc.preinstall)
+
+    , comment "script to run after installing"
+    , strField "postinstall" (snd <$> desc.postinstall)
+
+    , comment "script to run before cleaning"
+    , strField "preclean"    (snd <$> desc.preclean)
+
+    , comment "script to run after cleaning"
+    , strField "postclean"   (snd <$> desc.postclean)
+    ]
+
+  where
+
+    comment : String -> Doc ann
+    comment str =
+      let ws = "--" :: words str in
+      let commSoftLine = Union (Chara ' ') (hcat [Line, pretty "-- "]) in
+      Line <+> concatWith (\x, y => x <+> commSoftLine <+> y) ws
+
+    field : String -> Maybe (Doc ann) -> Doc ann
+    field nm Nothing = hsep [ pretty "--", pretty nm, equals ]
+    field nm (Just d) = hsep [ pretty nm, equals, d ]
+
+    verField : String -> Maybe PkgVersion -> Doc ann
+    verField nm = field nm . map pretty
+
+    strField : String -> Maybe String -> Doc ann
+    strField nm = field nm . map (pretty . show)
+
+    seqField : Pretty a => String -> List a -> Doc ann
+    seqField nm [] = hsep [ pretty "--", pretty nm, equals ]
+    seqField nm xs = pretty nm
+                <++> equals
+                <++> align (sep (punctuate comma (map pretty xs)))

src/Idris/SetOptions.idr

@@ -9,6 +9,7 @@ import Libraries.Utils.Path
 import Libraries.Data.List1 as Lib
 
 import Idris.CommandLine
+import Idris.Package.Types
 import Idris.REPL
 import Idris.Syntax
 import Idris.Version
@@ -28,7 +29,7 @@ import System.Directory
 -- in a given path. Return an empty list on file error (e.g. path not existing)
 export
 candidateDirs : String -> String -> PkgVersionBounds ->
-                IO (List (String, PkgVersion))
+                IO (List (String, Maybe PkgVersion))
 candidateDirs dname pkg bounds
     = do Right d <- openDir dname
              | Left err => pure []
@@ -37,10 +38,9 @@ candidateDirs dname pkg bounds
     toVersion : String -> Maybe PkgVersion
     toVersion = map MkPkgVersion
               . traverse parsePositive
-              . forget
               . split (== '.')
 
-    getVersion : String -> (String, PkgVersion)
+    getVersion : String -> (String, Maybe PkgVersion)
     getVersion str =
       -- Split the dir name into parts concatenated by "-"
       -- treating the last part as the version number
@@ -49,18 +49,18 @@ candidateDirs dname pkg bounds
       -- accept hyphenated directory names without a part
       -- corresponding to a version number.
       case Lib.unsnoc $ split (== '-') str of
-        (Nil, last) => (last, MkPkgVersion [0])
+        (Nil, last) => (last, Nothing)
         (init,last) =>
           case toVersion last of
-            Just v  => (concat $ intersperse "-" init, v)
-            Nothing => (str, MkPkgVersion [0])
+            Just v  => (concat $ intersperse "-" init, Just v)
+            Nothing => (str, Nothing)
 
     -- Return a list of paths that match the version spec
     -- (full name, version string)
     -- We'll order by version string that the highest version number is the
     -- one we use
-    getFiles : Directory -> List (String, PkgVersion) ->
-               IO (List (String, PkgVersion))
+    getFiles : Directory -> List (String, Maybe PkgVersion) ->
+               IO (List (String, Maybe PkgVersion))
     getFiles d acc
         = do Right str <- dirEntry d
                    | Left err => pure (reverse acc)

src/Libraries/System/Directory/Tree.idr

@@ -0,0 +1,169 @@
+module Libraries.System.Directory.Tree
+
+import Data.DPair
+import Data.List
+import Data.Nat
+import Data.Strings
+import System.Directory
+import Libraries.Utils.Path
+
+%default total
+
+------------------------------------------------------------------------------
+-- Filenames
+
+||| A `Filename root` is  anchored in `root`.
+||| We use a `data` type so that Idris can easily infer `root` when passing
+||| a `FileName` around. We do not use a `record` because we do not want to
+||| allow users to manufacture their own `FileName`.
+||| To get an absolute path, we need to append said filename to the root.
+export
+data FileName : Path -> Type where
+  MkFileName : String -> FileName root
+
+||| Project the string out of a `FileName`.
+export
+fileName : FileName root -> String
+fileName (MkFileName str) = str
+
+||| Convert a filename anchored in `root` to a filepath by appending the name
+||| to the root path.
+export
+toFilePath : {root : Path} -> FileName root -> String
+toFilePath file = show (root /> fileName file)
+
+export
+directoryExists : {root : Path} -> FileName root -> IO Bool
+directoryExists fp = do
+  Right dir <- openDir (toFilePath fp)
+    | Left _ => pure False
+  closeDir dir
+  pure True
+
+------------------------------------------------------------------------------
+-- Directory trees
+
+||| A `Tree root` is the representation of a directory tree anchored in `root`.
+||| Each directory contains a list of files and a list of subtrees waiting to be
+||| explored. The fact these subtrees are IO-bound means the subtrees will be
+||| lazily constructed on demand.
+public export
+SubTree : Path -> Type
+
+public export
+record Tree (root : Path) where
+  constructor MkTree
+  files    : List (FileName root)
+  subTrees : List (SubTree root)
+
+SubTree root = (dir : FileName root ** IO (Tree (root /> fileName dir)))
+
+||| An empty tree contains no files and has no sub-directories.
+export
+emptyTree : Tree root
+emptyTree = MkTree [] []
+
+||| Filter out files and directories that do not satisfy a given predicate.
+export
+filter : (filePred, dirPred : {root : _} -> FileName root -> Bool) ->
+         {root : _} -> Tree root -> Tree root
+filter filePred dirPred (MkTree files dirs) = MkTree files' dirs' where
+
+  files' : List (FileName root)
+  files' = filter filePred files
+
+  dirs' : List (SubTree root)
+  dirs' = flip mapMaybe dirs $ \ (dname ** iot) => do
+            guard (dirPred dname)
+            pure (dname ** map (assert_total (filter filePred dirPred)) iot)
+
+||| Sort the lists of files and directories using the given comparison functions
+export
+sortBy : (fileCmp, dirCmp : {root : _} -> FileName root -> FileName root -> Ordering) ->
+         {root : _} -> Tree root -> Tree root
+sortBy fileCmp dirCmp (MkTree files dirs) = MkTree files' dirs' where
+
+  files' : List (FileName root)
+  files' = sortBy fileCmp files
+
+  dirs' : List (SubTree root)
+  dirs' = sortBy (\ d1, d2 => dirCmp (fst d1) (fst d2))
+        $ flip map dirs $ \ (dname ** iot) =>
+          (dname ** map (assert_total (sortBy fileCmp dirCmp)) iot)
+
+||| Sort the list of files and directories alphabetically
+export
+sort : {root : _} -> Tree root -> Tree root
+sort = sortBy cmp cmp where
+
+  cmp : {root : _} -> FileName root -> FileName root -> Ordering
+  cmp a b = compare (fileName a) (fileName b)
+
+
+||| Exploring a filesystem from a given root to produce a tree
+export
+explore : (root : Path) -> IO (Tree root)
+
+go : {root : Path} -> Directory -> Tree root -> IO (Tree root)
+
+explore root = do
+  Right dir <- openDir (show root)
+    | Left err => pure emptyTree
+  assert_total (go dir emptyTree)
+
+go dir acc = case !(dirEntry dir) of
+  -- If there is no next entry then we are done and can return the accumulator.
+  Left err => acc <$ closeDir dir
+  -- Otherwise we have an entry and need to categorise it
+  Right entry => do
+    -- ignore aliases for current and parent directories
+    let False = elem entry [".", ".."]
+         | _ => assert_total (go dir acc)
+    -- if the entry is a directory, add it to the (lazily explored)
+    -- list of subdirectories
+    let entry : FileName root = MkFileName entry
+    let acc = if !(directoryExists entry)
+                then { subTrees $= ((entry ** explore _) ::) } acc
+                else { files    $= (entry                ::) } acc
+    assert_total (go dir acc)
+
+
+||| Display a tree by printing it procedurally. Note that because directory
+||| trees contain suspended computations corresponding to their subtrees this
+||| has to be an `IO` function. We make it return Unit rather than a String
+||| because we do not want to assume that the tree is finite.
+export
+covering
+print : Tree root -> IO ()
+print t = go [([], ".", Evidence root (pure t))] where
+
+  -- This implementation is unadulterated black magic.
+  -- Do NOT touch it if nothing is broken.
+
+  padding : Bool -> List Bool -> String
+  padding isDir = fastConcat . go [] where
+
+    go : List String -> List Bool -> List String
+    go acc [] = acc
+    go acc (b :: bs) = go (hd :: acc) bs where
+      hd : String
+      hd = if isDir && isNil acc
+           then if b then " ├ " else " └ "
+           else if b then " │"  else "  "
+
+  prefixes : Nat -> List Bool
+  prefixes n = snoc (replicate (pred n) True) False
+
+  covering
+  go : List (List Bool, String, Exists (IO . Tree)) -> IO ()
+  go [] = pure ()
+  go ((bs, fn, Evidence _ iot) :: iots) = do
+    t <- iot
+    putStrLn (padding True bs ++ fn)
+    let pad = padding False bs
+    let pads = prefixes (length t.files + length t.subTrees)
+    for_ (zip pads t.files) $ \ (b, fp) =>
+      putStrLn (pad ++ (if b then " ├ " else " └ ") ++ fileName fp)
+    let bss = map (:: bs) (prefixes (length t.subTrees))
+    go (zipWith (\ bs, (dir ** iot) => (bs, fileName dir, Evidence _ iot)) bss t.subTrees)
+    go iots

src/Libraries/Utils/Path.idr

@@ -13,7 +13,7 @@ import Libraries.Text.Quantity
 
 import System.Info
 
-infixr 5 </>
+infixr 5 </>, />
 infixr 7 <.>
 
 
@@ -340,6 +340,7 @@ setFileName' name path =
   else
     append' path (parse name)
 
+export
 splitFileName : String -> (String, String)
 splitFileName name =
   case break (== '.') $ reverse $ unpack name of
@@ -369,6 +370,23 @@ export
 isRelative : String -> Bool
 isRelative = not . isAbsolute
 
+||| Appends the right path to the left path.
+|||
+||| If the path on the right is absolute, it replaces the left path.
+|||
+||| On Windows:
+|||
+||| - If the right path has a root but no volume (e.g., `\windows`), it replaces
+|||   everything except for the volume (if any) of left.
+||| - If the right path has a volume but no root, it replaces left.
+|||
+||| ```idris example
+||| parse "/usr" /> "local/etc" == "/usr/local/etc"
+||| ```
+export
+(/>) : (left : Path) -> (right : String) -> Path
+(/>) left right = append' left (parse right)
+
 ||| Appends the right path to the left path.
 |||
 ||| If the path on the right is absolute, it replaces the left path.
@@ -384,7 +402,8 @@ isRelative = not . isAbsolute
 ||| ```
 export
 (</>) : (left : String) -> (right : String) -> String
-(</>) left right = show $ append' (parse left) (parse right)
+(</>) left right = show $ parse left /> right
+
 
 ||| Joins path components into one.
 |||
@@ -393,7 +412,7 @@ export
 ||| ```
 export
 joinPath : List String -> String
-joinPath xs = foldl (</>) "" xs
+joinPath xs = show $ foldl (/>) (parse "") xs
 
 ||| Splits path into components.
 |||

src/Parser/Lexer/Package.idr

@@ -121,7 +121,8 @@ lex : String -> Either (Int, Int, String) (List (WithBounds Token))
 lex str =
   case lexTo (const False) rawTokens str of
        (tokenData, (l, c, "")) =>
-         Right $ (filter (useful . val) tokenData) ++ [MkBounded EndOfInput False (MkBounds l c l c)]
+         Right $ (filter (useful . val) tokenData)
+          ++ [MkBounded EndOfInput False (MkBounds l c l c)]
        (_, fail) => Left fail
   where
     useful : Token -> Bool

tests/Main.idr

@@ -136,20 +136,23 @@ idrisTestsData = MkTestPool []
        "record001", "record002", "record003", "record004", "record005",
        "record006", "record007"]
 
+idrisTestsEvaluator : TestPool
+idrisTestsEvaluator = MkTestPool []
+      [ -- Evaluator
+       "evaluator001", "evaluator002", "evaluator003", "evaluator004",
+       -- Miscellaneous REPL
+       "interpreter001", "interpreter002", "interpreter003", "interpreter004",
+       "interpreter005", "interpreter006", "interpreter007"]
+
 idrisTests : TestPool
 idrisTests = MkTestPool []
        -- Documentation strings
       ["docs001", "docs002",
-       -- Evaluator
-       "evaluator001", "evaluator002", "evaluator003", "evaluator004",
        -- Unfortunately the behaviour of Double is platform dependent so the
        -- following test is turned off.
        -- "evaluator005",
        -- Modules and imports
        "import001", "import002", "import003", "import004", "import005",
-       -- Miscellaneous REPL
-       "interpreter001", "interpreter002", "interpreter003", "interpreter004",
-       "interpreter005", "interpreter006", "interpreter007",
        -- Implicit laziness, lazy evaluation
        "lazy001",
        -- Namespace blocks
@@ -157,7 +160,7 @@ idrisTests = MkTestPool []
        -- Parameters blocks
        "params001",
        -- Packages and ipkg files
-       "pkg001", "pkg002", "pkg003", "pkg004", "pkg005", "pkg006",
+       "pkg001", "pkg002", "pkg003", "pkg004", "pkg005", "pkg006", "pkg007",
        -- Positivity checking
        "positivity001", "positivity002", "positivity003",
        -- Larger programs arising from real usage. Typically things with
@@ -275,6 +278,7 @@ main = runner
   , testPaths "idris2" idrisTestsPerformance
   , testPaths "idris2" idrisTestsRegression
   , testPaths "idris2" idrisTestsData
+  , testPaths "idris2" idrisTestsEvaluator
   , testPaths "idris2" idrisTests
   , testPaths "typedd-book" typeddTests
   , testPaths "ideMode" ideModeTests

tests/idris2/pkg007/A/Path/Of/Dires/First.idr

@@ -0,0 +1,8 @@
+module A.Path.Of.Dires.First
+
+%default total
+
+public export
+data Tree : Type -> Type where
+  Leaf : a -> Tree a
+  Node : Tree a -> Tree a -> Tree a

tests/idris2/pkg007/A/Path/Of/Dires/Second.idr

@@ -0,0 +1,9 @@
+module A.Path.Of.Dires.Second
+
+import public A.Path.Of.Dires.First
+
+%default total
+
+export
+example : Tree Nat
+example = Node (Node (Leaf 0) (Leaf 1)) (Leaf 2)

tests/idris2/pkg007/Another/Fourth.idr

@@ -0,0 +1,9 @@
+module Another.Fourth
+
+import A.Path.Of.Dires.Second
+import Another.One.Third
+
+%default total
+
+example2 : Tree Nat
+example2 = map S example

tests/idris2/pkg007/Another/One/Third.idr

@@ -0,0 +1,10 @@
+module Another.One.Third
+
+import A.Path.Of.Dires.First
+
+%default total
+
+export
+map : (a -> b) -> Tree a -> Tree b
+map f (Leaf a) = Leaf (f a)
+map f (Node l r) = Node (map f l) (map f r)

tests/idris2/pkg007/expected

@@ -0,0 +1,6 @@
+Package name: Package authors: Package options: Source directory: 1/4: Building A.Path.Of.Dires.First (A/Path/Of/Dires/First.idr)
+2/4: Building A.Path.Of.Dires.Second (A/Path/Of/Dires/Second.idr)
+3/4: Building Another.One.Third (Another/One/Third.idr)
+4/4: Building Another.Fourth (Another/Fourth.idr)
+Package name: Package authors: Package options: Source directory: 1/2: Building Yet.Another.Path (src/Yet/Another/Path.idr)
+2/2: Building And.A.Proof (src/And/A/Proof.idr)

tests/idris2/pkg007/input

@@ -0,0 +1,4 @@
+cool
+gallais
+-p contrib
+

tests/idris2/pkg007/input2

@@ -0,0 +1,4 @@
+cool
+gallais
+-p contrib
+src

tests/idris2/pkg007/run

@@ -0,0 +1,9 @@
+$1 --init < input
+$1 --build cool.ipkg
+rm -Rf build/
+
+$1 --init cool2.ipkg < input2
+$1 --build cool2.ipkg
+rm -Rf build/
+
+rm -f cool.ipkg cool2.ipkg

tests/idris2/pkg007/src/And/A/Proof.idr

@@ -0,0 +1,8 @@
+module And.A.Proof
+
+import Yet.Another.Path as Val
+
+%default total
+
+equality : Val.val === 2+3
+equality = Refl

tests/idris2/pkg007/src/Yet/Another/Path.idr

@@ -0,0 +1,7 @@
+module Yet.Another.Path
+
+%default total
+
+public export
+val : Nat
+val = 5