Incorporate suggestions

- land `HelloWorld.agda` and `TrivialBackend.hs` in files
- replace `runCommand` by `stdenvNoCC.mkDerivation`
- refactor asserts

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

@@ -2,34 +2,25 @@
 let
   mainProgram = "agda-trivial-backend";
 
-  hello-world = pkgs.writeText "hello-world" ''
+  hello-world = ./files/HelloWorld.agda;
-    {-# OPTIONS --guardedness #-}
-    open import IO
-    open import Level
 
-    main = run {0ℓ} (putStrLn "Hello World!")
+  agda-trivial-backend = pkgs.stdenvNoCC.mkDerivation {
-  '';
+    name = "trivial-backend";
-  agda-trivial-backend =
+    meta = { inherit mainProgram; };
-    pkgs.runCommand "trivial-backend"
+    version = "${pkgs.haskellPackages.Agda.version}";
-      {
+    src = ./files/TrivialBackend.hs;
-        version = "${pkgs.haskellPackages.Agda.version}";
+    buildInputs = [
-        meta.mainProgram = "${mainProgram}";
+      (pkgs.haskellPackages.ghcWithPackages (pkgs: [ pkgs.Agda ]))
-        buildInputs = [ (pkgs.haskellPackages.ghcWithPackages (pkgs: [ pkgs.Agda ])) ];
+    ];
-      }
+    dontUnpack = true;
-      ''
+    buildPhase = ''
-        cat << EOF > Main.hs
+      ghc $src -o ${mainProgram}
-        module Main where
+    '';
-
+    installPhase = ''
-        import Agda.Main ( runAgda )
+      mkdir -p $out/bin
-
+      cp ${mainProgram} $out/bin
-        main :: IO ()
+    '';
-        main = runAgda []
+  };
-        EOF
-
-        ghc Main.hs -o ${mainProgram}
-        mkdir -p $out/bin
-        cp ${mainProgram} $out/bin
-      '';
 in
 {
   name = "agda-trivial-backend";
@@ -58,14 +49,16 @@ in
   testScript = ''
     # agda executable is not present
     machine.fail("agda --version")
+    # 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
-    assert "Hello World!" in machine.succeed(
+    text = machine.succeed("./HelloWorld")
-        "./HelloWorld"
+    assert "Hello World!" in text, f"HelloWorld does not run properly: output was {text}"
-    ), "HelloWorld does not run properly"
   '';
 }