Pack.Runner.Database

Definitions

data Safe : PkgDesc -> Type

  Proof that the safety aspects of a value have been checked.
  Right now, this is restricted to `.ipkg` files (and thus, resolved
  libs and apps) with custom build and install hooks.

Totality: total
Visibility: export
Constructor: 

IsSafe : Safe d

0 SafeLib : Type

  Alias for `ResolvedLib Safe`

Totality: total
Visibility: public export

data NotPack : PkgDesc -> Type

  Proof that an app is not pack, i.e. does not have an
  executable called pack. We want to make sure that
  users don't inadvertently overwrite the pack installation.

Totality: total
Visibility: export
Constructor: 

IsNotPack : Safe d -> NotPack d

0 toSafe : NotPack d -> Safe d

  Extract the `Safe d` wrapped in a `NotPack d`

Totality: total
Visibility: export

0 SafeApp : Type

  Alias for `ResolvedApp Safe`

Totality: total
Visibility: public export

0 SafePkg : Type

  Alias for `Either SafeLib SafeApp`

Totality: total
Visibility: public export

notPackIsSafe : Desc NotPack -> Desc Safe

  This holds, sind `NotPack d` implies `Safe d` as shown by
  `toSafe`.

Totality: total
Visibility: export

safe : HasIO io => Env => Desc t -> EitherT PackErr io (Desc Safe)

  Check if a package has special build- or install hooks
  defined, and if yes, prompt the user
  before continuing (unless `safetyPrompt` in the
  `Config` is set to `False` or the package's name is listed
  in the whitelist of safe packages).

Totality: total
Visibility: export

notPack : HasIO io => Env => Desc t -> EitherT PackErr io (Desc NotPack)

  Like `safe` but verify also that the package does not
  produce an executable called "pack"

Totality: total
Visibility: export

parseLibIpkg : HasIO io => Env => File Abs -> File Abs -> EitherT PackErr io (Desc Safe)

  Parse an `.ipkg` file and check if it has custom build hooks.

Totality: total
Visibility: export

findAndParseLocalIpkg : HasIO io => Env => PkgOrIpkg -> EitherT PackErr io (Desc Safe)

  Parse an `.ipkg` file from a command line arg or a local
  package given as a package name and check if it has custom build hooks.

Totality: total
Visibility: export

refinePkg : HasIO io => CurDir => Maybe PkgOrIpkg -> EitherT PackErr io PkgOrIpkg

  Returns present package, or else tries to find the only loca `.ipkg` file.

Totality: total
Visibility: export

parseAppIpkg : HasIO io => Env => File Abs -> File Abs -> EitherT PackErr io (Desc NotPack)

  Parse an `.ipkg` file representing an application
  and check if it has no custom build hooks and does not produce
  an executable called "pack".

Totality: total
Visibility: export

safeLib : HasIO io => Env => ResolvedLib t -> EitherT PackErr io SafeLib

  Check if a resolved library is safe to install (prompt, if it uses
  custom build hooks in its `.ipkg` file).

Totality: total
Visibility: export

safeApp : HasIO io => Env => ResolvedApp t -> EitherT PackErr io SafeApp

  Check if a resolved app is safe to install (prompt, if it uses
  custom build hooks in its `.ipkg` file).
  
  This fails if the app produces an executable called "pack": We don't
  want to overwrite the pack installation.

Totality: total
Visibility: export

checkLOA : HasIO io => Env => LibOrApp U U -> EitherT PackErr io SafePkg

  Runs `safeLib` or `safeApp` on a library or app.

Totality: total
Visibility: export

withPkgEnv : HasIO io => Env => PkgName -> Package -> (Path Abs -> EitherT PackErr io a) -> EitherT PackErr io a

  Run a pack action in the directory of a (possibly cloned) package.

Totality: total
Visibility: export

appStatus : HasIO io => Env => PkgName -> Hash -> (p : Package) -> Body -> EitherT PackErr io (AppStatus p)

  Generates the `AppStatus` of a package representing an application.

Totality: total
Visibility: export

resolveLib : HasIO io => Env => {default [<] _ : SnocList PkgName} -> PkgName -> EitherT PackErr io (ResolvedLib U)

  Try to fully resolve a library given as a package name.
  This will look up the library in the current package collection
  and will fetch and read its (possibly cached) `.ipkg` file.

Totality: total
Visibility: export

resolveApp : HasIO io => Env => PkgName -> EitherT PackErr io (ResolvedApp U)

  Try to fully resolve an application given as a package name.
  This will look up the app in the current package collection
  and will fetch and read its (possibly cached) `.ipkg` file.

Visibility: export

resolveAny : HasIO io => Env => InstallType -> PkgName -> EitherT PackErr io (LibOrApp U U)

  Try to fully resolve an application or library given as a package.
  This will look up the package name in the current package collection
  and will fetch and read its (possibly cached) `.ipkg` file.

Visibility: export

appPath : HasIO io => PkgName -> Env -> EitherT PackErr io ()

  Prints the absolute path of an application's installed executable
  to stdout. This is used in the wrapper scripts we use for invoking
  the correct version of apps such as `idris2-lsp`, the version of
  which depend on the `pack.toml` files currently in scope.

Visibility: export

checkDeletable : HasIO io => Env => List PkgName -> EitherT PackErr io ()

  Verifies that the given list of libraries is safe to be deleted

Visibility: export

garbageCollector : HasIO io => Env -> EitherT PackErr io ()

  Delete installations from previous package collections.

Totality: total
Visibility: export

transitiveDeps : HasIO io => Env => List (InstallType, PkgName) -> EitherT PackErr io (List (LibOrApp U U))

  Resolve the (transitive) dependencies of the given libs and apps.

Visibility: export

plan : HasIO io => Env => List (InstallType, PkgName) -> EitherT PackErr io (List SafePkg)

  Create a build plan for the given list of packages and apps
  plus their dependencies.
  
  All packages depend on the prelude and
  base, so we make sure these are installed as well.

Visibility: export