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