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
  

Documentation

getDefaultLibraries

Arguments

:: FilePath

Project root.

-> Bool

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

-> 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).

getInstalledLibraries

Arguments

:: Maybe FilePath

Override the default libraries file?

-> 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.

libraryIncludePaths

Arguments

:: Maybe FilePath

libraries file (error reporting only).

-> [AgdaLibFile]

Libraries Agda knows about.

-> [LibName]

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

-> LibM [FilePath]

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

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

type LibName = String

A symbolic library name.

type LibM = ExceptT Doc IO

Throws Doc exceptions.

Exported for testing

data 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

Fields

• 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.

Instances

Eq VersionView

Defined in Agda.Interaction.Library

Methods

(==) :: VersionView -> VersionView -> Bool

(/=) :: VersionView -> VersionView -> Bool

Show VersionView

Defined in Agda.Interaction.Library

Methods

showsPrec :: Int -> VersionView -> ShowS

show :: VersionView -> String

showList :: [VersionView] -> ShowS

versionView :: 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.)

unVersionView :: VersionView -> LibName

Print a VersionView, inverse of versionView (modulo leading zeros).

findLib' :: (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" ] == []