[ refactor ] Add a nix overlay

[mitchmindtree]

This PR adds a Nix overlay and exposes it from the flake. For context, overlays provide a convenient way to merge a set of packages into a larger nixpkgs set.

The overlay attempts to follow the precedent set by the existing idris2 setup in nixpkgs - it exposes the idris2 packages via idris2Packages, then re-exports idris2 at the top-level. Specifically:

• pkgs.idris2Packages.buildIdris
• pkgs.idris2Packages.idris2
• pkgs.idris2Packages.idris2Api
• pkgs.idris2Packages.support
• pkgs.idris2

To avoid duplication, the package derivation calls have been moved to the overlay and the package outputs changed to make use of the merged pkgs set by using the overlay via self. The idris2Api derivation has been moved into its own file as a part of the refactor.

[mattpolzin]

Does offering an overlay need to change so much of the existing flake code? It seems to me like the least disruptive change would be to simply pass the already established idris2, idris2Api, etc. to the overlay nix file. In other words, is it really best to make the overlay the center of everything?

[mitchmindtree]

The main reason I opted to move those package derivation calls into the overlay is that it tends to be much easier to expose an overlay to the rest of the flake outputs, rather than vice versa.

E.g. the overlay can be conveniently merged with the nixpkgs set, and the package outputs exposed with pkgs.<pkg>.

On the other hand, providing flake outputs to an overlay is trickier to do in a manner that does not make it more difficult for non-flake overlay users.

It seems to me like the least disruptive change would be to simply pass the already established idris2, idris2Api, etc

I'd be curious to see your take on this and would be happy to see a PR against this one with the approach you'd take!

It seems a shame to not take advantage of the benefits of the overlay, but perhaps I'm missing some easier way to make the package outputs accessible to the flake in a non-flake-user friendly manner.

In other words, is it really best to make the overlay the center of everything?

Fwiw, in this case the overlay is just calling the packages as we were previously in flake.nix, the main derivations are still in ./nix/*.nix.

[mattpolzin]

On the other hand, providing flake outputs to an overlay is trickier to do in a manner that does not make it more difficult for non-flake overlay users.

It's possible I am missing something here so let me know if my suggestion below misses the point.

I'd be curious to see your take on this [...]

If you move the existing packages up into the let block then the overlay can be defined with 7 lines of change.

diff --git a/flake.nix b/flake.nix
index 3d3e26eef3..95e357494c 100644
--- a/flake.nix
+++ b/flake.nix
@@ -62,12 +62,6 @@
             '';
           };
           stdenv' = with pkgs; if stdenv.isDarwin then overrideSDK stdenv "11.0" else stdenv;
-        in {
-          checks = import ./nix/test.nix {
-            inherit (pkgs) system stdenv runCommand lib;
-            inherit nixpkgs flake-utils;
-            idris = self;
-          };
           packages = rec {
             support = idris2Support;
             idris2 = idris2Pkg;
@@ -76,10 +70,23 @@
           } // (import ./nix/text-editor.nix {
             inherit pkgs idris-emacs-src idris2Pkg;
           });
-          inherit buildIdris;
+        in {
+          inherit packages buildIdris;
+          checks = import ./nix/test.nix {
+            inherit (pkgs) system stdenv runCommand lib;
+            inherit nixpkgs flake-utils;
+            idris = self;
+          };
           devShells.default = pkgs.mkShell.override { stdenv = stdenv'; } {
             packages = idris2Pkg.buildInputs;
           };
+          overlays.default = final: prev: {
+            idris2 = final.idris2Packages.idris2;
+            idris2Packages = prev.idris2Packages // {
+              inherit (packages) support idris2 idris2Api;
+              inherit buildIdris;
+            };
+          };
         };
     in lib.mkOvrOptsFlake
     (opts: flake-utils.lib.eachDefaultSystem (per-system opts) // sys-agnostic);

It seems a shame to not take advantage of the benefits of the overlay [...]

I don't see it as advantageous to use the overlay to build the flake. I find it makes more sense to me to build the flake as its own thing -- it may have some things in common with nixpkgs, and it may use nixpkgs as its input, but it exists for more than just the reason that it can represent newer versions of Idris2 than the one found in nixpkgs. To depend on an overlay to have overridden the right stuff in nixpkgs in order for the flake to work feels fragile and hard to follow IMO; if someone makes a mistake in a future change, instead of an obvious error about something being undefined, they may simply be unintentionally using part of the upstream nixpkgs when they should be overriding it.

---

I think you've cleaned a couple of things up that are worthwhile regardless of the rest and I am not saying I won't accept any PR that does more than the bare minimum number of line changes. It's more the flipping of the script that feels unnecessary.

[mitchmindtree]

If you move the existing packages up into the let block then the overlay can be defined with 7 lines of change.

I believe the main difference between this approach, and the approach taken in the PR, is that with the PR approach the overlay is accessible to non-flake users (as mentioned above). Feel free to correct me if I'm wrong and there's still some way for a non-flake user to use this!

It's more the flipping of the script that feels unnecessary.

I certainly have no grand overlay agenda 😅 If we don't mind about the non-flake-user use-case and would prefer to make minimal changes, I'm happy to change this to the diff you've shared above!

[mattpolzin]

I believe the main difference between this approach, and the approach taken in the PR, is that with the PR approach the overlay is accessible to non-flake users

I'm not sure what the most common way to use an overlay hosted in a third party repo is for a non-flake user, but since Idris2 uses flake-compat, the overlay is accessible with or without it being its own file (nix-instantiate --eval -A overlays.x86_64-darwin.default gets me the overlay via default.nix on my darwin laptop, for example). I'd say accessing the flake via default.nix is easier even because there's no need to provide an Idris2 version -- it's the exact Idris2 version/commit as you specified in fetchFromGitHub or similar.

[gallais]

How many .nix files does it take to change a lightbulb?
Jokes aside, I see they're almost all in a separate directory so go wild if you must.

[mitchmindtree]

@mattpolzin that's a good point that the overlay should technically still accessible via the flake.nix file itself.

I've added a commit that instead declares the overlay in terms of the package outputs. It's a little more verbose than your diff (as overlays are actually system agnostic) but still less changes than the original PR and hopefully easier to review.

[mattpolzin]

not a request for change, I just would not have ever thought to do it this way (as opposed to ../.) which I thought was interesting. Interesting that such an obviously equivalent path never crossed my mind.