4 | module Pack.Core.Types
6 | import public Data.FilePath.File
10 | import Derive.Prelude
11 | import Idris.Package.Types
15 | %language ElabReflection
26 | quote : Interpolation a => a -> String
27 | quote v = "\"\{v}\""
37 | relativeTo : (origin, target : Path Abs) -> Path Rel
38 | relativeTo (PAbs _ sx) (PAbs _ sy) = PRel $
go (sx <>> []) (sy <>> [])
41 | go : (o,t : List Body) -> SnocList Body
42 | go [>] t = Lin <>< t
43 | go xs [] = Lin <>< xs $> ".."
44 | go (x :: xs) (y :: ys) = case x == y of
46 | False => Lin <>< (((x :: xs) $> "..") ++ (y :: ys))
50 | isIpkgBody : Body -> Bool
51 | isIpkgBody = (Just "ipkg" ==) . extension
55 | isTomlBody : Body -> Bool
56 | isTomlBody = (Just "toml" ==) . extension
60 | isHtmlBody : Body -> Bool
61 | isHtmlBody = (Just "html" ==) . extension
63 | toRelPath : String -> Path Rel
64 | toRelPath s = case the FilePath (fromString s) of
65 | FP (PAbs _ sx) => PRel sx
66 | FP (PRel sx) => PRel sx
72 | toAbsPath : (parent : Path Abs) -> FilePath -> Path Abs
73 | toAbsPath parent (FP $
PAbs d sx) = PAbs d sx
74 | toAbsPath parent (FP $
PRel sx) = parent </> PRel sx
80 | parse : String -> (parentDir : Path Abs) -> Path Abs
81 | parse s parentDir = toAbsPath parentDir (fromString s)
84 | Cast String (Path Rel) where
87 | export infixl 5 <//>
91 | (<//>) : Cast a (Path Rel) => Path t -> a -> Path t
92 | p <//> v = p </> cast v
99 | (//>) : Cast a Body => Path t -> a -> Path t
100 | p //> v = p /> cast v
102 | export infixl 8 <->
106 | (<->) : Cast a Body => Cast b Body => a -> b -> Body
107 | x <-> y = the Body (cast x) <+> "-" <+> cast y
111 | Cast PkgVersion Body where
112 | cast = fromMaybe "0" . parse . show
116 | Cast (Maybe PkgVersion) Body where
118 | cast (Just v) = cast v
123 | toAbsFile : Path Abs -> File Rel -> File Abs
124 | toAbsFile parentDir (MkF p f) = MkF (parentDir </> p) f
127 | Cast (File t) (Path t) where cast = toPath
136 | record PackDirs where
182 | data CurDir : Type where
184 | CD : (dir : Path Abs) -> CurDir
187 | Interpolation CurDir where
188 | interpolate (CD dir) = interpolate dir
193 | curDir : (cd : CurDir) => Path Abs
194 | curDir {cd = CD dir} = dir
199 | data TmpDir : Type where
201 | TD : (dir : Path Abs) -> TmpDir
204 | Interpolation TmpDir where
205 | interpolate (TD dir) = interpolate dir
210 | tmpDir : (td : TmpDir) => Path Abs
211 | tmpDir {td = TD dir} = dir
219 | record TTCVersion where
222 | version : Maybe Body
227 | ttcVersion : (ttc : TTCVersion) => Maybe Body
228 | ttcVersion = ttc.version
237 | Interpolation FileError where interpolate = show
242 | Interpolation PkgVersion where interpolate = show
254 | %runElab derive "URL" [Show,Eq,FromString]
257 | Interpolation URL where interpolate = value
260 | Cast URL (Path Rel) where
261 | cast (MkURL s) = case unpack s of
262 | 'h'::'t'::'t'::'p'::'s'::':'::'/'::'/':: t => cast (pack t)
263 | 'h'::'t'::'t'::'p'::':'::'/'::'/':: t => cast (pack t)
272 | record Commit where
273 | constructor MkCommit
276 | %runElab derive "Commit" [Show,Eq,FromString]
279 | Interpolation Commit where interpolate = value
282 | Cast Commit (Path Rel) where
283 | cast = toRelPath . value
291 | %runElab derive "Hash" [Show,Eq,FromString]
294 | Interpolation Hash where interpolate = value
297 | Cast Hash (Path Rel) where
298 | cast = toRelPath . value
306 | record Branch where
307 | constructor MkBranch
310 | %runElab derive "Branch" [Show,Eq,FromString]
313 | Interpolation Branch where interpolate = value
316 | Cast Branch (Path Rel) where
317 | cast = toRelPath . value
325 | record PkgName where
326 | constructor MkPkgName
329 | %runElab derive "PkgName" [Show,Eq,Ord,FromString]
332 | Interpolation PkgName where interpolate = value
335 | Cast PkgName (Path Rel) where
336 | cast = toRelPath . value
345 | data PkgOrIpkg : Type where
346 | Pkg : PkgName -> PkgOrIpkg
347 | Ipkg : File Abs -> PkgOrIpkg
355 | data PkgType = PLib | PApp
358 | Interpolation PkgType where
359 | interpolate PLib = "lib"
360 | interpolate PApp = "app"
364 | PLib == PLib = True
365 | PApp == PApp = True
370 | compare PLib PApp = LT
371 | compare PApp PLib = GT
382 | data InstallType : Type where
383 | Library : InstallType
384 | App : (withWrapperScript : Bool) -> InstallType
387 | Interpolation InstallType where
388 | interpolate Library = "library"
389 | interpolate (App b) = "app"
392 | Eq InstallType where
393 | Library == Library = True
394 | App b1 == App b2 = b1 == b2
398 | Ord InstallType where
399 | compare Library (App _) = LT
400 | compare (App _) Library = GT
401 | compare Library Library = EQ
402 | compare (App b1) (App b2) = compare b1 b2
411 | record DBName where
412 | constructor MkDBName
416 | Eq DBName where (==) = (==) `on` value
419 | Ord DBName where compare = compare `on` value
422 | Interpolation DBName where interpolate = interpolate . value
425 | Cast DBName Body where
430 | Head = MkDBName "HEAD"
434 | All = MkDBName "all"
446 | record Desc (t : PkgDesc -> Type) where
462 | 0 U : PkgDesc -> Type
468 | dependencies : PkgDesc -> List PkgName
469 | dependencies d = map (MkPkgName . pkgname) $
d.depends
473 | dependencies : Desc t -> List PkgName
474 | dependencies d = dependencies d.desc
482 | data CmdArg : Type where
488 | Escapable : String -> CmdArg
495 | NoEscape : String -> CmdArg
502 | interface CmdArgable a where
503 | toCmdArg : a -> CmdArg
506 | CmdArgable CmdArg where
512 | Interpolation a => CmdArgable a where
513 | toCmdArg = Escapable . interpolate
525 | data CmdArgList : Type where
527 | (::) : CmdArgable a => a -> CmdArgList -> CmdArgList
529 | cmdArgList : CmdArgList -> List CmdArg
531 | cmdArgList (x::xs) = toCmdArg x :: cmdArgList xs
540 | escapeCmd : CmdArgList -> String
541 | escapeCmd = unwords . map manageArg . cmdArgList where
542 | manageArg : CmdArg -> String
543 | manageArg $
Escapable s = escapeArg s
544 | manageArg $
NoEscape s = s
557 | (++) : CmdArg -> CmdArg -> CmdArg
558 | Escapable x ++ Escapable y = Escapable $
x ++ y
559 | Escapable x ++ NoEscape y = NoEscape $
escapeArg x ++ y
560 | NoEscape x ++ Escapable y = NoEscape $
x ++ escapeArg y
561 | NoEscape x ++ NoEscape y = NoEscape $
x ++ y
563 | namespace CmdArgList
567 | (++) : CmdArgList -> CmdArgList -> CmdArgList
569 | (x::xs) ++ ys = x :: xs ++ ys
572 | Semigroup CmdArgList where
576 | Monoid CmdArgList where
582 | concatMap : Monoid m => (CmdArg -> m) -> CmdArgList -> m
583 | concatMap f [] = neutral
584 | concatMap f (x::xs) = f (toCmdArg x) <+> concatMap f xs
589 | fromStrList : List String -> CmdArgList
590 | fromStrList = foldr (\x, xs => x::xs) Nil
599 | record LineBufferingCmd where
601 | constructor MkLineBufferingCmd
602 | lineBufferingCmd : CmdArgList
610 | data LogLevel : Type where
619 | llToNat : LogLevel -> Nat
624 | llToNat Warning = 4
625 | llToNat Silence = 5
628 | Eq LogLevel where (==) = (==) `on` llToNat
631 | Ord LogLevel where compare = compare `on` llToNat
634 | Interpolation LogLevel where
635 | interpolate Debug = "debug"
636 | interpolate Build = "build"
637 | interpolate Info = "info"
638 | interpolate Cache = "cache"
639 | interpolate Warning = "warning"
640 | interpolate Silence = ""
643 | logLevels : List (String, LogLevel)
645 | [ ("debug" , Debug )
646 | , ("build" , Build )
648 | , ("cache" , Cache )
649 | , ("warning", Warning)
650 | , ("silence", Silence)
655 | record LogRef where
657 | constructor MkLogRef
666 | data TOMLErr : Type where
669 | MissingKey : (path : List String) -> TOMLErr
672 | WrongType : (path : List String) -> (type : String) -> TOMLErr
674 | tomlPath : List String -> String
675 | tomlPath = concat . intersperse "."
677 | printTOMLErr : TOMLErr -> String
678 | printTOMLErr (MissingKey path) = "Missing toml key: \{tomlPath path}."
679 | printTOMLErr (WrongType path type) =
680 | "Wrong type at \{tomlPath path}. Expect \{type}."
685 | prefixKey : (key : String) -> Either TOMLErr a -> Either TOMLErr a
686 | prefixKey k = mapFst $
\case
687 | MissingKey p => MissingKey (k :: p)
688 | WrongType p t => WrongType (k :: p) t
692 | data PackErr : Type where
697 | NoPackDir : PackErr
703 | MkDir : (path : Path Abs) -> (err : FileError) -> PackErr
706 | ReadFile : (path : File Abs) -> (err : FileError) -> PackErr
709 | WriteFile : (path : File Abs) -> (err : FileError) -> PackErr
712 | DirEntries : (path : Path Abs) -> (err : FileError) -> PackErr
715 | Sys : (cmd : CmdArgList) -> (err : Int) -> PackErr
718 | ChangeDir : (path : Path Abs) -> PackErr
721 | UnknownPkg : (name : PkgName) -> PackErr
724 | IncompletePkg : (name : PkgName) -> PackErr
727 | NotLocalPkg : (name : PkgName) -> PackErr
731 | NoApp : (rep : PkgName) -> PackErr
735 | NoAppIpkg : (path : File Abs) -> PackErr
738 | InvalidPackageDesc : (s : String) -> PackErr
741 | EmptyPkgDB : PackErr
744 | InvalidDBHeader : (s : String) -> PackErr
747 | InvalidDBName : (s : String) -> PackErr
750 | InvalidPkgType : (s : String) -> PackErr
753 | InvalidPkgVersion : (s : String) -> PackErr
756 | InvalidLogLevel : (s : String) -> PackErr
759 | InvalidIpkgFile : (path : File Abs) -> PackErr
762 | InvalidBody : (s : String) -> PackErr
765 | NoFilePath : (str : String) -> PackErr
769 | MissingCorePackage :
771 | -> (version : PkgVersion)
772 | -> (commit : Commit)
776 | UnknownArg : (arg : String) -> PackErr
779 | InvalidArgs : (args : List String) -> PackErr
782 | ErroneousArg : (err : String) -> PackErr
786 | BuildMany : List Body -> PackErr
789 | UnknownCommand : String -> (usage : String) -> PackErr
794 | -> (args : List String)
795 | -> (usage : String)
800 | DirExists : Path Abs -> PackErr
803 | TOMLFile : (file : File Abs) -> (err : TOMLErr) -> PackErr
806 | TOMLParse : (err : String) -> PackErr
809 | BuildFailures : Nat -> PackErr
812 | ManualInstallPackApp : PackErr
815 | SafetyAbort : PackErr
817 | CyclicDeps : List PkgName -> PackErr
821 | printErr : PackErr -> String
822 | printErr NoCurDir = "Failed to get current directory."
824 | printErr NoPackDir = """
825 | Failed to figure out package directory.
826 | This means, that neither environment variable \"PACK_DIR\"
827 | nor environment varaible \"HOME\" was set.
830 | printErr NoTmpDir = """
831 | Failed to create temporary directory.
832 | Please check directory `PACK_DIR` and make sure to remove
833 | all `.tmpXY` directories you no longer need.
836 | printErr (MkDir path err) =
837 | "Error when creating directory \{quote path}: \{err}."
839 | printErr (ReadFile path err) =
840 | "Error when reading file \{quote path}: \{err}."
842 | printErr (WriteFile path err) =
843 | "Error when writing to file \{quote path}: \{err}."
845 | printErr (DirEntries path err) =
846 | "Error when reading directory \{quote path}: \{err}."
848 | printErr (Sys cmd err) = """
849 | Error when executing system command.
850 | Command: \{escapeCmd cmd}
851 | Error code: \{show err}
854 | printErr (ChangeDir path) =
855 | "Failed to change to directory \{quote path}."
857 | printErr (InvalidPackageDesc s) = """
858 | Invalid package description: \{quote s}.
859 | This should be of the format \"name,url,commit hash,ipkg file\".
862 | printErr (InvalidDBHeader s) = """
863 | Invalid data base header: \{quote s}.
864 | This should be of the format \"idris2 commit hash,idris2 version\".
867 | printErr (InvalidDBName s) = """
868 | Invalid data collection name: \{quote s}.
869 | This should be a non-empty string without path separators.
872 | printErr (InvalidBody s) = "Invalid file path body: \{quote s}."
874 | printErr (InvalidPkgType s) = """
875 | Invalid package type: \{quote s}.
876 | Valid types are `lib` and `bin`.
879 | printErr (InvalidPkgVersion s) = "Invalid package version: \{quote s}."
881 | printErr (InvalidLogLevel s) = """
882 | Invalid log level: \{quote s}. Valid values are
883 | \{joinBy "\n" $ ("- " ++) . fst <$> logLevels}
886 | printErr (UnknownPkg name) = "Unknown package: \{name}"
888 | printErr (IncompletePkg name) = "Incomplete data for custom package: \{name}"
890 | printErr (NotLocalPkg name) = "Not a local package: \{name}"
892 | printErr (NoApp rep) = "Package \{rep} is not an application"
894 | printErr (NoAppIpkg p) = "Package \{p} is not an application"
896 | printErr EmptyPkgDB = "Empty package data base"
898 | printErr (InvalidIpkgFile path) =
899 | "Failed to parse .ipkg file: \{path}"
901 | printErr (MissingCorePackage nm v c) =
902 | "Core package \{quote nm} missing for Idris2 version \{v} (commit: \{c})"
904 | printErr (UnknownArg arg) = "Unknown command line arg: \{arg}"
906 | printErr (InvalidArgs args) = "Invalid command line args: \{unwords args}"
908 | printErr (ErroneousArg err) = err
910 | printErr (UnknownCommand cmd usage) =
912 | Unknown command: "\{cmd}"
917 | printErr (InvalidCmdArgs cmd args usage) =
919 | Invalid argument(s) for command `\{cmd}`.
924 | printErr (BuildMany []) = "No local `.ipkg` files found."
925 | printErr (BuildMany fs@(_::_)) = """
926 | Ambiguous `.ipkg` files:
927 | \{joinBy "\n" $ ("- " ++) . interpolate <$> fs}
928 | Please choose only one.
931 | printErr (NoFilePath s) = "Not a file path : \{s}"
933 | printErr (DirExists path) = """
934 | Failed to clone Git repository into \{path}.
935 | Directory already exists.
938 | printErr (TOMLFile file err) =
939 | "Error in file \{file}: \{printTOMLErr err}."
941 | printErr (TOMLParse err) = err
943 | printErr (BuildFailures 1) = "1 package failed to build."
945 | printErr (BuildFailures n) = "\{show n} packages failed to build."
947 | printErr ManualInstallPackApp = """
948 | You are not supposed to manually install or remove the pack
949 | application. In order to update pack to the latest version on
950 | GitHub, run `pack update`.
952 | Note: If you didn't run `pack install-app pack` or a similar
953 | operation, "pack" might be listed as an auto-install application
954 | in one of your pack.toml files. Please remove it from there.
957 | printErr (CyclicDeps ps) =
958 | let cycle = fastConcat $
intersperse " -> " (map value ps)
960 | Dependency cylce detected:
964 | printErr SafetyAbort = "Aborted."
969 | readDBName : String -> Either PackErr DBName
970 | readDBName s = case Body.parse s of
971 | Just b => Right $
MkDBName b
972 | Nothing => Left (InvalidDBName s)
976 | readBody : String -> Either PackErr Body
977 | readBody s = case Body.parse s of
979 | Nothing => Left (InvalidBody s)
983 | readPkgType : String -> Either PackErr PkgType
984 | readPkgType "lib" = Right PLib
985 | readPkgType "bin" = Right PApp
986 | readPkgType "app" = Right PApp
987 | readPkgType s = Left (InvalidPkgType s)
994 | readAbsFile : (curdir : Path Abs) -> String -> Either PackErr (File Abs)
995 | readAbsFile cd s = case split $
toAbsPath cd (fromString s) of
996 | Just (p,b) => Right $
MkF p b
997 | Nothing => Left (NoFilePath s)
1000 | readLogLevel : String -> Either PackErr LogLevel
1001 | readLogLevel str = maybeToEither (InvalidLogLevel str) $
lookup str logLevels