agdaPackages: switch to --build-library

Use the new `--build-library` mode introduced in Agda 2.8.0 to build
libraries instead of relying on ad-hoc `Everything` files. This
simplifies most derivations (except cubical-mini which imports generated
`Everything` files from various modules).

Author: ncfavier

doc/languages-frameworks/agda.section.md

@@ -125,11 +125,10 @@ To install Agda without GHC, use `ghc = null;`.
 
 ## Writing Agda packages {#writing-agda-packages}
 
-To write a nix derivation for an Agda library, first check that the library has a `*.agda-lib` file.
+To write a nix derivation for an Agda library, first check that the library has a (single) `*.agda-lib` file.
 
 A derivation can then be written using `agdaPackages.mkDerivation`. This has similar arguments to `stdenv.mkDerivation` with the following additions:
 
-* `everythingFile` can be used to specify the location of the `Everything.agda` file, defaulting to `./Everything.agda`. If this file does not exist then either it should be patched in or the `buildPhase` should be overridden (see below).
 * `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`.
 
@@ -152,9 +151,9 @@ agdaPackages.mkDerivation {
 
 ### Building Agda packages {#building-agda-packages}
 
-The default build phase for `agdaPackages.mkDerivation` runs `agda` on the `Everything.agda` file.
+The default build phase for `agdaPackages.mkDerivation` runs `agda --build-library`.
 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.
+Additionally, a `preBuild` or `configurePhase` can be used if there are steps that need to be done prior to checking the library.
 `agda` and the Agda libraries contained in `buildInputs` are made available during the build phase.
 
 ### Installing Agda packages {#installing-agda-packages}
@@ -182,53 +181,37 @@ the Agda package set is small and can (still) be maintained by hand.
 
 ### Adding Agda packages to Nixpkgs {#adding-agda-packages-to-nixpkgs}
 
-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:
+To add an Agda package to `nixpkgs`, the derivation should be written to `pkgs/development/libraries/agda/${library-name}/default.nix` 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 derivation could look like:
 
 ```nix
 {
   mkDerivation,
   standard-library,
   fetchFromGitHub,
 }:
-{ }
-```
-
-Note that the derivation function is called with `mkDerivation` set to `agdaPackages.mkDerivation`, therefore you
-could use a similar set as in your `default.nix` from [Writing Agda Packages](#writing-agda-packages) with
-`agdaPackages.mkDerivation` replaced with `mkDerivation`.
 
-Here is an example skeleton derivation for iowa-stdlib:
-
-```nix
 mkDerivation {
-  version = "1.5.0";
-  pname = "iowa-stdlib";
-
+  pname = "my-library";
+  version = "1.0";
   src = <...>;
-
-  libraryFile = "";
-  libraryName = "IAL-1.3";
-
-  buildPhase = ''
-    runHook preBuild
-
-    patchShebangs find-deps.sh
-    make
-
-    runHook postBuild
-  '';
+  buildInputs = [ standard-library ];
+  meta = <...>;
 }
 ```
 
-This library has a file called `.agda-lib`, and so we give an empty string to `libraryFile` as nothing precedes `.agda-lib` in the filename. This file contains `name: IAL-1.3`, and so we let `libraryName =  "IAL-1.3"`. This library does not use an `Everything.agda` file and instead has a Makefile, so there is no need to set `everythingFile` and we set a custom `buildPhase`.
+You can look at other files under `pkgs/development/libraries/agda/` for more inspiration.
+
+Note that the derivation function is called with `mkDerivation` set to `agdaPackages.mkDerivation`, therefore you
+could use a similar set as in your `default.nix` from [Writing Agda Packages](#writing-agda-packages) with
+`agdaPackages.mkDerivation` replaced with `mkDerivation`.
 
 When writing an Agda package it is essential to make sure that no `.agda-lib` file gets added to the store as a single file (for example by using `writeText`). This causes Agda to think that the nix store is a Agda library and it will attempt to write to it whenever it typechecks something. See [https://github.com/agda/agda/issues/4613](https://github.com/agda/agda/issues/4613).
 
 In the pull request adding this library,
 you can test whether it builds correctly by writing in a comment:
 
 ```
-@ofborg build agdaPackages.iowa-stdlib
+@ofborg build agdaPackages.my-library
 ```
 
 ### Maintaining Agda packages {#agda-maintaining-packages}

pkgs/build-support/agda/default.nix

@@ -90,8 +90,6 @@ let
       pname,
       meta,
       buildInputs ? [ ],
-      everythingFile ? "./Everything.agda",
-      includePaths ? [ ],
       libraryName ? pname,
       libraryFile ? "${libraryName}.agda-lib",
       buildPhase ? null,
@@ -100,26 +98,22 @@ let
       ...
     }:
     let
-      agdaWithArgs = withPackages (filter (p: p ? isAgdaDerivation) buildInputs);
-      includePathArgs = concatMapStrings (path: "-i" + path + " ") (
-        includePaths ++ [ (dirOf everythingFile) ]
-      );
+      agdaWithPkgs = withPackages (filter (p: p ? isAgdaDerivation) buildInputs);
     in
     {
       inherit libraryName libraryFile;
 
       isAgdaDerivation = true;
 
-      buildInputs = buildInputs ++ [ agdaWithArgs ];
+      buildInputs = buildInputs ++ [ agdaWithPkgs ];
 
       buildPhase =
         if buildPhase != null then
           buildPhase
         else
           ''
             runHook preBuild
-            agda ${includePathArgs} ${everythingFile}
-            rm ${everythingFile} ${lib.interfaceFile Agda.version everythingFile}
+            agda --build-library
             runHook postBuild
           '';
 

pkgs/build-support/agda/lib.nix

@@ -6,8 +6,8 @@
     * The resulting path may not be normalized.
     *
     * Examples:
-    * interfaceFile pkgs.agda.version "./Everything.agda" == "_build/2.6.4.3/agda/./Everything.agdai"
-    * interfaceFile pkgs.agda.version "src/Everything.lagda.tex" == "_build/2.6.4.3/agda/src/Everything.agdai"
+    * interfaceFile pkgs.agda.version "./Foo.agda" == "_build/AGDA_VERSION/agda/./Foo.agdai"
+    * interfaceFile pkgs.agda.version "src/Foo.lagda.tex" == "_build/AGDA_VERSION/agda/src/Foo.agdai"
   */
   interfaceFile =
     agdaVersion: agdaFile:

pkgs/development/libraries/agda/1lab/default.nix

@@ -23,19 +23,8 @@ mkDerivation rec {
     shopt -s globstar extglob
     files=(src/**/*.@(agda|lagda.md))
     sed -Ei '/OPTIONS/s/ -v ?[^ #]+//g' "''${files[@]}"
-
-    # Generate all-pages manually instead of building the build script.
-    mkdir -p _build
-    for f in "''${files[@]}"; do
-      f=''${f#src/} f=''${f%%.*} f=''${f//\//.}
-      echo "open import $f"
-    done > _build/all-pages.agda
   '';
 
-  libraryName = "1lab";
-  libraryFile = "1lab.agda-lib";
-  everythingFile = "_build/all-pages.agda";
-
   meta = with lib; {
     description = "A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory ";
     homepage = src.meta.homepage;

pkgs/development/libraries/agda/agda-categories/default.nix

@@ -24,11 +24,6 @@ mkDerivation rec {
     # version update of the stdlib, so we get rid of the version constraint
     # altogether.
     sed -Ei 's/standard-library-[0-9.]+/standard-library/' agda-categories.agda-lib
-
-    # The Makefile of agda-categories uses git(1) instead of find(1) to
-    # determine the list of source files. We cannot use git, as $PWD will not
-    # be a valid Git working directory.
-    find src -name '*.agda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda
   '';
 
   buildInputs = [ standard-library ];

pkgs/development/libraries/agda/agda-prelude/default.nix

@@ -15,13 +15,6 @@ mkDerivation {
     hash = "sha256-ab+KojzRbkUTAFNH5OA78s0F5SUuXTbliai6badveg4=";
   };
 
-  preConfigure = ''
-    cd test
-    make everything
-    mv Everything.agda ..
-    cd ..
-  '';
-
   meta = with lib; {
     homepage = "https://github.com/UlfNorell/agda-prelude";
     description = "Programming library for Agda";

pkgs/development/libraries/agda/agdarsec/default.nix

@@ -16,13 +16,6 @@ mkDerivation rec {
     sha256 = "02fqkycvicw6m2xsz8p01aq8n3gj2d2gyx8sgj15l46f8434fy0x";
   };
 
-  everythingFile = "./index.agda";
-
-  includePaths = [
-    "src"
-    "examples"
-  ];
-
   buildInputs = [ standard-library ];
 
   meta = with lib; {

pkgs/development/libraries/agda/cubical/default.nix

@@ -2,7 +2,6 @@
   lib,
   mkDerivation,
   fetchFromGitHub,
-  ghc,
 }:
 
 mkDerivation rec {
@@ -16,13 +15,10 @@ mkDerivation rec {
     hash = "sha256-KwwN2g2naEo4/rKTz2L/0Guh5LxymEYP53XQzJ6eMjM=";
   };
 
-  # The cubical library has several `Everything.agda` files, which are
-  # compiled through the make file they provide.
-  nativeBuildInputs = [ ghc ];
-  buildPhase = ''
-    runHook preBuild
-    make
-    runHook postBuild
+  postPatch = ''
+    # This imports the Everything files, which we don't generate.
+    # TODO: remove for the next release
+    rm -rf Cubical/README.agda Cubical/Talks/EPA2020.agda
   '';
 
   meta = with lib; {

pkgs/development/libraries/agda/functional-linear-algebra/default.nix

@@ -18,10 +18,6 @@ mkDerivation rec {
     sha256 = "sha256-3nme/eH4pY6bD0DkhL4Dj/Vp/WnZqkQtZTNk+n1oAyY=";
   };
 
-  preConfigure = ''
-    sh generate-everything.sh
-  '';
-
   meta = with lib; {
     homepage = "https://github.com/ryanorendorff/functional-linear-algebra";
     description = ''

pkgs/development/libraries/agda/generics/default.nix

@@ -25,8 +25,6 @@ mkDerivation rec {
     rm tests.agda-lib
   '';
 
-  # everythingFile = "./README.agda";
-
   meta = with lib; {
     description = "Library for datatype-generic programming in Agda";
     homepage = src.meta.homepage;