nixos/tests/agda.nix

   1 import ./make-test-python.nix ({ pkgs, ... }:
   2
   3 let
   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   '';
  11 in
  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 )