import ./make-test-python.nix ({ pkgs, ... }:

let
  hello-world = pkgs.writeText "hello-world" ''
    open import IO
    open import Level

    main = run {0ℓ} (putStrLn "Hello World!")
  '';
in
{
  name = "agda";
  meta = with pkgs.lib.maintainers; {
    maintainers = [ alexarice turion ];
  };

  machine = { pkgs, ... }: {
    environment.systemPackages = [
      (pkgs.agda.withPackages {
        pkgs = p: [ p.standard-library ];
      })
    ];
    virtualisation.memorySize = 2000; # Agda uses a lot of memory
  };

  testScript = ''
    assert (
        "${pkgs.agdaPackages.lib.interfaceFile "Everything.agda"}" == "Everything.agdai"
    ), "wrong interface file for Everything.agda"
    assert (
        "${pkgs.agdaPackages.lib.interfaceFile "tmp/Everything.agda.md"}" == "tmp/Everything.agdai"
    ), "wrong interface file for tmp/Everything.agda.md"

    # Minimal script that typechecks
    machine.succeed("touch TestEmpty.agda")
    machine.succeed("agda TestEmpty.agda")

    # Minimal script that actually uses the standard library
    machine.succeed('echo "import IO" > TestIO.agda')
    machine.succeed("agda -l standard-library -i . TestIO.agda")

    # Hello world
    machine.succeed(
        "cp ${hello-world} HelloWorld.agda"
    )
    machine.succeed("agda -l standard-library -i . -c HelloWorld.agda")
    # Check execution
    assert "Hello World!" in machine.succeed(
        "./HelloWorld"
    ), "HelloWorld does not run properly"
  '';
}
)