From 0483e40becb6048629b6407d626f3a2b299b2a6f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Fri, 17 Oct 2025 17:12:38 +0200 Subject: [PATCH 01/11] Replace hardcoded agda binary by name from package --- pkgs/build-support/agda/default.nix | 6 +++--- pkgs/top-level/agda-packages.nix | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix index b8645053b6e9..1ae5ed706d48 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,7 +68,7 @@ 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 @@ -116,7 +116,7 @@ let else '' runHook preBuild - agda --build-library + ${lib.getExe agdaWithPkgs} --build-library runHook postBuild ''; diff --git a/pkgs/top-level/agda-packages.nix b/pkgs/top-level/agda-packages.nix index b9fab48170a6..4a000b4866d6 100644 --- a/pkgs/top-level/agda-packages.nix +++ b/pkgs/top-level/agda-packages.nix @@ -27,7 +27,7 @@ let lib = lib.extend (final: prev: import ../build-support/agda/lib.nix { lib = prev; }); - agda = withPackages [ ]; + "${Agda.meta.mainProgram}" = withPackages [ ]; standard-library = callPackage ../development/libraries/agda/standard-library { }; From a8967950c8d9cd63fea779afea73a9015988cca4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Fri, 17 Oct 2025 17:13:12 +0200 Subject: [PATCH 02/11] Remove agda-mode from executables --- pkgs/build-support/agda/default.nix | 1 - 1 file changed, 1 deletion(-) diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix index 1ae5ed706d48..e82f2a2d475c 100644 --- a/pkgs/build-support/agda/default.nix +++ b/pkgs/build-support/agda/default.nix @@ -71,7 +71,6 @@ let 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 ''; withPackages = arg: if isAttrs arg then withPackages' arg else withPackages' { pkgs = arg; }; From cd8deb7309458c6d537ff200dd3d4d21f532a06d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Sat, 18 Oct 2025 09:30:50 +0200 Subject: [PATCH 03/11] Revert change --- pkgs/top-level/agda-packages.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkgs/top-level/agda-packages.nix b/pkgs/top-level/agda-packages.nix index 4a000b4866d6..b9fab48170a6 100644 --- a/pkgs/top-level/agda-packages.nix +++ b/pkgs/top-level/agda-packages.nix @@ -27,7 +27,7 @@ let lib = lib.extend (final: prev: import ../build-support/agda/lib.nix { lib = prev; }); - "${Agda.meta.mainProgram}" = withPackages [ ]; + agda = withPackages [ ]; standard-library = callPackage ../development/libraries/agda/standard-library { }; From ab75be0a25c1f5aad18fd75188113f163b084f9e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Mon, 20 Oct 2025 10:20:52 +0200 Subject: [PATCH 04/11] Refactor tests/agda.nix to support more tests --- ci/OWNERS | 2 +- nixos/tests/{agda.nix => agda/base.nix} | 0 nixos/tests/agda/default.nix | 3 +++ nixos/tests/all-tests.nix | 4 +++- 4 files changed, 7 insertions(+), 2 deletions(-) rename nixos/tests/{agda.nix => agda/base.nix} (100%) create mode 100644 nixos/tests/agda/default.nix 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/nixos/tests/agda.nix b/nixos/tests/agda/base.nix similarity index 100% rename from nixos/tests/agda.nix rename to nixos/tests/agda/base.nix diff --git a/nixos/tests/agda/default.nix b/nixos/tests/agda/default.nix new file mode 100644 index 000000000000..ab473aa9e495 --- /dev/null +++ b/nixos/tests/agda/default.nix @@ -0,0 +1,3 @@ +{ runTest }: { + base = runTest ./base.nix; +} 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; From f933041b6c9edc13d66876beeed1ce4ae01e176f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Mon, 20 Oct 2025 10:46:08 +0200 Subject: [PATCH 05/11] Add test to override Agda package with custom backend --- nixos/tests/agda/default.nix | 4 +- nixos/tests/agda/override-with-backend.nix | 71 ++++++++++++++++++++++ 2 files changed, 74 insertions(+), 1 deletion(-) create mode 100644 nixos/tests/agda/override-with-backend.nix 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" + ''; +} From 4c64e800a39f1aef6128b6b3d255a2d5fdc80735 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Thu, 23 Oct 2025 09:43:22 +0200 Subject: [PATCH 06/11] Update pkgs/build-support/agda/default.nix Co-authored-by: Philip Taron --- pkgs/build-support/agda/default.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix index e82f2a2d475c..b1036c968daf 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 = "${Agda.meta.mainProgram}" + "WithPackages"; + pname = "${Agda.meta.mainProgram}WithPackages"; version = Agda.version; in runCommand "${pname}-${version}" From 5882fce4978881a8cd15aa378b907d9e7e661139 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Thu, 23 Oct 2025 10:48:35 +0200 Subject: [PATCH 07/11] Incorporate suggestions - land `HelloWorld.agda` and `TrivialBackend.hs` in files - replace `runCommand` by `stdenvNoCC.mkDerivation` - refactor asserts --- nixos/tests/agda/files/HelloWorld.agda | 5 ++ nixos/tests/agda/files/TrivialBackend.hs | 6 +++ nixos/tests/agda/override-with-backend.nix | 53 ++++++++++------------ 3 files changed, 34 insertions(+), 30 deletions(-) create mode 100644 nixos/tests/agda/files/HelloWorld.agda create mode 100644 nixos/tests/agda/files/TrivialBackend.hs 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 index 42845dd02b00..2bf9031a59ec 100644 --- a/nixos/tests/agda/override-with-backend.nix +++ b/nixos/tests/agda/override-with-backend.nix @@ -2,34 +2,25 @@ let mainProgram = "agda-trivial-backend"; - hello-world = pkgs.writeText "hello-world" '' - {-# OPTIONS --guardedness #-} - open import IO - open import Level + hello-world = ./files/HelloWorld.agda; - 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 - ''; + 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"; @@ -58,14 +49,16 @@ in testScript = '' # agda executable is not present machine.fail("agda --version") + # 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 - assert "Hello World!" in machine.succeed( - "./HelloWorld" - ), "HelloWorld does not run properly" + text = machine.succeed("./HelloWorld") + assert "Hello World!" in text, f"HelloWorld does not run properly: output was {text}" ''; } From fdf4727164f53e639de590b2d469a35afa2ff03f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Thu, 23 Oct 2025 10:56:34 +0200 Subject: [PATCH 08/11] =?UTF-8?q?maintainers:=20add=20Carlos=20Tom=C3=A9?= =?UTF-8?q?=20Corti=C3=B1as?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- maintainers/maintainer-list.nix | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/maintainers/maintainer-list.nix b/maintainers/maintainer-list.nix index ee193d84d31f..2eb719a887a5 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"; From fc65416f415828eeca02c1a272725937cf97677d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Thu, 23 Oct 2025 10:58:16 +0200 Subject: [PATCH 09/11] Add myself as a maintainer --- nixos/tests/agda/override-with-backend.nix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/nixos/tests/agda/override-with-backend.nix b/nixos/tests/agda/override-with-backend.nix index 2bf9031a59ec..429aafd21ed3 100644 --- a/nixos/tests/agda/override-with-backend.nix +++ b/nixos/tests/agda/override-with-backend.nix @@ -24,9 +24,9 @@ let in { name = "agda-trivial-backend"; - meta = { + meta = with pkgs.lib.maintainers; { maintainers = [ - # FIXME + carlostome ]; }; From 3c390383bcd3802a527a1945908d52f8e0d17dcf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Thu, 23 Oct 2025 11:00:34 +0200 Subject: [PATCH 10/11] Refactor agda/base.nix to use HelloWorld.agda file --- nixos/tests/agda/base.nix | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/nixos/tests/agda/base.nix b/nixos/tests/agda/base.nix index dfc733f4f576..c730a05e3c45 100644 --- a/nixos/tests/agda/base.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"; From 55ac814fa917268b18cb19581d4c75dc4d023a52 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Tue, 28 Oct 2025 18:13:45 +0100 Subject: [PATCH 11/11] Conditionally create symlink to agda-mode if present --- nixos/tests/agda/base.nix | 4 ++++ nixos/tests/agda/override-with-backend.nix | 3 ++- pkgs/build-support/agda/default.nix | 3 +++ 3 files changed, 9 insertions(+), 1 deletion(-) diff --git a/nixos/tests/agda/base.nix b/nixos/tests/agda/base.nix index c730a05e3c45..f804abda6f62 100644 --- a/nixos/tests/agda/base.nix +++ b/nixos/tests/agda/base.nix @@ -24,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/override-with-backend.nix b/nixos/tests/agda/override-with-backend.nix index 429aafd21ed3..bb64a473ee5d 100644 --- a/nixos/tests/agda/override-with-backend.nix +++ b/nixos/tests/agda/override-with-backend.nix @@ -47,8 +47,9 @@ in }; testScript = '' - # agda executable is not present + # 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 diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix index b1036c968daf..72e1d8dbd124 100644 --- a/pkgs/build-support/agda/default.nix +++ b/pkgs/build-support/agda/default.nix @@ -71,6 +71,9 @@ let 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}" + 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; };