Idris2Doc : Pack.Database.Types

Pack.Database.Types

(source)
Definitions
0 I : Type -> Type
  Type-level identity

  Totality: total
  Visibility: public export
data MetaCommit : Type
  A git commit hash or tag, or a meta commit: The latest commit of a branch.

  Totality: total
  Visibility: public export
  Constructors:
  
MC : Commit -> MetaCommit
  
Latest : Branch -> MetaCommit
  
Fetch : Branch -> MetaCommit

  Hints:
  
Eq MetaCommit
  
FromString MetaCommit
  
FromTOML MetaCommit
  
Interpolation MetaCommit
  
Show MetaCommit
toLatest : MetaCommit -> MetaCommit
  Totality: total
  Visibility: export
data FetchMethod : Type
  Strategy for resolving `MetaCommit`s

  Totality: total
  Visibility: public export
  Constructors:
  
MissingOnly : FetchMethod
  Update only meta commits, which don't have a cached entry in the
  "commits" directory. This is the default.
  
All : FetchMethod
  Update all custom commits. This is the strategy used with the `fetch`
  command.
  
ClearCommits : FetchMethod
  Remove the "commits" directory, thus forcing all meta commits to
  be resolved again. This is the strategy used with the `switch latest`
  command

  Hints:
  
Eq FetchMethod
  
Ord FetchMethod
  
Show FetchMethod
data CorePkg : Type
  Core packages bundled with the Idris compiler

  Totality: total
  Visibility: public export
  Constructors:
  
Prelude : CorePkg
  
Base : CorePkg
  
Contrib : CorePkg
  
Linear : CorePkg
  
Network : CorePkg
  
Test : CorePkg
  
Papers : CorePkg
  
IdrisApi : CorePkg

  Hints:
  
Cast CorePkg Body
  
Cast CorePkg (Path Rel)
  
Interpolation CorePkg
  
Uninhabited (IsLocal (Core {_:2936}))
  
Uninhabited (IsGit (Core {_:3115}))
corePkgs : List CorePkg
  The list of core packages.

  Totality: total
  Visibility: public export
corePkgName : CorePkg -> PkgName
  Package name of a core package.

  Totality: total
  Visibility: export
coreIpkgFile : CorePkg -> Body
  `.ipkg` file name corrsponding to a core package.

  Totality: total
  Visibility: export
coreIpkgPath : CorePkg -> File Rel
  Relative path to the `.ipkg` file corrsponding to a core package
  (in the Idris2 project).

  Totality: total
  Visibility: export
readCorePkg : String -> Maybe CorePkg
  Try to convert a string to a core package.

  Totality: total
  Visibility: export
isCorePkg : String -> Bool
  True, if the given string corresponds to one of the core packges.

  Totality: total
  Visibility: export
data Package_ : (Type -> Type) -> Type -> Type
  Description of a Git or local Idris package in the
  package database.
  
  Note: This does not contain the package name, as it
  will be paired with its name in a `SortedMap`.

  Totality: total
  Visibility: public export
  Constructors:
  
Git : f URL -> f c -> f (File Rel) -> f Bool -> Maybe (File Rel) -> Maybe String -> Package_ f c
  A Git repository, given as the package's URL,
  commit (hash or tag), and name of `.ipkg` file to use.
  `pkgPath` should be set to `True` for executables which need
  access to the `IDRIS2_PACKAGE_PATH`: The list of directories
  where Idris packages are installed.
  
Local : Path Abs -> File Rel -> Bool -> Maybe (File Rel) -> Package_ f c
  A local Idris project given as an absolute path to a local
  directory, and `.ipkg` file to use.
  `pkgPath` should be set to `True` for executable which need
  access to the `IDRIS2_PACKAGE_PATH`: The list of directories
  where Idris packages are installed.
  
Core : CorePkg -> Package_ f c
  A core package of the Idris2 project

  Hints:
  
FromTOML c => FromTOML (Package_ I c)
  
FromTOML c => FromTOML (Package_ Maybe c)
  
Functor (Package_ I)
traverse : Applicative f => (URL -> a -> f b) -> Package_ I a -> f (Package_ I b)
  Totality: total
  Visibility: export
0 Package : Type
  An alias for `Package_ Commit`: A package description with
  meta commits already resolved.

  Totality: total
  Visibility: public export
0 UserPackage : Type
  An alias for `Package_ MetaCommit`: A package description where
  the commit might still contain meta information.

  Totality: total
  Visibility: public export
0 PackageMap : Type
  Totality: total
  Visibility: public export
0 CustomMap : Type
  Totality: total
  Visibility: public export
data IsCore : Package -> Type
  Proof that a package is a core package

  Totality: total
  Visibility: public export
  Constructor: 
ItIsCore : IsCore (Core c)

  Hints:
  
Uninhabited (IsCore (Local {_:2747} {_:2746} {_:2745} {_:2744}))
  
Uninhabited (IsCore (Git {_:2796} {_:2797} {_:2798} {_:2799} {_:2801} {_:2800}))
isCore : (p : Package) -> Dec (IsCore p)
  Decides, if the given package represents
  one of the core packages (`base`, `prelude`, etc.)

  Totality: total
  Visibility: export
data IsLocal : Package -> Type
  Proof that a package is a local package

  Totality: total
  Visibility: public export
  Constructor: 
ItIsLocal : IsLocal (Local {_:2931} {_:2930} {_:2929} {_:2928})

  Hints:
  
Uninhabited (IsLocal (Core {_:2936}))
  
Uninhabited (IsLocal (Git {_:2967} {_:2968} {_:2969} {_:2970} {_:2972} {_:2971}))
isLocal : (p : Package) -> Dec (IsLocal p)
  Decides, if the given package represents
  a local package.

  Totality: total
  Visibility: export
data IsGit : Package -> Type
  Proof that a package is a Git package

  Totality: total
  Visibility: public export
  Constructor: 
ItIsGit : IsGit (Git {_:3105} {_:3106} {_:3107} {_:3108} {_:3110} {_:3109})

  Hints:
  
Uninhabited (IsGit (Core {_:3115}))
  
Uninhabited (IsGit (Local {_:3143} {_:3142} {_:3141} {_:3140}))
isGit : (p : Package) -> Dec (IsGit p)
  Decides, if the given package represents
  a Git package.

  Totality: total
  Visibility: export
usePackagePath : Package_ I c -> Bool
  True, if the given application needs access to the
  folders where Idris package are installed.

  Totality: total
  Visibility: export
ipkg : Path Abs -> Package -> File Abs
  Absolute path to the `.ipkg` file of a package.

  Totality: total
  Visibility: export
data PkgStatus : Package -> Type
  Installation status of an Idris package.

  Totality: total
  Visibility: public export
  Constructors:
  
Missing : Hash -> PkgStatus p
  
Installed : Hash -> Bool -> PkgStatus p
hash : PkgStatus p -> Hash
  Totality: total
  Visibility: export
record ResolvedLib : (PkgDesc -> Type) -> Type
  A resolved library, which was cloned from a Git repo
  or looked up in the local file system. This comes with
  a fully parsed `PkgDesc` (representing the `.ipkg` file).

  Totality: total
  Visibility: public export
  Constructor: 
RL : (pkg : Package) -> Hash -> PkgName -> Desc t -> PkgStatus pkg -> List (DPair Package PkgStatus) -> ResolvedLib t

  Projections:
  
.deps : ResolvedLib t -> List (DPair Package PkgStatus)
  
.desc : ResolvedLib t -> Desc t
  
.hash : ResolvedLib t -> Hash
  
.name : ResolvedLib t -> PkgName
  
.pkg : ResolvedLib t -> Package
  
.status : ({rec:0} : ResolvedLib t) -> PkgStatus (pkg {rec:0})
.pkg : ResolvedLib t -> Package
  Totality: total
  Visibility: public export
pkg : ResolvedLib t -> Package
  Totality: total
  Visibility: public export
.hash : ResolvedLib t -> Hash
  Totality: total
  Visibility: public export
hash : ResolvedLib t -> Hash
  Totality: total
  Visibility: public export
.name : ResolvedLib t -> PkgName
  Totality: total
  Visibility: public export
name : ResolvedLib t -> PkgName
  Totality: total
  Visibility: public export
.desc : ResolvedLib t -> Desc t
  Totality: total
  Visibility: public export
desc : ResolvedLib t -> Desc t
  Totality: total
  Visibility: public export
.status : ({rec:0} : ResolvedLib t) -> PkgStatus (pkg {rec:0})
  Totality: total
  Visibility: public export
status : ({rec:0} : ResolvedLib t) -> PkgStatus (pkg {rec:0})
  Totality: total
  Visibility: public export
.deps : ResolvedLib t -> List (DPair Package PkgStatus)
  Totality: total
  Visibility: public export
deps : ResolvedLib t -> List (DPair Package PkgStatus)
  Totality: total
  Visibility: public export
nameStr : ResolvedLib t -> String
  Extracts the package name from a resolved library.

  Totality: total
  Visibility: export
reTag : ResolvedLib s -> Desc t -> ResolvedLib t
  Change the type-level tag of a resolved library.

  Totality: total
  Visibility: export
dependencies : ResolvedLib t -> List PkgName
  Extracts the dependencies of a resolved library.

  Totality: total
  Visibility: export
isInstalled : ResolvedLib t -> Bool
  Check if the given library is installed

  Totality: total
  Visibility: export
data AppStatus : Package -> Type
  Installation status of an Idris app.

  Totality: total
  Visibility: public export
  Constructors:
  
Missing : Hash -> AppStatus p
  The app has not been compiled and is therfore missing
  
Installed : Hash -> AppStatus p
  The app has been built but is not on the `PATH`.
  
BinInstalled : Hash -> AppStatus p
  The app has been built and a wrapper script has been added
  to `$PACK_DIR/bin`, so it should be on the `PATH`.
record ResolvedApp : (PkgDesc -> Type) -> Type
  A resolved application, which was cloned from a Git repo
  or looked up in the local file system. This comes with
  a fully parsed `PkgDesc` (representing the `.ipkg` file).

  Totality: total
  Visibility: public export
  Constructor: 
RA : (pkg : Package) -> Hash -> PkgName -> Desc t -> AppStatus pkg -> Body -> List (DPair Package PkgStatus) -> ResolvedApp t

  Projections:
  
.deps : ResolvedApp t -> List (DPair Package PkgStatus)
  
.desc : ResolvedApp t -> Desc t
  
.exec : ResolvedApp t -> Body
  
.hash : ResolvedApp t -> Hash
  
.name : ResolvedApp t -> PkgName
  
.pkg : ResolvedApp t -> Package
  
.status : ({rec:0} : ResolvedApp t) -> AppStatus (pkg {rec:0})
.pkg : ResolvedApp t -> Package
  Totality: total
  Visibility: public export
pkg : ResolvedApp t -> Package
  Totality: total
  Visibility: public export
.hash : ResolvedApp t -> Hash
  Totality: total
  Visibility: public export
hash : ResolvedApp t -> Hash
  Totality: total
  Visibility: public export
.name : ResolvedApp t -> PkgName
  Totality: total
  Visibility: public export
name : ResolvedApp t -> PkgName
  Totality: total
  Visibility: public export
.desc : ResolvedApp t -> Desc t
  Totality: total
  Visibility: public export
desc : ResolvedApp t -> Desc t
  Totality: total
  Visibility: public export
.status : ({rec:0} : ResolvedApp t) -> AppStatus (pkg {rec:0})
  Totality: total
  Visibility: public export
status : ({rec:0} : ResolvedApp t) -> AppStatus (pkg {rec:0})
  Totality: total
  Visibility: public export
.exec : ResolvedApp t -> Body
  Totality: total
  Visibility: public export
exec : ResolvedApp t -> Body
  Totality: total
  Visibility: public export
.deps : ResolvedApp t -> List (DPair Package PkgStatus)
  Totality: total
  Visibility: public export
deps : ResolvedApp t -> List (DPair Package PkgStatus)
  Totality: total
  Visibility: public export
nameStr : ResolvedApp t -> String
  Extracts the package name from a resolved application.

  Totality: total
  Visibility: export
dependencies : ResolvedApp t -> List PkgName
  Extracts the dependencies of a resolved application.

  Totality: total
  Visibility: export
reTag : ResolvedApp s -> Desc t -> ResolvedApp t
  Change the type-level tag of a resolved application.

  Totality: total
  Visibility: export
usePackagePath : ResolvedApp t -> Bool
  True, if the given application needs access to the
  folders where Idris package are installed.

  Totality: total
  Visibility: export
data LibOrApp : (PkgDesc -> Type) -> (PkgDesc -> Type) -> Type
  Either a resolved library or application tagged with the given tag.
  This is to be used in build plans, so applications come with the
  additional info whether we want to install a wrapper script or not.

  Totality: total
  Visibility: public export
  Constructors:
  
Lib : ResolvedLib t -> LibOrApp t s
  
App : Bool -> ResolvedApp s -> LibOrApp t s
dependencies : LibOrApp t s -> List PkgName
  Extract the dependencies of a resolved library or application.

  Totality: total
  Visibility: export
pkg : LibOrApp t s -> Package
  Extract the package of a resolved library or application.

  Totality: total
  Visibility: export
desc : LibOrApp t t -> Desc t
  Extract the description of a resolved library or application.

  Totality: total
  Visibility: export
name : LibOrApp t s -> PkgName
  Extract the package name of a resolved library or application.

  Totality: total
  Visibility: export
libName : LibOrApp t s -> Maybe PkgName
  Try to extract the package name of a resolved library.

  Totality: total
  Visibility: export
record DB_ : Type -> Type
  DB used for building packages. This includes
  the Idris commit to use, together with a curated list of
  known packages.

  Totality: total
  Visibility: public export
  Constructor: 
MkDB : URL -> c -> PkgVersion -> SortedMap PkgName (Package_ I c) -> DB_ c

  Projections:
  
.idrisCommit : DB_ c -> c
  
.idrisURL : DB_ c -> URL
  
.idrisVersion : DB_ c -> PkgVersion
  
.packages : DB_ c -> SortedMap PkgName (Package_ I c)

  Hint: 
Functor DB_
.idrisURL : DB_ c -> URL
  Totality: total
  Visibility: public export
idrisURL : DB_ c -> URL
  Totality: total
  Visibility: public export
.idrisCommit : DB_ c -> c
  Totality: total
  Visibility: public export
idrisCommit : DB_ c -> c
  Totality: total
  Visibility: public export
.idrisVersion : DB_ c -> PkgVersion
  Totality: total
  Visibility: public export
idrisVersion : DB_ c -> PkgVersion
  Totality: total
  Visibility: public export
.packages : DB_ c -> SortedMap PkgName (Package_ I c)
  Totality: total
  Visibility: public export
packages : DB_ c -> SortedMap PkgName (Package_ I c)
  Totality: total
  Visibility: public export
0 DB : Type
  Totality: total
  Visibility: public export
0 MetaDB : Type
  Totality: total
  Visibility: public export
setVersion : PkgVersion -> DB -> DB
  Sets the package version.

  Totality: total
  Visibility: export
traverseDB : Applicative f => (URL -> a -> f b) -> DB_ a -> f (DB_ b)
  Effectfully convert package descriptions in a DB

  Totality: total
  Visibility: export
printDB : DB -> String
  Convert a package collection to a valid TOML string.

  Totality: total
  Visibility: export
mergeUP : UserPackage -> UserPackage -> UserPackage
  Totality: total
  Visibility: export