agda: parameterize agda infrastructure by Agda executable name (NixOS#452961)

Author: ncfavier

ci/OWNERS

@@ -343,7 +343,7 @@ pkgs/development/python-modules/buildcatrust/ @ajs124 @lukegb @mweinelt
 /pkgs/top-level/agda-packages.nix         @NixOS/agda
 /pkgs/development/libraries/agda          @NixOS/agda
 /doc/languages-frameworks/agda.section.md @NixOS/agda
-/nixos/tests/agda.nix                     @NixOS/agda
+/nixos/tests/agda                         @NixOS/agda
 
 # Idris
 /pkgs/development/idris-modules @Infinisil

maintainers/maintainer-list.nix

@@ -4254,6 +4254,11 @@
     githubId = 498906;
     name = "Karolis Stasaitis";
   };
+  carlostome = {
+    name = "Carlos Tomé Cortiñas";
+    github = "carlostome";
+    githubId = 2206578;
+  };
   carlsverre = {
     email = "accounts@carlsverre.com";
     github = "carlsverre";

nixos/tests/agda.nix nixos/tests/agda/base.nixnixos/tests/agda.nix renamed to nixos/tests/agda/base.nix

@@ -1,13 +1,7 @@
 { pkgs, ... }:
 
 let
-  hello-world = pkgs.writeText "hello-world" ''
-    {-# OPTIONS --guardedness #-}
-    open import IO
-    open import Level
-
-    main = run {0ℓ} (putStrLn "Hello World!")
-  '';
+  hello-world = ./files/HelloWorld.agda;
 in
 {
   name = "agda";
@@ -30,6 +24,10 @@ in
     };
 
   testScript = ''
+    # agda and agda-mode are in path
+    machine.succeed("agda --version")
+    machine.succeed("agda-mode")
+
     # Minimal script that typechecks
     machine.succeed("touch TestEmpty.agda")
     machine.succeed("agda TestEmpty.agda")

nixos/tests/agda/default.nix

@@ -0,0 +1,5 @@
+{ runTest }:
+{
+  base = runTest ./base.nix;
+  override-with-backend = runTest ./override-with-backend.nix;
+}

nixos/tests/agda/files/HelloWorld.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --guardedness #-}
+open import IO
+open import Level
+
+main = run {0ℓ} (putStrLn "Hello World!")

nixos/tests/agda/files/TrivialBackend.hs

@@ -0,0 +1,6 @@
+module Main where
+
+import Agda.Main ( runAgda )
+
+main :: IO ()
+main = runAgda []

nixos/tests/agda/override-with-backend.nix

@@ -0,0 +1,65 @@
+{ pkgs, ... }:
+let
+  mainProgram = "agda-trivial-backend";
+
+  hello-world = ./files/HelloWorld.agda;
+
+  agda-trivial-backend = pkgs.stdenvNoCC.mkDerivation {
+    name = "trivial-backend";
+    meta = { inherit mainProgram; };
+    version = "${pkgs.haskellPackages.Agda.version}";
+    src = ./files/TrivialBackend.hs;
+    buildInputs = [
+      (pkgs.haskellPackages.ghcWithPackages (pkgs: [ pkgs.Agda ]))
+    ];
+    dontUnpack = true;
+    buildPhase = ''
+      ghc $src -o ${mainProgram}
+    '';
+    installPhase = ''
+      mkdir -p $out/bin
+      cp ${mainProgram} $out/bin
+    '';
+  };
+in
+{
+  name = "agda-trivial-backend";
+  meta = with pkgs.lib.maintainers; {
+    maintainers = [
+      carlostome
+    ];
+  };
+
+  nodes.machine =
+    { pkgs, ... }:
+    let
+      agdaPackages = pkgs.agdaPackages.override (oldAttrs: {
+        Agda = agda-trivial-backend;
+      });
+    in
+    {
+      environment.systemPackages = [
+        (agdaPackages.agda.withPackages {
+          pkgs = p: [ p.standard-library ];
+        })
+      ];
+      virtualisation.memorySize = 2000; # Agda uses a lot of memory
+    };
+
+  testScript = ''
+    # agda and agda-mode are not in path
+    machine.fail("agda --version")
+    machine.fail("agda-mode")
+    # backend is present
+    text = machine.succeed("${mainProgram} --help")
+    assert "${mainProgram}" in text
+    # Hello world
+    machine.succeed(
+        "cp ${hello-world} HelloWorld.agda"
+    )
+    machine.succeed("${mainProgram} -l standard-library -i . -c HelloWorld.agda")
+    # Check execution
+    text = machine.succeed("./HelloWorld")
+    assert "Hello World!" in text, f"HelloWorld does not run properly: output was {text}"
+  '';
+}

nixos/tests/all-tests.nix

@@ -203,7 +203,9 @@ in
   adguardhome = runTest ./adguardhome.nix;
   aesmd = runTestOn [ "x86_64-linux" ] ./aesmd.nix;
   agate = runTest ./web-servers/agate.nix;
-  agda = runTest ./agda.nix;
+  agda = import ./agda {
+    inherit runTest;
+  };
   age-plugin-tpm-decrypt = runTest ./age-plugin-tpm-decrypt.nix;
   agnos = discoverTests (import ./agnos.nix);
   agorakit = runTest ./web-apps/agorakit.nix;

pkgs/build-support/agda/default.nix

@@ -45,7 +45,7 @@ let
     }:
     let
       libraryFile = mkLibraryFile pkgs;
-      pname = "agdaWithPackages";
+      pname = "${Agda.meta.mainProgram}WithPackages";
       version = Agda.version;
     in
     runCommand "${pname}-${version}"
@@ -68,10 +68,12 @@ let
       }
       ''
         mkdir -p $out/bin
-        makeWrapper ${lib.getExe Agda} $out/bin/agda \
+        makeWrapper ${lib.getExe Agda} $out/bin/${Agda.meta.mainProgram} \
           ${lib.optionalString (ghc != null) ''--add-flags "--with-compiler=${ghc}/bin/ghc"''} \
           --add-flags "--library-file=${libraryFile}"
-        ln -s ${lib.getExe' Agda "agda-mode"} $out/bin/agda-mode
+        if [ -e ${lib.getExe' Agda "agda-mode"} ]; then
+          ln -s ${lib.getExe' Agda "agda-mode"} $out/bin/agda-mode
+        fi
       '';
 
   withPackages = arg: if isAttrs arg then withPackages' arg else withPackages' { pkgs = arg; };
@@ -116,7 +118,7 @@ let
         else
           ''
             runHook preBuild
-            agda --build-library
+            ${lib.getExe agdaWithPkgs} --build-library
             runHook postBuild
           '';