diff options
author | Lassulus <github@lassul.us> | 2020-06-16 14:11:01 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-16 14:11:01 +0200 |
commit | 453014b4561dd82d72dddda961ed999905bbde5a (patch) | |
tree | 440f5b6f205e5b014c5919930508e2c0931c31d8 /doc | |
parent | 5e8b626898b70ba9eb9a58262959fdcfa0849bec (diff) | |
parent | e215c3bcac09ea3c1b1c9a5f9acd65b8e1791133 (diff) |
Merge pull request #89245 from alexarice/agda-literate
agda: install literate files
Diffstat (limited to 'doc')
-rw-r--r-- | doc/languages-frameworks/agda.section.md | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/doc/languages-frameworks/agda.section.md b/doc/languages-frameworks/agda.section.md index 8cba6d9faa7d..72b895f5da12 100644 --- a/doc/languages-frameworks/agda.section.md +++ b/doc/languages-frameworks/agda.section.md @@ -67,7 +67,17 @@ A derivation can then be written using `agdaPackages.mkDerivation`. This has sim + `libraryName` should be the name that appears in the `*.agda-lib` file, defaulting to `pname`. + `libraryFile` should be the file name of the `*.agda-lib` file, defaulting to `${libraryName}.agda-lib`. -The build phase for `agdaPackages.mkDerivation` simply runs `agda` on the `Everything.agda` file. If something else is needed to build the package (e.g. `make`) then the `buildPhase` should be overridden (or a `preBuild` or `configurePhase` can be used if there are steps that need to be done prior to checking the `Everything.agda` file). `agda` and the Agda libraries contained in `buildInputs` are made available during the build phase. The install phase simply copies all `.agda`, `.agdai` and `.agda-lib` files to the output directory. Again, this can be overridden. +### Build phase +The default build phase for `agdaPackages.mkDerivation` simply runs `agda` on the `Everything.agda` file. +If something else is needed to build the package (e.g. `make`) then the `buildPhase` should be overridden. +Additionally, a `preBuild` or `configurePhase` can be used if there are steps that need to be done prior to checking the `Everything.agda` file. +`agda` and the Agda libraries contained in `buildInputs` are made available during the build phase. + +### Install phase +The default install phase copies agda source files, agda interface files (`*.agdai`) and `*.agda-lib` files to the output directory. +This can be overridden. + +By default, agda sources are files ending on `.agda`, or literate agda files ending on `.lagda`, `.lagda.tex`, `.lagda.org`, `.lagda.md`, `.lagda.rst`. The list of recognised agda source extensions can be extended by setting the `extraExtensions` config variable. To add an agda package to `nixpkgs`, the derivation should be written to `pkgs/development/libraries/agda/${library-name}/` and an entry should be added to `pkgs/top-level/agda-packages.nix`. Here it is called in a scope with access to all other agda libraries, so the top line of the `default.nix` can look like: ``` |