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 # Minimal script that typechecks
29 machine.succeed("touch TestEmpty.agda")
30 machine.succeed("agda TestEmpty.agda")
31
32 # Hello world
33 machine.succeed(
34 "cp ${hello-world} HelloWorld.agda"
35 )
36 machine.succeed("agda -l standard-library -i . -c HelloWorld.agda")
37 # Check execution
38 assert "Hello World!" in machine.succeed(
39 "./HelloWorld"
40 ), "HelloWorld does not run properly"
41 '';
42}
43)