colin/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

agda: fix manual build

Browse Source 
/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"
This commit is contained in:
Cole Helbling 2020-06-17 13:50:59 -07:00
parent e215c3bcac
commit 5baa7541d7
No known key found for this signature in database
GPG Key ID: B37E0F2371016A4C
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
doc/languages-frameworks/agda.section.md
View File

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