HORIZON HASKELLDocslts/ghc-9.14.x3e2d5682026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 9.14.1 · lts/ghc-9.14.x · 3e2d568 · 2026-10-11

ModuleAgda-2.8.0.2Haskell2010

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
  • 8 types
  • 16 values
  • PackageAgda-2.8.0.2
  • Exports24
  • LanguageHaskell2010
  • LicenceMIT
  • SourceLibrary.hs
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 LibName
#

A symbolic library name.

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.

Instances9Eq, Ord, Show, Generic, NFData, Hashable, …
valueparseLibName :: String -> LibName
#

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

parseLibName "foo-1.2.3"    == LibName "foo" [1, 2, 3]
parseLibName "foo-01.002.3" == LibName "foo" [1, 2, 3]

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

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 an .agda-lib file, or be part of the default project.

Constructors

Instances3Generic, NFData, Rep

Exported for testing

1 declaration
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" ] == []