diff --git a/ci/OWNERS b/ci/OWNERS index b459a496cdf3..e03682addd23 100644 --- a/ci/OWNERS +++ b/ci/OWNERS @@ -343,7 +343,7 @@ pkgs/development/python-modules/buildcatrust/ @ajs124 @lukegb @mweinelt /pkgs/top-level/agda-packages.nix @NixOS/agda /pkgs/development/libraries/agda @NixOS/agda /doc/languages-frameworks/agda.section.md @NixOS/agda -/nixos/tests/agda.nix @NixOS/agda +/nixos/tests/agda @NixOS/agda # Idris /pkgs/development/idris-modules @Infinisil diff --git a/maintainers/maintainer-list.nix b/maintainers/maintainer-list.nix index 963a97193aeb..8d672effcb02 100644 --- a/maintainers/maintainer-list.nix +++ b/maintainers/maintainer-list.nix @@ -4254,6 +4254,11 @@ githubId = 498906; name = "Karolis Stasaitis"; }; + carlostome = { + name = "Carlos Tomé Cortiñas"; + github = "carlostome"; + githubId = 2206578; + }; carlsverre = { email = "accounts@carlsverre.com"; github = "carlsverre"; diff --git a/nixos/tests/agda.nix b/nixos/tests/agda/base.nix similarity index 82% rename from nixos/tests/agda.nix rename to nixos/tests/agda/base.nix index dfc733f4f576..f804abda6f62 100644 --- a/nixos/tests/agda.nix +++ b/nixos/tests/agda/base.nix @@ -1,13 +1,7 @@ { pkgs, ... }: let - hello-world = pkgs.writeText "hello-world" '' - {-# OPTIONS --guardedness #-} - open import IO - open import Level - - main = run {0ℓ} (putStrLn "Hello World!") - ''; + hello-world = ./files/HelloWorld.agda; in { name = "agda"; @@ -30,6 +24,10 @@ in }; testScript = '' + # agda and agda-mode are in path + machine.succeed("agda --version") + machine.succeed("agda-mode") + # Minimal script that typechecks machine.succeed("touch TestEmpty.agda") machine.succeed("agda TestEmpty.agda") diff --git a/nixos/tests/agda/default.nix b/nixos/tests/agda/default.nix new file mode 100644 index 000000000000..ad0527beac30 --- /dev/null +++ b/nixos/tests/agda/default.nix @@ -0,0 +1,5 @@ +{ runTest }: +{ + base = runTest ./base.nix; + override-with-backend = runTest ./override-with-backend.nix; +} diff --git a/nixos/tests/agda/files/HelloWorld.agda b/nixos/tests/agda/files/HelloWorld.agda new file mode 100644 index 000000000000..5cef59109c4b --- /dev/null +++ b/nixos/tests/agda/files/HelloWorld.agda @@ -0,0 +1,5 @@ +{-# OPTIONS --guardedness #-} +open import IO +open import Level + +main = run {0ℓ} (putStrLn "Hello World!") diff --git a/nixos/tests/agda/files/TrivialBackend.hs b/nixos/tests/agda/files/TrivialBackend.hs new file mode 100644 index 000000000000..0a37115eb80f --- /dev/null +++ b/nixos/tests/agda/files/TrivialBackend.hs @@ -0,0 +1,6 @@ +module Main where + +import Agda.Main ( runAgda ) + +main :: IO () +main = runAgda [] diff --git a/nixos/tests/agda/override-with-backend.nix b/nixos/tests/agda/override-with-backend.nix new file mode 100644 index 000000000000..bb64a473ee5d --- /dev/null +++ b/nixos/tests/agda/override-with-backend.nix @@ -0,0 +1,65 @@ +{ pkgs, ... }: +let + mainProgram = "agda-trivial-backend"; + + hello-world = ./files/HelloWorld.agda; + + agda-trivial-backend = pkgs.stdenvNoCC.mkDerivation { + name = "trivial-backend"; + meta = { inherit mainProgram; }; + version = "${pkgs.haskellPackages.Agda.version}"; + src = ./files/TrivialBackend.hs; + buildInputs = [ + (pkgs.haskellPackages.ghcWithPackages (pkgs: [ pkgs.Agda ])) + ]; + dontUnpack = true; + buildPhase = '' + ghc $src -o ${mainProgram} + ''; + installPhase = '' + mkdir -p $out/bin + cp ${mainProgram} $out/bin + ''; + }; +in +{ + name = "agda-trivial-backend"; + meta = with pkgs.lib.maintainers; { + maintainers = [ + carlostome + ]; + }; + + 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 and agda-mode are not in path + machine.fail("agda --version") + machine.fail("agda-mode") + # backend is present + text = machine.succeed("${mainProgram} --help") + assert "${mainProgram}" in text + # Hello world + machine.succeed( + "cp ${hello-world} HelloWorld.agda" + ) + machine.succeed("${mainProgram} -l standard-library -i . -c HelloWorld.agda") + # Check execution + text = machine.succeed("./HelloWorld") + assert "Hello World!" in text, f"HelloWorld does not run properly: output was {text}" + ''; +} diff --git a/nixos/tests/all-tests.nix b/nixos/tests/all-tests.nix index d1eb5b439da0..490ffa11ed24 100644 --- a/nixos/tests/all-tests.nix +++ b/nixos/tests/all-tests.nix @@ -203,7 +203,9 @@ in adguardhome = runTest ./adguardhome.nix; aesmd = runTestOn [ "x86_64-linux" ] ./aesmd.nix; agate = runTest ./web-servers/agate.nix; - agda = runTest ./agda.nix; + agda = import ./agda { + inherit runTest; + }; age-plugin-tpm-decrypt = runTest ./age-plugin-tpm-decrypt.nix; agnos = discoverTests (import ./agnos.nix); agorakit = runTest ./web-apps/agorakit.nix; diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix index b8645053b6e9..72e1d8dbd124 100644 --- a/pkgs/build-support/agda/default.nix +++ b/pkgs/build-support/agda/default.nix @@ -45,7 +45,7 @@ let }: let libraryFile = mkLibraryFile pkgs; - pname = "agdaWithPackages"; + pname = "${Agda.meta.mainProgram}WithPackages"; version = Agda.version; in runCommand "${pname}-${version}" @@ -68,10 +68,12 @@ let } '' mkdir -p $out/bin - makeWrapper ${lib.getExe Agda} $out/bin/agda \ + makeWrapper ${lib.getExe Agda} $out/bin/${Agda.meta.mainProgram} \ ${lib.optionalString (ghc != null) ''--add-flags "--with-compiler=${ghc}/bin/ghc"''} \ --add-flags "--library-file=${libraryFile}" - ln -s ${lib.getExe' Agda "agda-mode"} $out/bin/agda-mode + if [ -e ${lib.getExe' Agda "agda-mode"} ]; then + ln -s ${lib.getExe' Agda "agda-mode"} $out/bin/agda-mode + fi ''; withPackages = arg: if isAttrs arg then withPackages' arg else withPackages' { pkgs = arg; }; @@ -116,7 +118,7 @@ let else '' runHook preBuild - agda --build-library + ${lib.getExe agdaWithPkgs} --build-library runHook postBuild '';