Idris2Doc : Pack.Config.Types

Pack.Config.Types

(source)
Reexports
import public Data.List.Quantifiers
Definitions
data Autoload : Type
  Packages to automatically load in a REPL session
  in absence of an `.ipkg` file in scope.

  Totality: total
  Visibility: public export
  Constructors:
  
NoPkgs : Autoload
  Don't load any packages automatically (the default)
  
Installed : Autoload
  Load all installed packages of the current scope
  
AutoLibs : Autoload
  Use the packages from the list of packages to be installed
  automatically
  
AutoPkgs : List PkgName -> Autoload
  Use the given explicit list of packages
  
ForcePkgs : List PkgName -> Autoload
  Use the given explicit list of packages even in the
  presence of an `.ipkg` file.

  Hint: 
FromTOML Autoload
data QueryType : Type
  What to show when querying the data base

  Totality: total
  Visibility: public export
  Constructors:
  
NameOnly : QueryType
  Display only the matching packages' names
  
ShortDesc : QueryType
  Display names and short descriptions
  
Dependencies : QueryType
  List direct dependencies
  
Ipkg : QueryType
  Print the full `.ipkg` file
  
Details : QueryType
  List detailed information about a package
  
Tree : QueryType
  Print dependency tree
  
ReverseTree : QueryType
  Print inverse dependency tree
  (That is, a tree of packages depending on a given package)
data Codegen : Type
  Code generator to use

  Totality: total
  Visibility: public export
  Constructors:
  
Default : Codegen
  
Chez : Codegen
  
ChezSep : Codegen
  
Racket : Codegen
  
Gambit : Codegen
  
Node : Codegen
  
JavaScript : Codegen
  
RefC : Codegen
  
VMCode : Codegen
  
Other : String -> Codegen

  Hints:
  
FromTOML Codegen
  
Interpolation Codegen
fromString : String -> Codegen
  Totality: total
  Visibility: public export
data WithIpkg : Type
  Data type describing whether to search for an `.ipkg`
  file in one of the parent directories (the default), not
  to use an `.ipkg` file at all, or to use the one provided at
  the command line.
  
  This is only relevant when working with Idris source files
  directly, for instance when loading them into a REPL session.

  Totality: total
  Visibility: public export
  Constructors:
  
Search : CurDir -> WithIpkg
  Search for an `.ipkg` file in a parent directory.
  If an `.idr` file is provided, the parent directories
  of this file will be searched. If no `.idr` file is
  given, the current working directory will be search,
  which is given as an argument to this constructor.
  
None : WithIpkg
  Don't use an `.ipkg` file.
  
Use : File Abs -> WithIpkg
  Use the given `.ipkg` file, provided as a command line
  argument.
data RlwrapConfig : Type
  Data type describing whether `rlwrap` command should be used
  and which additional arguments should be passed to it.
  
  This is basically equivalent to `Maybe CmdArgList`, but
  separate type disallows confusion with `Maybe` from `MConfig`,
  i.e. between not being set and set to not to use `rlwrap`.

  Totality: total
  Visibility: public export
  Constructors:
  
DoNotUseRlwrap : RlwrapConfig
  
UseRlwrap : CmdArgList -> RlwrapConfig

  Hint: 
FromTOML RlwrapConfig
record Config_ : (Type -> Type) -> Type -> Type
  User-defined configuration
  
  @ f : This is used to represent the context of values.
        When we use the config as an environment for running pack
        programs, the context will be set to `I` (the identity function
        for types). This means, all fields will be mandatory.
        For updating the configuration from a `pack.toml` file,
        we use context `Maybe`, because all values will be optional.
  
  @ c : This is the type of commit given for custom packages.

  Totality: total
  Visibility: public export
  Constructor: 
MkConfig : f DBName -> Maybe URL -> Maybe c -> List c -> Maybe URL -> Maybe c -> f FilePath -> f Bool -> f Bool -> f Bool -> f Bool -> f Bool -> f Bool -> f Bool -> f (List PkgName) -> f Bool -> f Bool -> f Bool -> f WithIpkg -> f RlwrapConfig -> f CmdArgList -> f (List PkgName) -> f (List PkgName) -> f Autoload -> f CustomMap -> f QueryType -> f LogLevel -> f Codegen -> f Body -> f (SortedMap String LogLevel) -> f Bool -> Config_ f c

  Projections:
  
.allIdrisCommits : Config_ f c -> List c
  All Idris commits mentioned in used configs
  
.autoApps : Config_ f c -> f (List PkgName)
  Applications to install automatically
  
.autoLibs : Config_ f c -> f (List PkgName)
  Libraries to install automatically
  
.autoLoad : Config_ f c -> f Autoload
  Libraries to automatically load in a REPL session
  
.bootstrap : Config_ f c -> f Bool
  Whether to bootstrap when building Idris2
  
.bootstrapStage3 : Config_ f c -> f Bool
  Whether to rebuild Idris2 with the stage 2 compiler
  
.codegen : Config_ f c -> f Codegen
  Codegen to use
  
.collection : Config_ f c -> f DBName
  Package collection to use
  
.custom : Config_ f c -> f CustomMap
  Customizations to the package data base
  
.extraArgs : Config_ f c -> f CmdArgList
  Any extra arguments to pass to Idris2 executable.
  
.gcPrompt : Config_ f c -> f Bool
  Whether to prompt for a confirmation when
  running the garbage collector for removing no longer used
  installation directories.
  
.gcPurge : Config_ f c -> f Bool
  Whether to remove not only stuff compiled with outdated version
  of the compiler but also libs and apps whose install hash does not
  match the current one.
  
.gitInit : Config_ f c -> f Bool
  Whether to initialize git.
  
.idrisCommit : Config_ f c -> Maybe c
  Custom Idris commit
  This overrides the one from the package collection if not
  set to `Nothing`.
  
.idrisURL : Config_ f c -> Maybe URL
  URL to a custom Idris repo
  This overrides the one from the package collection if not
  set to `Nothing`.
  
.levels : Config_ f c -> f (SortedMap String LogLevel)
  Default LogLevels for different commands
  
.logLevel : Config_ f c -> f LogLevel
  Verbosity of the Log
  
.output : Config_ f c -> f Body
  Name of output file when compiling Idris source files
  
.packCommit : Config_ f c -> Maybe c
  Custom pack branch to use (default is `main`)
  
.packURL : Config_ f c -> Maybe URL
  Custom pack repo
  
.queryType : Config_ f c -> f QueryType
  Type of query to run
  
.rlwrap : Config_ f c -> f RlwrapConfig
  Whether to use `rlwrap` to run a REPL session
  
.safetyPrompt : Config_ f c -> f Bool
  Whether to prompt for a confirmation when
  building or installing a package with custom
  build or install hooks.
  
.scheme : Config_ f c -> f FilePath
  Scheme executable to use
  
.skipTests : Config_ f c -> f Bool
  Whether to skip tests during collection checking
  
.useKatla : Config_ f c -> f Bool
  Whether to use katla to add semantically highlighted source code
  to the library docs.
  
.warnDepends : Config_ f c -> f Bool
  Whether to issue a warning in presence of a local `depends` directory
  
.whitelist : Config_ f c -> f (List PkgName)
  List of package names, for which we will not issue a safety prompt
  in case of custom `.ipkg` hooks, even if `safetyPrompt` is set
  to `True`
  
.withDocs : Config_ f c -> f Bool
  Whether to install the library docs as well
  
.withIpkg : Config_ f c -> f WithIpkg
  The `.ipkg` file to use (if any) when starting a REPL session
  
.withSrc : Config_ f c -> f Bool
  Whether to install the library sources as well
.collection : Config_ f c -> f DBName
  Package collection to use

  Totality: total
  Visibility: public export
collection : Config_ f c -> f DBName
  Package collection to use

  Totality: total
  Visibility: public export
.idrisURL : Config_ f c -> Maybe URL
  URL to a custom Idris repo
  This overrides the one from the package collection if not
  set to `Nothing`.

  Totality: total
  Visibility: public export
idrisURL : Config_ f c -> Maybe URL
  URL to a custom Idris repo
  This overrides the one from the package collection if not
  set to `Nothing`.

  Totality: total
  Visibility: public export
.idrisCommit : Config_ f c -> Maybe c
  Custom Idris commit
  This overrides the one from the package collection if not
  set to `Nothing`.

  Totality: total
  Visibility: public export
idrisCommit : Config_ f c -> Maybe c
  Custom Idris commit
  This overrides the one from the package collection if not
  set to `Nothing`.

  Totality: total
  Visibility: public export
.allIdrisCommits : Config_ f c -> List c
  All Idris commits mentioned in used configs

  Totality: total
  Visibility: public export
allIdrisCommits : Config_ f c -> List c
  All Idris commits mentioned in used configs

  Totality: total
  Visibility: public export
.packURL : Config_ f c -> Maybe URL
  Custom pack repo

  Totality: total
  Visibility: public export
packURL : Config_ f c -> Maybe URL
  Custom pack repo

  Totality: total
  Visibility: public export
.packCommit : Config_ f c -> Maybe c
  Custom pack branch to use (default is `main`)

  Totality: total
  Visibility: public export
packCommit : Config_ f c -> Maybe c
  Custom pack branch to use (default is `main`)

  Totality: total
  Visibility: public export
.scheme : Config_ f c -> f FilePath
  Scheme executable to use

  Totality: total
  Visibility: public export
scheme : Config_ f c -> f FilePath
  Scheme executable to use

  Totality: total
  Visibility: public export
.bootstrap : Config_ f c -> f Bool
  Whether to bootstrap when building Idris2

  Totality: total
  Visibility: public export
bootstrap : Config_ f c -> f Bool
  Whether to bootstrap when building Idris2

  Totality: total
  Visibility: public export
.bootstrapStage3 : Config_ f c -> f Bool
  Whether to rebuild Idris2 with the stage 2 compiler

  Totality: total
  Visibility: public export
bootstrapStage3 : Config_ f c -> f Bool
  Whether to rebuild Idris2 with the stage 2 compiler

  Totality: total
  Visibility: public export
.safetyPrompt : Config_ f c -> f Bool
  Whether to prompt for a confirmation when
  building or installing a package with custom
  build or install hooks.

  Totality: total
  Visibility: public export
safetyPrompt : Config_ f c -> f Bool
  Whether to prompt for a confirmation when
  building or installing a package with custom
  build or install hooks.

  Totality: total
  Visibility: public export
.gcPrompt : Config_ f c -> f Bool
  Whether to prompt for a confirmation when
  running the garbage collector for removing no longer used
  installation directories.

  Totality: total
  Visibility: public export
gcPrompt : Config_ f c -> f Bool
  Whether to prompt for a confirmation when
  running the garbage collector for removing no longer used
  installation directories.

  Totality: total
  Visibility: public export
.gcPurge : Config_ f c -> f Bool
  Whether to remove not only stuff compiled with outdated version
  of the compiler but also libs and apps whose install hash does not
  match the current one.

  Totality: total
  Visibility: public export
gcPurge : Config_ f c -> f Bool
  Whether to remove not only stuff compiled with outdated version
  of the compiler but also libs and apps whose install hash does not
  match the current one.

  Totality: total
  Visibility: public export
.warnDepends : Config_ f c -> f Bool
  Whether to issue a warning in presence of a local `depends` directory

  Totality: total
  Visibility: public export
warnDepends : Config_ f c -> f Bool
  Whether to issue a warning in presence of a local `depends` directory

  Totality: total
  Visibility: public export
.skipTests : Config_ f c -> f Bool
  Whether to skip tests during collection checking

  Totality: total
  Visibility: public export
skipTests : Config_ f c -> f Bool
  Whether to skip tests during collection checking

  Totality: total
  Visibility: public export
.whitelist : Config_ f c -> f (List PkgName)
  List of package names, for which we will not issue a safety prompt
  in case of custom `.ipkg` hooks, even if `safetyPrompt` is set
  to `True`

  Totality: total
  Visibility: public export
whitelist : Config_ f c -> f (List PkgName)
  List of package names, for which we will not issue a safety prompt
  in case of custom `.ipkg` hooks, even if `safetyPrompt` is set
  to `True`

  Totality: total
  Visibility: public export
.withSrc : Config_ f c -> f Bool
  Whether to install the library sources as well

  Totality: total
  Visibility: public export
withSrc : Config_ f c -> f Bool
  Whether to install the library sources as well

  Totality: total
  Visibility: public export
.withDocs : Config_ f c -> f Bool
  Whether to install the library docs as well

  Totality: total
  Visibility: public export
withDocs : Config_ f c -> f Bool
  Whether to install the library docs as well

  Totality: total
  Visibility: public export
.useKatla : Config_ f c -> f Bool
  Whether to use katla to add semantically highlighted source code
  to the library docs.

  Totality: total
  Visibility: public export
useKatla : Config_ f c -> f Bool
  Whether to use katla to add semantically highlighted source code
  to the library docs.

  Totality: total
  Visibility: public export
.withIpkg : Config_ f c -> f WithIpkg
  The `.ipkg` file to use (if any) when starting a REPL session

  Totality: total
  Visibility: public export
withIpkg : Config_ f c -> f WithIpkg
  The `.ipkg` file to use (if any) when starting a REPL session

  Totality: total
  Visibility: public export
.rlwrap : Config_ f c -> f RlwrapConfig
  Whether to use `rlwrap` to run a REPL session

  Totality: total
  Visibility: public export
rlwrap : Config_ f c -> f RlwrapConfig
  Whether to use `rlwrap` to run a REPL session

  Totality: total
  Visibility: public export
.extraArgs : Config_ f c -> f CmdArgList
  Any extra arguments to pass to Idris2 executable.

  Totality: total
  Visibility: public export
extraArgs : Config_ f c -> f CmdArgList
  Any extra arguments to pass to Idris2 executable.

  Totality: total
  Visibility: public export
.autoLibs : Config_ f c -> f (List PkgName)
  Libraries to install automatically

  Totality: total
  Visibility: public export
autoLibs : Config_ f c -> f (List PkgName)
  Libraries to install automatically

  Totality: total
  Visibility: public export
.autoApps : Config_ f c -> f (List PkgName)
  Applications to install automatically

  Totality: total
  Visibility: public export
autoApps : Config_ f c -> f (List PkgName)
  Applications to install automatically

  Totality: total
  Visibility: public export
.autoLoad : Config_ f c -> f Autoload
  Libraries to automatically load in a REPL session

  Totality: total
  Visibility: public export
autoLoad : Config_ f c -> f Autoload
  Libraries to automatically load in a REPL session

  Totality: total
  Visibility: public export
.custom : Config_ f c -> f CustomMap
  Customizations to the package data base

  Totality: total
  Visibility: public export
custom : Config_ f c -> f CustomMap
  Customizations to the package data base

  Totality: total
  Visibility: public export
.queryType : Config_ f c -> f QueryType
  Type of query to run

  Totality: total
  Visibility: public export
queryType : Config_ f c -> f QueryType
  Type of query to run

  Totality: total
  Visibility: public export
.logLevel : Config_ f c -> f LogLevel
  Verbosity of the Log

  Totality: total
  Visibility: public export
logLevel : Config_ f c -> f LogLevel
  Verbosity of the Log

  Totality: total
  Visibility: public export
.codegen : Config_ f c -> f Codegen
  Codegen to use

  Totality: total
  Visibility: public export
codegen : Config_ f c -> f Codegen
  Codegen to use

  Totality: total
  Visibility: public export
.output : Config_ f c -> f Body
  Name of output file when compiling Idris source files

  Totality: total
  Visibility: public export
output : Config_ f c -> f Body
  Name of output file when compiling Idris source files

  Totality: total
  Visibility: public export
.levels : Config_ f c -> f (SortedMap String LogLevel)
  Default LogLevels for different commands

  Totality: total
  Visibility: public export
levels : Config_ f c -> f (SortedMap String LogLevel)
  Default LogLevels for different commands

  Totality: total
  Visibility: public export
.gitInit : Config_ f c -> f Bool
  Whether to initialize git.

  Totality: total
  Visibility: public export
gitInit : Config_ f c -> f Bool
  Whether to initialize git.

  Totality: total
  Visibility: public export
0 IConfig : Type -> Type
  Configuration with mandatory fields.

  Totality: total
  Visibility: public export
0 MConfig : Type -> Type
  Configuration with optional fields.

  Totality: total
  Visibility: public export
0 MetaConfig : Type
  Application config with meta commits not yet resolved.

  Totality: total
  Visibility: public export
0 Config : Type
  Fully resolved application config.

  Totality: total
  Visibility: public export
0 UserConfig : Type
  User-defined adjustments to the application config.

  Totality: total
  Visibility: public export
traverse : Applicative f => (URL -> a -> f b) -> URL -> Config_ I a -> f (Config_ I b)
  Effectfully convert all custom package descriptions
  stored in a configuration. This is mainly used to
  resolve meta commits to mere commits.

  Totality: total
  Visibility: export
configToLogRef : Config => LogRef
  This allows us to use a `Config` in scope when we
  need an auto-implicit `LogLevel` for logging.

  Totality: total
  Visibility: export
metaConfigToLogRef : MetaConfig => LogRef
  This allows us to use a `MetaConfig` in scope when we
  need an auto-implicit `LogLevel` for logging.

  Totality: total
  Visibility: export
mergeRight : SortedMap k v -> SortedMap k v -> SortedMap k v
  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 8
init : CurDir => DBName -> MetaConfig
  Initial config

  Totality: total
  Visibility: export
update : IConfig c -> MConfig c -> IConfig c
  Update a config with optional settings

  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 7
data HasIdris : Config -> DB -> Type
  Proof that we have verified that the required Idris
  compiler has been installed.

  Totality: total
  Visibility: public export
  Constructor: 
ItHasIdris : HasIdris c db
0 LibCache : Type
  Cache used during package resolution

  Totality: total
  Visibility: public export
emptyCache : HasIO io => io LibCache
  Create an empty library cache

  Totality: total
  Visibility: export
cacheLib : HasIO io => LibCache => PkgName -> ResolvedLib U -> io (ResolvedLib U)
  Cache a resolved library

  Totality: total
  Visibility: export
lookupLib : HasIO io => LibCache => PkgName -> io (Maybe (ResolvedLib U))
  Lookup a library in the cache

  Totality: total
  Visibility: export
uncacheLib : HasIO io => LibCache => PkgName -> io ()
  Lookup a library in the cache

  Totality: total
  Visibility: export
record Env : Type
  Environment used by most pack methods, consisting of
  the `PACK_DIR` environment variable, the user-defined
  application configuratin, and the data collection to
  use.

  Totality: total
  Visibility: public export
  Constructor: 
MkEnv : PackDirs -> TmpDir -> Config -> LibCache -> DB -> SortedMap PkgName Package -> LineBufferingCmd -> Clock UTC -> Env

  Projections:
  
.all : Env -> SortedMap PkgName Package
  
.cache : Env -> LibCache
  
.clock : Env -> Clock UTC
  
.config : Env -> Config
  
.db : Env -> DB
  
.linebuf : Env -> LineBufferingCmd
  
.packDirs : Env -> PackDirs
  
.tmpDir : Env -> TmpDir

  Hints:
  
Env => Config
  
Env => DB
  
IdrisEnv => Env
  
Env => LibCache
  
Env => LineBufferingCmd
  
Env => PackDirs
  
Env => TmpDir
.packDirs : Env -> PackDirs
  Totality: total
  Visibility: public export
packDirs : Env -> PackDirs
  Totality: total
  Visibility: public export
.tmpDir : Env -> TmpDir
  Totality: total
  Visibility: public export
tmpDir : Env -> TmpDir
  Totality: total
  Visibility: public export
.config : Env -> Config
  Totality: total
  Visibility: public export
config : Env -> Config
  Totality: total
  Visibility: public export
.cache : Env -> LibCache
  Totality: total
  Visibility: public export
cache : Env -> LibCache
  Totality: total
  Visibility: public export
.db : Env -> DB
  Totality: total
  Visibility: public export
db : Env -> DB
  Totality: total
  Visibility: public export
.all : Env -> SortedMap PkgName Package
  Totality: total
  Visibility: public export
all : Env -> SortedMap PkgName Package
  Totality: total
  Visibility: public export
.linebuf : Env -> LineBufferingCmd
  Totality: total
  Visibility: public export
linebuf : Env -> LineBufferingCmd
  Totality: total
  Visibility: public export
.clock : Env -> Clock UTC
  Totality: total
  Visibility: public export
clock : Env -> Clock UTC
  Totality: total
  Visibility: public export
nanoString : Env => String
  Returns the current nanoseconds as a string.

  Totality: total
  Visibility: export
envToPackDirs : Env => PackDirs
  This allows us to use an `Env` in scope when we
  need an auto-implicit `PackDirs`.

  Totality: total
  Visibility: export
envToTmpDir : Env => TmpDir
  This allows us to use an `Env` in scope when we
  need an auto-implicit `TmpDir`.

  Totality: total
  Visibility: export
envToCache : Env => LibCache
  This allows us to use an `Env` in scope when we
  need an auto-implicit `LibCache`.

  Totality: total
  Visibility: export
envToConfig : Env => Config
  This allows us to use an `Env` in scope when we
  need an auto-implicit `Config`.

  Totality: total
  Visibility: export
envToDB : Env => DB
  This allows us to use an `Env` in scope when we
  need an auto-implicit `DB`.

  Totality: total
  Visibility: export
envToLinebuf : Env => LineBufferingCmd
  This allows us to use an `Env` in scope when we
  need an auto-implicit `LineBufferingCmd`.

  Totality: total
  Visibility: export
record IdrisEnv : Type
  Like `Pack.Config.Types.Env`, but with an erased proof
  that the Idris compiler installation has been verified.

  Totality: total
  Visibility: public export
  Constructor: 
MkIdrisEnv : (env : Env) -> TTCVersion -> (0 _ : HasIdris (env .config) (env .db)) -> IdrisEnv

  Projections:
  
.env : IdrisEnv -> Env
  
0 .prf : ({rec:0} : IdrisEnv) -> HasIdris ((env {rec:0}) .config) ((env {rec:0}) .db)
  
.ttc : IdrisEnv -> TTCVersion

  Hints:
  
IdrisEnv => Env
  
IdrisEnv => TTCVersion
.env : IdrisEnv -> Env
  Totality: total
  Visibility: public export
env : IdrisEnv -> Env
  Totality: total
  Visibility: public export
.ttc : IdrisEnv -> TTCVersion
  Totality: total
  Visibility: public export
ttc : IdrisEnv -> TTCVersion
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : IdrisEnv) -> HasIdris ((env {rec:0}) .config) ((env {rec:0}) .db)
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : IdrisEnv) -> HasIdris ((env {rec:0}) .config) ((env {rec:0}) .db)
  Totality: total
  Visibility: public export
idrisEnvToEnv : IdrisEnv => Env
  This allows us to use an `IdrisEnv` in scope when we
  need an auto-implicit `Env`.

  Totality: total
  Visibility: export
idrisEnvToTTC : IdrisEnv => TTCVersion
  This allows us to use an `IdrisEnv` in scope when we
  need an auto-implicit `TTCVersion`.

  Totality: total
  Visibility: export
interface Arg : Type -> Type
  An interface for parsing the argument list of a pack command

  Parameters: a
Methods:
  
argDesc_ : String
  
readArg : List String -> Maybe (a, List String)

Implementations:
  
Arg a => Arg (Maybe a)
  
CurDir => Arg (File Abs)
  
CurDir => Arg (Path Abs)
  
CurDir => Arg PkgOrIpkg
  
Arg PkgName
  
Arg PkgType
  
Arg CmdArgList
  
Arg (List PkgName)
  
Arg Body
  
Arg DBName
  
Arg String
  
Arg PkgQuery
  
Arg FuzzyQuery
  
Arg ConfiguredCmd
  
Arg TrivialCmd
  
Arg Cmd
argDesc_ : Arg a => String
  Totality: total
  Visibility: public export
readArg : Arg a => List String -> Maybe (a, List String)
  Totality: total
  Visibility: public export
argDesc : (0 a : Type) -> Arg a => String
  Utility version of `argDesc_` with an explicit erased type argument.

  Totality: total
  Visibility: public export
parseSingleMaybe : (String -> Maybe a) -> List String -> Maybe (a, List String)
  Utility for implementing `readArg` via a function reading a single string.

  Totality: total
  Visibility: export
parseSingle : (String -> Either e a) -> List String -> Maybe (a, List String)
  Utility for implementing `readArg` via a function reading a single string.

  Totality: total
  Visibility: export
readSingle : (String -> a) -> List String -> Maybe (a, List String)
  Utility for implementing `readArg` via a function reading a single string.

  Totality: total
  Visibility: export
interface Command : Type -> Type
  Interface representing pack commands. We abstract over this
  because both pack and pack-admin accept different types of
  commands, but both use the same functionality for reading
  the application config based on the command they use.
  
  A command `c` is expected to be an enum type. This interface provides
  a name and detailed description for each command, as well as the types of
  arguments a command takes.
  
  This allows us to generate useful error messages when the wrong type
  of argument is passed to a command. It also allows us to implement the
  parsing of commands only once.

  Parameters: c
Methods:
  
defaultCommand : c
  The command to use if only command line options but
  not command is given.
  
appName : String
  Name of the application in question
  
cmdName : c -> String
  Name of command in question
  
defaultLevel : c -> LogLevel
  The default log level to use.
  
desc : c -> String
  Detailed usage description of the command
  
usage : Lazy String
  General usage of the application in question
  
0 ArgTypes : c -> List Type
  Types of arguments required by the given command
  
readCommand_ : String -> Maybe c
  Tries to read a command from a String
  
readArgs : CurDir => (cmd : c) -> All Arg (ArgTypes cmd)
  List of argument readers for the current command
  
adjConfig_ : HasIO io => PackDirs => TmpDir => (cmd : c) -> All I (ArgTypes cmd) -> MetaConfig -> EitherT PackErr io MetaConfig
  Some commands overwrite certain aspects of the user-defined
  config. For instance, `pack switch latest` must overwrite the
  package collection read from the `pack.toml` files with the
  latest package collection available.
defaultCommand : Command c => c
  The command to use if only command line options but
  not command is given.

  Totality: total
  Visibility: public export
appName : Command c => String
  Name of the application in question

  Totality: total
  Visibility: public export
cmdName : Command c => c -> String
  Name of command in question

  Totality: total
  Visibility: public export
defaultLevel : Command c => c -> LogLevel
  The default log level to use.

  Totality: total
  Visibility: public export
desc : Command c => c -> String
  Detailed usage description of the command

  Totality: total
  Visibility: public export
usage : Command c => Lazy String
  General usage of the application in question

  Totality: total
  Visibility: public export
0 ArgTypes : Command c => c -> List Type
  Types of arguments required by the given command

  Totality: total
  Visibility: public export
readCommand_ : Command c => String -> Maybe c
  Tries to read a command from a String

  Totality: total
  Visibility: public export
readArgs : {auto __con : Command c} -> CurDir => (cmd : c) -> All Arg (ArgTypes cmd)
  List of argument readers for the current command

  Totality: total
  Visibility: public export
adjConfig_ : {auto __con : Command c} -> HasIO io => PackDirs => TmpDir => (cmd : c) -> All I (ArgTypes cmd) -> MetaConfig -> EitherT PackErr io MetaConfig
  Some commands overwrite certain aspects of the user-defined
  config. For instance, `pack switch latest` must overwrite the
  package collection read from the `pack.toml` files with the
  latest package collection available.

  Totality: total
  Visibility: public export
usageHeader : CurDir => Command c => Maybe c -> String
  Header line for a usage string

  Totality: total
  Visibility: export
usageDesc : CurDir => Command c => Maybe c -> String
  Detailed description how to use the given command.
  
  This is a general description of the application
  in case the argument is `Nothing`.

  Totality: total
  Visibility: export
0 Args : Command c => c -> Type
  Type of arguments expected by the given command

  Totality: total
  Visibility: public export
0 CommandWithArgs : (c : Type) -> Command c => Type
  A pack command together with its list of arguments

  Totality: total
  Visibility: public export
readCommand : (0 c : Type) -> {auto {conArg:11582} : Command c} -> CurDir -> List String -> Either PackErr (CommandWithArgs c)
  Convenience alias for `readCommand_` with an explicit
  erased argument for the command type.

  Totality: total
  Visibility: export
adjConfig : HasIO io => {auto {conArg:11662} : Command c} -> PackDirs => TmpDir => CommandWithArgs c -> MetaConfig -> EitherT PackErr io MetaConfig
  Some commands overwrite certain aspects of the user-defined
  config. For instance, `pack switch latest` must overwrite the
  package collection read from the `pack.toml` files with the
  latest package collection available.

  Totality: total
  Visibility: export