Agda rework

doc/languages-frameworks/agda.section.md

@@ -0,0 +1,96 @@
+---
+title: Agda
+author: Alex Rice (alexarice)
+date: 2020-01-06
+---
+# Agda
+
+## How to use Agda
+
+Agda can be installed from `agda`:
+```
+$ nix-env -iA agda
+```
+
+To use agda with libraries, the `agda.withPackages` function can be used. This function either takes:
++ A list of packages,
++ or a function which returns a list of packages when given the `agdaPackages` attribute set,
++ or an attribute set containing a list of packages and a GHC derivation for compilation (see below).
+
+For example, suppose we wanted a version of agda which has access to the standard library. This can be obtained with the expressions:
+
+```
+agda.withPackages [ agdaPackages.standard-library ]
+```
+
+or
+
+```
+agda.withPackages (p: [ p.standard-library ])
+```
+
+or can be called as in the [Compiling Agda](#compiling-agda) section.
+
+If you want to use a library in your home directory (for instance if it is a development version) then typecheck it manually (using `agda.withPackages` if necessary) and then override the `src` attribute of the package to point to your local repository.
+
+Agda will not by default use these libraries. To tell agda to use the library we have some options:
+- Call `agda` with the library flag:
+```
+$ agda -l standard-library -i . MyFile.agda
+```
+- Write a `my-library.agda-lib` file for the project you are working on which may look like:
+```
+name: my-library
+include: .
+depends: standard-library
+```
+- Create the file `~/.agda/defaults` and add any libraries you want to use by default.
+
+More information can be found in the [official Agda documentation on library management](https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html).
+
+## Compiling Agda
+Agda modules can be compiled with the `--compile` flag. A version of `ghc` with `ieee` is made available to the Agda program via the `--with-compiler` flag.
+This can be overridden by a different version of `ghc` as follows:
+
+```
+agda.withPackages {
+  pkgs = [ ... ];
+  ghc = haskell.compiler.ghcHEAD;
+}
+```
+
+## Writing Agda packages
+To write a nix derivation for an agda library, first check that the library has a `*.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`.
+
+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.
+
+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:
+```
+{ mkDerivation, standard-library, fetchFromGitHub }:
+```
+and `mkDerivation` should be called instead of `agdaPackages.mkDerivation`. Here is an example skeleton derivation for iowa-stdlib:
+
+```
+mkDerivation {
+  version = "1.5.0";
+  pname = "iowa-stdlib";
+
+  src = ...
+
+  libraryFile = "";
+  libraryName = "IAL-1.3";
+
+  buildPhase = ''
+    patchShebangs find-deps.sh
+    make
+  '';
+}
+```
+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`.
+
+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).

doc/languages-frameworks/index.xml

@@ -5,6 +5,7 @@
  <para>
   The <link linkend="chap-stdenv">standard build environment</link> makes it easy to build typical Autotools-based packages with very little code. Any other kind of package can be accomodated by overriding the appropriate phases of <literal>stdenv</literal>. However, there are specialised functions in Nixpkgs to easily build packages for other programming languages, such as Perl or Haskell. These are described in this chapter.
  </para>
+ <xi:include href="agda.section.xml" />
  <xi:include href="android.section.xml" />
  <xi:include href="beam.xml" />
  <xi:include href="bower.xml" />

nixos/tests/agda.nix

@@ -0,0 +1,41 @@
+import ./make-test-python.nix ({ pkgs, ... }:
+
+let
+  hello-world = pkgs.writeText "hello-world" ''
+    open import IO
+
+    main = run(putStrLn "Hello World!")
+  '';
+in
+{
+  name = "agda";
+  meta = with pkgs.stdenv.lib.maintainers; {
+    maintainers = [ alexarice turion ];
+  };
+
+  machine = { pkgs, ... }: {
+    environment.systemPackages = [
+      (pkgs.agda.withPackages {
+        pkgs = p: [ p.standard-library ];
+      })
+    ];
+    virtualisation.memorySize = 2000; # Agda uses a lot of memory
+  };
+
+  testScript = ''
+    # Minimal script that typechecks
+    machine.succeed("touch TestEmpty.agda")
+    machine.succeed("agda TestEmpty.agda")
+
+    # Minimal script that actually uses the standard library
+    machine.succeed('echo "import IO" > TestIO.agda')
+    machine.succeed("agda -l standard-library -i . TestIO.agda")
+
+    # # Hello world
+    machine.succeed(
+        "cp ${hello-world} HelloWorld.agda"
+    )
+    machine.succeed("agda -l standard-library -i . -c HelloWorld.agda")
+  '';
+}
+)

nixos/tests/all-tests.nix

@@ -23,6 +23,7 @@ in
 {
   _3proxy = handleTest ./3proxy.nix {};
   acme = handleTest ./acme.nix {};
+  agda = handleTest ./agda.nix {};
   atd = handleTest ./atd.nix {};
   automysqlbackup = handleTest ./automysqlbackup.nix {};
   avahi = handleTest ./avahi.nix {};

pkgs/build-support/agda/default.nix

@@ -1,90 +1,71 @@
-# Builder for Agda packages. Mostly inspired by the cabal builder.
+# Builder for Agda packages.
 
-{ stdenv, Agda, glibcLocales
-, writeShellScriptBin
-, extension ? (self: super: {})
-}:
+{ stdenv, lib, self, Agda, runCommandNoCC, makeWrapper, writeText, mkShell, ghcWithPackages }:
 
-with stdenv.lib.strings;
+with lib.strings;
 
 let
-  defaults = self : {
-    # There is no Hackage for Agda so we require src.
-    inherit (self) src name;
-
-    isAgdaPackage = true;
-
-    buildInputs = [ Agda ] ++ self.buildDepends;
-    buildDepends = [];
-
-    buildDependsAgda = stdenv.lib.filter
-      (dep: dep ? isAgdaPackage && dep.isAgdaPackage)
-      self.buildDepends;
-    buildDependsAgdaShareAgda = map (x: x + "/share/agda") self.buildDependsAgda;
-
-    # Not much choice here ;)
-    LANG = "en_US.UTF-8";
-    LOCALE_ARCHIVE = stdenv.lib.optionalString
-      stdenv.isLinux
-      "${glibcLocales}/lib/locale/locale-archive";
-
-    everythingFile = "Everything.agda";
-
-    propagatedBuildInputs = self.buildDependsAgda;
-    propagatedUserEnvPkgs = self.buildDependsAgda;
-
-    # Immediate source directories under which modules can be found.
-    sourceDirectories = [ ];
-
-    # This is used if we have a top-level element that only serves
-    # as the container for the source and we only care about its
-    # contents. The directories put here will have their
-    # *contents* copied over as opposed to sourceDirectories which
-    # would make a direct copy of the whole thing.
-    topSourceDirectories = [ "src" ];
-
-    # FIXME: `dirOf self.everythingFile` is what we really want, not hardcoded "./"
-    includeDirs = self.buildDependsAgdaShareAgda
-                  ++ self.sourceDirectories ++ self.topSourceDirectories
-                  ++ [ "." ];
-    buildFlags = stdenv.lib.concatMap (x: ["-i" x]) self.includeDirs;
-
-    agdaWithArgs = "${Agda}/bin/agda ${toString self.buildFlags}";
-
-    buildPhase = ''
-      runHook preBuild
-      ${self.agdaWithArgs} ${self.everythingFile}
-      runHook postBuild
+  withPackages' = {
+    pkgs,
+    ghc ? ghcWithPackages (p: with p; [ ieee ])
+  }: let
+    pkgs' = if builtins.isList pkgs then pkgs else pkgs self;
+    library-file = writeText "libraries" ''
+      ${(concatMapStringsSep "\n" (p: "${p}/${p.libraryFile}") pkgs')}
     '';
-
-    installPhase = let
-      srcFiles = self.sourceDirectories
-                 ++ map (x: x + "/*") self.topSourceDirectories;
-    in ''
-      runHook preInstall
-      mkdir -p $out/share/agda
-      cp -pR ${concatStringsSep " " srcFiles} $out/share/agda
-      runHook postInstall
-    '';
-
-    passthru = {
-      env = stdenv.mkDerivation {
-        name = "interactive-${self.name}";
-        inherit (self) LANG LOCALE_ARCHIVE;
-        AGDA_PACKAGE_PATH = concatMapStrings (x: x + ":") self.buildDependsAgdaShareAgda;
-        buildInputs = let
-          # Makes a wrapper available to the user. Very useful in
-          # nix-shell where all dependencies are -i'd.
-          agdaWrapper = writeShellScriptBin "agda" ''
-            exec ${self.agdaWithArgs} "$@"
-          '';
-        in [agdaWrapper] ++ self.buildDepends;
+    pname = "agdaWithPackages";
+    version = Agda.version;
+  in runCommandNoCC "${pname}-${version}" {
+    inherit pname version;
+    nativeBuildInputs = [ makeWrapper ];
+    passthru.unwrapped = Agda;
+  } ''
+    mkdir -p $out/bin
+    makeWrapper ${Agda}/bin/agda $out/bin/agda \
+      --add-flags "--with-compiler=${ghc}/bin/ghc" \
+      --add-flags "--library-file=${library-file}" \
+      --add-flags "--local-interfaces"
+    makeWrapper ${Agda}/bin/agda-mode $out/bin/agda-mode
+    ''; # Local interfaces has been added for now: See https://github.com/agda/agda/issues/4526
+
+  withPackages = arg: if builtins.isAttrs arg then withPackages' arg else withPackages' { pkgs = arg; };
+
+
+  defaults =
+    { pname
+    , buildInputs ? []
+    , everythingFile ? "./Everything.agda"
+    , libraryName ? pname
+    , libraryFile ? "${libraryName}.agda-lib"
+    , buildPhase ? null
+    , installPhase ? null
+    , ...
+    }: let
+      agdaWithArgs = withPackages (builtins.filter (p: p ? isAgdaDerivation) buildInputs);
+    in
+      {
+        inherit libraryName libraryFile;
+
+        isAgdaDerivation = true;
+
+        buildInputs = buildInputs ++ [ agdaWithArgs ];
+
+        buildPhase = if buildPhase != null then buildPhase else ''
+          runHook preBuild
+          agda -i ${dirOf everythingFile} ${everythingFile}
+          runHook postBuild
+        '';
+
+        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" {} +
+          runHook postInstall
+        '';
       };
-    };
-  };
 in
-{ mkDerivation = args: let
-      super = defaults self // args self;
-      self  = super // extension self super;
-    in stdenv.mkDerivation self;
+{
+  mkDerivation = args: stdenv.mkDerivation (args // defaults args);
+
+  inherit withPackages withPackages';
 }