pyrox.dev
1{ 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 = [
16 alexarice
17 turion
18 ];
19 };
20
21 nodes.machine =
22 { pkgs, ... }:
23 {
24 environment.systemPackages = [
25 (pkgs.agda.withPackages {
26 pkgs = p: [ p.standard-library ];
27 })
28 ];
29 virtualisation.memorySize = 2000; # Agda uses a lot of memory
30 };
31
32 testScript = ''
33 # Minimal script that typechecks
34 machine.succeed("touch TestEmpty.agda")
35 machine.succeed("agda TestEmpty.agda")
36
37 # Hello world
38 machine.succeed(
39 "cp ${hello-world} HelloWorld.agda"
40 )
41 machine.succeed("agda -l standard-library -i . -c HelloWorld.agda")
42 # Check execution
43 assert "Hello World!" in machine.succeed(
44 "./HelloWorld"
45 ), "HelloWorld does not run properly"
46 '';
47}