From 5baa7541d73e57f26d1da9ca0c663cc7be31f256 Mon Sep 17 00:00:00 2001 From: Cole Helbling Date: Wed, 17 Jun 2020 13:50:59 -0700 Subject: agda: fix manual build /build/doc/manual-full.xml:12764:35: error: ID "build-phase" has already been defined /build/doc/manual-full.xml:9029:33: error: first occurrence of ID "build-phase" --- doc/languages-frameworks/agda.section.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/languages-frameworks/agda.section.md b/doc/languages-frameworks/agda.section.md index 72b895f5da12..9ce046d05b6f 100644 --- a/doc/languages-frameworks/agda.section.md +++ b/doc/languages-frameworks/agda.section.md @@ -67,13 +67,13 @@ 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`. -### Build phase +### Building Agda packages 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 +### Installing Agda packages The default install phase copies agda source files, agda interface files (`*.agdai`) and `*.agda-lib` files to the output directory. This can be overridden. -- cgit 1.4.1