diff --git a/nixos/tests/agda/default.nix b/nixos/tests/agda/default.nix index ab473aa9e495..ad0527beac30 100644 --- a/nixos/tests/agda/default.nix +++ b/nixos/tests/agda/default.nix @@ -1,3 +1,5 @@ -{ runTest }: { +{ runTest }: +{ base = runTest ./base.nix; + override-with-backend = runTest ./override-with-backend.nix; } diff --git a/nixos/tests/agda/override-with-backend.nix b/nixos/tests/agda/override-with-backend.nix new file mode 100644 index 000000000000..42845dd02b00 --- /dev/null +++ b/nixos/tests/agda/override-with-backend.nix @@ -0,0 +1,71 @@ +{ pkgs, ... }: +let + mainProgram = "agda-trivial-backend"; + + hello-world = pkgs.writeText "hello-world" '' + {-# OPTIONS --guardedness #-} + open import IO + open import Level + + main = run {0ℓ} (putStrLn "Hello World!") + ''; + agda-trivial-backend = + pkgs.runCommand "trivial-backend" + { + version = "${pkgs.haskellPackages.Agda.version}"; + meta.mainProgram = "${mainProgram}"; + buildInputs = [ (pkgs.haskellPackages.ghcWithPackages (pkgs: [ pkgs.Agda ])) ]; + } + '' + cat << EOF > Main.hs + module Main where + + import Agda.Main ( runAgda ) + + main :: IO () + main = runAgda [] + EOF + + ghc Main.hs -o ${mainProgram} + mkdir -p $out/bin + cp ${mainProgram} $out/bin + ''; +in +{ + name = "agda-trivial-backend"; + meta = { + maintainers = [ + # FIXME + ]; + }; + + nodes.machine = + { pkgs, ... }: + let + agdaPackages = pkgs.agdaPackages.override (oldAttrs: { + Agda = agda-trivial-backend; + }); + in + { + environment.systemPackages = [ + (agdaPackages.agda.withPackages { + pkgs = p: [ p.standard-library ]; + }) + ]; + virtualisation.memorySize = 2000; # Agda uses a lot of memory + }; + + testScript = '' + # agda executable is not present + machine.fail("agda --version") + # Hello world + machine.succeed( + "cp ${hello-world} HelloWorld.agda" + ) + machine.succeed("${mainProgram} -l standard-library -i . -c HelloWorld.agda") + # Check execution + assert "Hello World!" in machine.succeed( + "./HelloWorld" + ), "HelloWorld does not run properly" + ''; +}