1 files changed, 16 insertions, 7 deletions
diff --git a/nixos/tests/agda.nix b/nixos/tests/agda.nix
index e158999e57d..ec61af2afe7 100644
--- a/nixos/tests/agda.nix
+++ b/nixos/tests/agda.nix
@@ -2,14 +2,16 @@ import ./make-test-python.nix ({ pkgs, ... }:
 
 let
   hello-world = pkgs.writeText "hello-world" ''
+    {-# OPTIONS --guardedness #-}
     open import IO
+    open import Level
 
-    main = run(putStrLn "Hello World!")
+    main = run {0ℓ} (putStrLn "Hello World!")
   '';
 in
 {
   name = "agda";
-  meta = with pkgs.stdenv.lib.maintainers; {
+  meta = with pkgs.lib.maintainers; {
     maintainers = [ alexarice turion ];
   };
 
@@ -23,19 +25,26 @@ in
   };
 
   testScript = ''
+    assert (
+        "${pkgs.agdaPackages.lib.interfaceFile "Everything.agda"}" == "Everything.agdai"
+    ), "wrong interface file for Everything.agda"
+    assert (
+        "${pkgs.agdaPackages.lib.interfaceFile "tmp/Everything.agda.md"}" == "tmp/Everything.agdai"
+    ), "wrong interface file for tmp/Everything.agda.md"
+
     # 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
+    # Hello world
     machine.succeed(
         "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"
   '';
 }
 )