From b4b4e369212c9f0f5792455a81424a27210a9c61 Mon Sep 17 00:00:00 2001
From: Alexander Ben Nasrallah <me@abn.sh>
Date: Thu, 7 Jan 2021 15:55:52 +0100
Subject: [PATCH 1/2] agda.withPackages: use GHC with ieee754 as default

As mentioned in the package description of ieee on Hackage,
ieee is deprecated in favor of ieee754.
---
 doc/languages-frameworks/agda.section.md | 2 +-
 pkgs/build-support/agda/default.nix      | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/languages-frameworks/agda.section.md b/doc/languages-frameworks/agda.section.md
index 66b4a2083021..f57b194a7266 100644
--- a/doc/languages-frameworks/agda.section.md
+++ b/doc/languages-frameworks/agda.section.md
@@ -46,7 +46,7 @@ depend: standard-library
 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.
+Agda modules can be compiled with the `--compile` flag. A version of `ghc` with `ieee754` is made available to the Agda program via the `--with-compiler` flag.
 This can be overridden by a different version of `ghc` as follows:
 
 ```
diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix
index 3c973e8cc0ac..046bdd061f8c 100644
--- a/pkgs/build-support/agda/default.nix
+++ b/pkgs/build-support/agda/default.nix
@@ -7,7 +7,7 @@ with lib.strings;
 let
   withPackages' = {
     pkgs,
-    ghc ? ghcWithPackages (p: with p; [ ieee ])
+    ghc ? ghcWithPackages (p: with p; [ ieee754 ])
   }: let
     pkgs' = if builtins.isList pkgs then pkgs else pkgs self;
     library-file = writeText "libraries" ''

From 67e43b7453ec197e5045f64dc630b57a3160038f Mon Sep 17 00:00:00 2001
From: Alexander Ben Nasrallah <me@abn.sh>
Date: Fri, 22 Jan 2021 17:25:29 +0100
Subject: [PATCH 2/2] nixos/tests/agda: check execution of HelloWorld

Test that the compiled executable actually runs.
---
 nixos/tests/agda.nix | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/nixos/tests/agda.nix b/nixos/tests/agda.nix
index bbdeb7395aa7..ccc6a9bbfd1e 100644
--- a/nixos/tests/agda.nix
+++ b/nixos/tests/agda.nix
@@ -36,6 +36,10 @@ in
         "cp ${hello-world} HelloWorld.agda"
     )
     machine.succeed("agda -l standard-library -i . -c HelloWorld.agda")
+    # Check execution
+    assert "Hello World!" in machine.succeed(
+        "./HelloWorld"
+    ), "HelloWorld does not run properly"
   '';
 }
 )