blob: ec61af2afe754a92754198928fe75f7100698d1f (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
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"
'';
}
)
|