agda: install literate files

2 files changed, 23 insertions, 2 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:
 ```
diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix
index 205aff555730..3c973e8cc0ac 100644
--- a/pkgs/build-support/agda/default.nix
+++ b/pkgs/build-support/agda/default.nix
@@ -30,6 +30,16 @@ let
 
   withPackages = arg: if builtins.isAttrs arg then withPackages' arg else withPackages' { pkgs = arg; };
 
+  extensions = [
+    "agda"
+    "agda-lib"
+    "agdai"
+    "lagda"
+    "lagda.md"
+    "lagda.org"
+    "lagda.rst"
+    "lagda.tex"
+  ];
 
   defaults =
     { pname
@@ -39,6 +49,7 @@ let
     , libraryFile ? "${libraryName}.agda-lib"
     , buildPhase ? null
     , installPhase ? null
+    , extraExtensions ? []
     , ...
     }: let
       agdaWithArgs = withPackages (builtins.filter (p: p ? isAgdaDerivation) buildInputs);
@@ -59,7 +70,7 @@ let
         installPhase = if installPhase != null then installPhase else ''
           runHook preInstall
           mkdir -p $out
-          find \( -name '*.agda' -or -name '*.agdai' -or -name '*.agda-lib' \) -exec cp -p --parents -t "$out" {} +
+          find \( ${concatMapStringsSep " -or " (p: "-name '*.${p}'") (extensions ++ extraExtensions)} \) -exec cp -p --parents -t "$out" {} +
           runHook postInstall
         '';
       };