pyrox.dev
1import ./make-test-python.nix ({ pkgs, ... }:
2
3let
4 hello-world = pkgs.writeText "hello-world" ''
5 open import IO
6 open import Level
7
8 main = run {0ℓ} (putStrLn "Hello World!")
9 '';
10in
11{
12 name = "agda";
13 meta = with pkgs.lib.maintainers; {
14 maintainers = [ alexarice turion ];
15 };
16
17 machine = { pkgs, ... }: {
18 environment.systemPackages = [
19 (pkgs.agda.withPackages {
20 pkgs = p: [ p.standard-library ];
21 })
22 ];
23 virtualisation.memorySize = 2000; # Agda uses a lot of memory
24 };
25
26 testScript = ''
27 assert (
28 "${pkgs.agdaPackages.lib.interfaceFile "Everything.agda"}" == "Everything.agdai"
29 ), "wrong interface file for Everything.agda"
30 assert (
31 "${pkgs.agdaPackages.lib.interfaceFile "tmp/Everything.agda.md"}" == "tmp/Everything.agdai"
32 ), "wrong interface file for tmp/Everything.agda.md"
33
34 # Minimal script that typechecks
35 machine.succeed("touch TestEmpty.agda")
36 machine.succeed("agda TestEmpty.agda")
37
38 # Minimal script that actually uses the standard library
39 machine.succeed('echo "import IO" > TestIO.agda')
40 machine.succeed("agda -l standard-library -i . TestIO.agda")
41
42 # Hello world
43 machine.succeed(
44 "cp ${hello-world} HelloWorld.agda"
45 )
46 machine.succeed("agda -l standard-library -i . -c HelloWorld.agda")
47 # Check execution
48 assert "Hello World!" in machine.succeed(
49 "./HelloWorld"
50 ), "HelloWorld does not run properly"
51 '';
52}
53)