agda: parameterize agda infrastructure by Agda executable name

[carlostome]

This PR addresses two issues:

• build-support/agda/default.nix has the name of the executable provided by the Agda dependency hardcoded everywhere. This prevents reusing the available infrastructure with other agda executables (e.g., provided by custom agda backends such as agda2hs).

• build-support/agda/default.nix exports agda-mode executable. However, in version 2.8.0 this is deprecated. This PR removes this.

Things done

• Built on platform:
  • x86_64-linux
  • aarch64-linux
  • x86_64-darwin
  • aarch64-darwin
• Tested, as applicable:
  • NixOS tests in nixos/tests.
  • Package tests at passthru.tests.
  • Tests in lib/tests or pkgs/test for functions and "core" functionality.
• Ran nixpkgs-review on this PR. See nixpkgs-review usage.
• Tested basic functionality of all binary files, usually in ./result/bin/.
• Nixpkgs Release Notes
  • Package update: when the change is major or breaking.
• NixOS Release Notes
  • Module addition: when adding a new NixOS module.
  • Module update: when the change is significant.
• Fits CONTRIBUTING.md, pkgs/README.md, maintainers/README.md and other READMEs.

---

Add a 👍 reaction to pull requests you find important.

[turion]

Sounds sensible. Is this used anywhere though? If not, maybe you can add a derivation to the tests that builds something with agda2hs?

[carlostome]

I intend to use it in: https://github.com/IntersectMBO/formal-ledger-specifications, where we use a custom agda backend.

It is also possible to use it with agda2hs (see here)

Sounds sensible. Is this used anywhere though? If not, maybe you can add a derivation to the tests that builds something with agda2hs?

I don't think agda2hs is currently part of nixpkgs so I don't know how feasible is that. It is indeed part of haskellPackages.

[ncfavier]

Is there a reason to remove this now? If not I would prefer to follow upstream's deprecation cycle. The executable currently prints a deprecation message when run.

[carlostome]

The reason is to be compatible with backends that do not have an agda-mode executable.

[ncfavier]

This sounds like the kind of out-of-tree compatibility that would be hard to maintain in nixpkgs since we don't have any non-default backends here.

Adding a test derivation in nixpkgs as suggested by @turion could address this.

[ncfavier]

I'd still prefer to conditionally link agda-mode if it exists.

[carlostome]

If not, maybe you can add a derivation to the tests that builds something with agda2hs?

Where would such derivation go?

[philiptaron]

I've got a bunch of completely non-blocking comments; my overall comment is that this use of meta.mainProgram as the configuration point seems odd and wrong to me.

Isn't the actual contract that whatever replaces agda needs to fulfill what it does, even if it uses a different name?

In other words, if agda2hs is used, the trivial derivation that makes it symlink to the $out/bin/agda name would also work for your purposes, as I understand it.

[philiptaron]

Tangent about nested attrsets in this file

I see this is following the pattern of the rest of the imports in this file; in other files, I would have expected lib.recurseIntoAttrs to make the set of tests here built and eval'd by CI.

I don't really understand @roberth's change #191540 that introduced this stanza which deals with that...

nixpkgs/nixos/tests/all-tests.nix

Lines 113 to 125 in f991670

	findTests =
	tree:
	if tree ? recurseForDerivations && tree.recurseForDerivations then
	mapAttrs (k: findTests) (builtins.removeAttrs tree [ "recurseForDerivations" ])
	else
	callTest tree;
	runTest =
	arg:
	let
	r = doRunTest arg;
	in
	findTests r;

[philiptaron]

Let's print what it did output:

Suggested change

	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}"

[carlostome]

I'm happy to add these suggestions. I was trying to be consistent with what was already in https://github.com/carlostome/nixpkgs/blob/d56290ec3cb5b490e5a6cb351e3e11b8df874789/nixos/tests/agda/base.nix

[philiptaron]

Isn't this:

Suggested change

	meta.mainProgram = "${mainProgram}";
	meta = { inherit mainProgram; };

?

[philiptaron]

Land yourself here?

[philiptaron]

I'd have landed this into the directory rather than using pkgs.writeText.

[philiptaron]

I'd land this into the directory rather than use cat.

[philiptaron]

I'd use stdenvNoCC.mkDerivation here.

[carlostome]

Isn't the actual contract that whatever replaces agda needs to fulfill what it does, even if it uses a different name?

To answer this propertly we would have to define first "what (agda) does". For the change I'm proposing I have two cases in mind where one can be argued to fulfill what agda does and the other clearly does not but still can benefit from the agda nixpkgs infrastructure (mkDerivation, withPackages):

• Case 1: A backend for Agda that is fully compatible with all Agda libraries present in nixpkgs.
• Case 2: A backend like agda2hs that is not compatible with the Agda libraries in nixpkgs.

In other words, if agda2hs is used, the trivial derivation that makes it symlink to the $out/bin/agda name would also work for your purposes, as I understand it.

There is a small subtlety here. Agda backends "know" the name of their executable and use this for example with agda --emacs-mode setup. So for instance if we were to use this to drop in a nix shell and use emacs with agda mode then the executable will not be found in the path.

[philiptaron]

I'm going to let @ncfavier and the Haskell / @NixOS/agda folks review/merge. I don't know enough about this domain to make the proper decision.