diff --git a/idris2api.ipkg b/idris2api.ipkg index 0500e13f0..33d01c6db 100644 --- a/idris2api.ipkg +++ b/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, diff --git a/libs/contrib/System/Directory/Tree.idr b/libs/contrib/System/Directory/Tree.idr new file mode 100644 index 000000000..d083f458b --- /dev/null +++ b/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 diff --git a/libs/contrib/System/Path.idr b/libs/contrib/System/Path.idr index 61ca30e30..91332daa5 100644 --- a/libs/contrib/System/Path.idr +++ b/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. ||| diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg index 9e112597c..275a8ade7 100644 --- a/libs/contrib/contrib.ipkg +++ b/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, diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 5fa56dc86..0bcac2089 100644 --- a/src/Idris/CommandLine.idr +++ b/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]) diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 6d5038c1d..d3a99968c 100644 --- a/src/Idris/Package.idr +++ b/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 diff --git a/src/Idris/Package/Init.idr b/src/Idris/Package/Init.idr new file mode 100644 index 000000000..284d19c8f --- /dev/null +++ b/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 diff --git a/src/Idris/Package/Types.idr b/src/Idris/Package/Types.idr new file mode 100644 index 000000000..f4a34e141 --- /dev/null +++ b/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))) diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 02fd36827..44df641ad 100644 --- a/src/Idris/SetOptions.idr +++ b/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) diff --git a/src/Libraries/System/Directory/Tree.idr b/src/Libraries/System/Directory/Tree.idr new file mode 100644 index 000000000..115bdad9e --- /dev/null +++ b/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 diff --git a/src/Libraries/Utils/Path.idr b/src/Libraries/Utils/Path.idr index a44cb8d9d..d736193ff 100644 --- a/src/Libraries/Utils/Path.idr +++ b/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. ||| diff --git a/src/Parser/Lexer/Package.idr b/src/Parser/Lexer/Package.idr index bf6a8f8d2..10f755dee 100644 --- a/src/Parser/Lexer/Package.idr +++ b/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 diff --git a/tests/Main.idr b/tests/Main.idr index d077f066e..25ba2321c 100644 --- a/tests/Main.idr +++ b/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 diff --git a/tests/idris2/pkg007/A/Path/Of/Dires/First.idr b/tests/idris2/pkg007/A/Path/Of/Dires/First.idr new file mode 100644 index 000000000..4a9407eb4 --- /dev/null +++ b/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 diff --git a/tests/idris2/pkg007/A/Path/Of/Dires/Second.idr b/tests/idris2/pkg007/A/Path/Of/Dires/Second.idr new file mode 100644 index 000000000..8a46d6e4e --- /dev/null +++ b/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) diff --git a/tests/idris2/pkg007/Another/Fourth.idr b/tests/idris2/pkg007/Another/Fourth.idr new file mode 100644 index 000000000..579ef50fa --- /dev/null +++ b/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 diff --git a/tests/idris2/pkg007/Another/One/Third.idr b/tests/idris2/pkg007/Another/One/Third.idr new file mode 100644 index 000000000..7cb2fee76 --- /dev/null +++ b/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) diff --git a/tests/idris2/pkg007/expected b/tests/idris2/pkg007/expected new file mode 100644 index 000000000..9bce36120 --- /dev/null +++ b/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) diff --git a/tests/idris2/pkg007/input b/tests/idris2/pkg007/input new file mode 100644 index 000000000..cdc0edeb3 --- /dev/null +++ b/tests/idris2/pkg007/input @@ -0,0 +1,4 @@ +cool +gallais +-p contrib + diff --git a/tests/idris2/pkg007/input2 b/tests/idris2/pkg007/input2 new file mode 100644 index 000000000..57cd548bf --- /dev/null +++ b/tests/idris2/pkg007/input2 @@ -0,0 +1,4 @@ +cool +gallais +-p contrib +src diff --git a/tests/idris2/pkg007/run b/tests/idris2/pkg007/run new file mode 100755 index 000000000..542eda6c8 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/tests/idris2/pkg007/src/And/A/Proof.idr b/tests/idris2/pkg007/src/And/A/Proof.idr new file mode 100644 index 000000000..744af6dc4 --- /dev/null +++ b/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 diff --git a/tests/idris2/pkg007/src/Yet/Another/Path.idr b/tests/idris2/pkg007/src/Yet/Another/Path.idr new file mode 100644 index 000000000..9973d76be --- /dev/null +++ b/tests/idris2/pkg007/src/Yet/Another/Path.idr @@ -0,0 +1,7 @@ +module Yet.Another.Path + +%default total + +public export +val : Nat +val = 5