Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Setup

Description

Agda's self-setup.

Synopsis

- getAgdaAppDir :: IO FilePath
- getDataDir :: IO FilePath
- getDataFileName :: FilePath -> IO FilePath
- setup :: Bool -> IO ()

# Documentation

getAgdaAppDir :: IO FilePath Source #

Get the path to `~/.agda` (system-specific). Can be overwritten by the `AGDA_DIR` environment variable.

(This is not to be confused with the directory `getDataDir` for the data files that Agda needs (e.g. the primitive modules).)

getDataDir :: IO FilePath Source #

This overrides the `getDataDir` from '`Paths_Agda'`. See the documentation for the `--print-agda-data-dir` flag.

getDataFileName :: FilePath -> IO FilePath Source #

This overrides the `getDataFileName` from '`Paths_Agda'`.

setup :: Bool -> IO () Source #

`False`: Check whether we need to setup Agda. This function can be called when starting up Agda.

`True`: force a setup e.g. when passing Agda option `--setup`.

Copies the embedded data files to the designated data directory.