HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

ModuleAgda-2.7.0.1Haskell2010

Agda.Interaction.Library

Library management.

Sample use:

    -- Get libraries as listed in .agda/libraries file.
    libs <- getInstalledLibraries Nothing

    -- Get the libraries (and immediate paths) relevant for projectRoot.
    -- This involves locating and processing the .agda-lib file for the project.
    (libNames, includePaths) <-  getDefaultLibraries projectRoot True

    -- Get include paths of depended-on libraries.
    resolvedPaths <- libraryIncludePaths Nothing libs libNames

    let allPaths = includePaths ++ resolvedPaths
  • 9 types
  • 13 values
  • PackageAgda-2.7.0.1
  • Exports22
  • LanguageHaskell2010
  • LicenceMIT
  • SourceLibrary.hs
valuegetAgdaAppDir :: IO FilePath
#

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 for the data files that Agda needs (e.g. the primitive modules).)

valuegetDefaultLibraries
  1. :: FilePath

    Project root.

  2. -> Bool

    Use defaults if no .agda-lib file exists for this project?

  3. -> LibM ([LibName], [FilePath])

    The returned LibNames are all non-empty strings.

#

Get dependencies and include paths for given project root:

Look for .agda-lib files according to findAgdaLibFiles. If none are found, use default dependencies (according to defaults file) and current directory (project root).

valuegetInstalledLibraries
  1. :: Maybe FilePath

    Override the default libraries file?

  2. -> LibM [AgdaLibFile]

    Content of library files. (Might have empty LibNames.)

#

Parse the descriptions of the libraries Agda knows about.

Returns none if there is no libraries file.

valuelibraryIncludePaths
  1. :: Maybe FilePath

    libraries file (error reporting only).

  2. -> [AgdaLibFile]

    Libraries Agda knows about.

  3. -> [LibName]

    (Non-empty) library names to be resolved to (lists of) pathes.

  4. -> LibM [FilePath]

    Resolved pathes (no duplicates). Contains "." if [LibName] does.

#

Get all include pathes for a list of libraries to use.

datadata OptionsPragma
#

The options from an OPTIONS pragma (or a .agda-lib file).

In the future it might be nice to switch to a more structured representation. Note that, currently, there is not a one-to-one correspondence between list elements and options.

Constructors

Instances5Show, Semigroup, Monoid, NFData, EmbPrj
datadata AgdaLibFile
#

Content of a .agda-lib file.

Constructors

Instances4Show, Generic, NFData, Rep
datadata LibWarning
#

Constructors

Instances6Show, Generic, NFData, Pretty, EmbPrj, Rep
datadata LibPositionInfo
#

Information about which .agda-lib file we are reading and from where in the libraries file it came from.

Constructors

Instances5Show, Generic, NFData, EmbPrj, Rep
datadata ProjectConfig
#

A file can either belong to a project located at a given root containing one or more .agda-lib files, or be part of the default project.

Constructors

Instances3Generic, NFData, Rep

Exported for testing

4 declarations
datadata VersionView
#

Library names are structured into the base name and a suffix of version numbers, e.g. mylib-1.2.3. The version suffix is optional.

Constructors

  • VersionView
    • vvBase :: LibName

      Actual library name.

    • vvNumbers :: [Integer]

      Major version, minor version, subminor version, etc., all non-negative. Note: a priori, there is no reason why the version numbers should be Ints.

Instances2Eq, Show
valueversionView :: LibName -> VersionView
#

Split a library name into basename and a list of version numbers.

versionView "foo-1.2.3"    == VersionView "foo" [1, 2, 3]
versionView "foo-01.002.3" == VersionView "foo" [1, 2, 3]

Note that because of leading zeros, versionView is not injective. (unVersionView . versionView would produce a normal form.)

valuefindLib' :: (a -> LibName) -> LibName -> [a] -> [a]
#

Generalized version of findLib for testing.

findLib' id "a"   [ "a-1", "a-02", "a-2", "b" ] == [ "a-02", "a-2" ]
findLib' id "a"   [ "a", "a-1", "a-01", "a-2", "b" ] == [ "a" ]
findLib' id "a-1" [ "a", "a-1", "a-01", "a-2", "b" ] == [ "a-1", "a-01" ]
findLib' id "a-2" [ "a", "a-1", "a-01", "a-2", "b" ] == [ "a-2" ]
findLib' id "c"   [ "a", "a-1", "a-01", "a-2", "b" ] == []