nixpkgs/nixos/tests/agda.nix
Manuel Bärenz 65fcd698bb nixosTests.agda: Adapt to --guardedness requirements
The one-line test is hard to fix in a readable manner
and doesn't really add value above the hello-world test.
So rather simplify to reduce maintenance.
2021-07-15 10:25:44 +02:00

50 lines
1.3 KiB
Nix
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import ./make-test-python.nix ({ pkgs, ... }:
let
hello-world = pkgs.writeText "hello-world" ''
{-# OPTIONS --guardedness #-}
open import IO
open import Level
main = run {0} (putStrLn "Hello World!")
'';
in
{
name = "agda";
meta = with pkgs.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 = ''
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")
# 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"
'';
}
)