Refactor flake.nix (#7032)

This PR makes the following changes:

* Add a `.envrc` file to auto-load the `flake.nix` when I enter the repository
  * This helps with e.g. Haskell VSCode integration
  * Only affects users of `direnv`
  * An alternative would be to add `.envrc` to the `.gitignore`, and let each developer write their own `.envrc`

* Refactor the `flake.nix` file
  * Replace the [deprecated attributes](NixOS/nix#5532) `defaultPackage` and `devShell`
  * Explicitly track the `nixpkgs` dependency
    * This seems to be the convention for most flakes I have viewed
  * Add comments
  * Stop using a nixpkg overlay
    * Overlays are verbose & not newbie-friendly
    * [Overlays are overkill here, and do not scale well](https://zimbatm.com/notes/1000-instances-of-nixpkgs)
  * Misc. refactoring to reduce length

I have tested the following features of `flake.nix`:

* `nix develop` starts a sub-shell with `cabal`,etc. where I can build agda
* `nix build` produces binaries in `result/bin/`

Commits:

* Add .envrc

* flake.nix: replace deprecated `.devShell` etc.

* flake.nix: track nixpkgs explicitly

As opposed to implicitly via the flake registry:
https://nixos.org/manual/nix/stable/command-ref/new-cli/nix3-flake#types

* flake.nix: de-overlay & add comments

* .gitignore nix build outputs

* flake.nix: bump nixpkgs pin

* flake.nix: add back overlay

Using flake-parts to keep the overlay non-obtrusive

* flake.nix: mark overlay as experimental

.envrc

@@ -0,0 +1,6 @@
+# Auto-load a development environment from flake.nix
+# when entering the root of the repository
+
+# This only affects users of the `direnv` tool
+
+use flake

.gitignore

@@ -83,3 +83,5 @@ stack.yaml
 stack*.yaml.lock
 trash.txt
 \#*\#
+.direnv
+result

flake.nix

@@ -1,61 +1,64 @@
 {
   description = "Agda is a dependently typed programming language / interactive theorem prover.";
 
-  inputs.flake-utils.url = "github:numtide/flake-utils";
+  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-23.11";
+  inputs.flake-parts.url = "github:hercules-ci/flake-parts";
 
-  outputs = { self, nixpkgs, flake-utils }: (flake-utils.lib.eachDefaultSystem (system: let
-    pkgs = import nixpkgs { inherit system; overlays = [ self.overlay ]; };
-  in {
-    packages = {
-      inherit (pkgs.haskellPackages) Agda;
+  outputs = inputs:
+      inputs.flake-parts.lib.mkFlake { inputs = inputs; } {
+    # Support all the OSes
+    systems = [ "x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin" ];
+    perSystem = {pkgs, ...}: let
+      hlib = pkgs.haskell.lib.compose;
+      hpkgs = pkgs.haskellPackages;
 
-      # TODO agda2-mode
-    };
-
-    defaultPackage = self.packages.${system}.Agda;
+      # The `agda` and `agda-mode` programs, built with `cabal build`
+      # (and GHC & Haskell libraries from the nixpkgs snapshot)
+      agda-pkg = hpkgs.developPackage {
+          root = ./.;
+          modifier = hlib.dontCheck;
+          # TODO Make check phase work
+          # At least requires:
+          #   Setting AGDA_BIN (or using the Makefile, which at least requires cabal-install)
+          #   Making agda-stdlib available (or disabling the relevant tests somehow)
+        };
 
-    devShell = pkgs.haskellPackages.shellFor {
-      packages = ps: with ps; [ Agda ];
-      nativeBuildInputs = with pkgs; [
-        cabal-install
-        haskell-language-server
-        haskellPackages.fix-whitespace
+      # Development environment with tools for hacking on agda
+      agda-dev-shell = hpkgs.shellFor {
+        # Which haskell packages to prepare a dev env for
+        packages = _: [agda-pkg];
+        # Extra software to provide in the dev shell
+        nativeBuildInputs = [
+            # Tools for building agda
+            pkgs.cabal-install
+            pkgs.haskell-language-server
+            hpkgs.fix-whitespace
+            # Tools for building the agda docs
+            (pkgs.python3.withPackages (py3pkgs: [
+              py3pkgs.sphinx
+              py3pkgs.sphinx_rtd_theme
+            ]))
+          ];
 
-        # documentation
-        (python3.withPackages (ps: with ps; [
-          sphinx
-          sphinx_rtd_theme
-        ]))
-      ];
-    };
-  })) // {
-    overlay = final: prev: {
-      haskellPackages = prev.haskellPackages.override {
-        overrides = self.haskellOverlay;
+        # Include an offline-usable `hoogle` command
+        # pre-loaded with all the haskell dependencies
+        withHoogle = true;
       };
-    };
 
-    haskellOverlay = final: prev: let
-      inherit (final) callCabal2nixWithOptions;
-
-      shortRev = builtins.substring 0 9 self.rev;
-
-      postfix = if self ? revCount then "${toString self.revCount}_${shortRev}" else "Dirty";
     in {
-      # TODO use separate evaluation system?
-      Agda = callCabal2nixWithOptions "Agda" ./. "--flag enable-cluster-counting --flag optimise-heavily" ({
-        mkDerivation = args: final.mkDerivation (args // {
-          version = "${args.version}-pre${postfix}";
+      packages.default = agda-pkg;        # Entry point for `nix build`
+      devShells.default = agda-dev-shell; # Entry point for `nix develop`
 
-          postInstall = "$out/bin/agda-mode compile";
-
-          # TODO Make check phase work
-          # At least requires:
-          #   Setting AGDA_BIN (or using the Makefile, which at least requires cabal-install)
-          #   Making agda-stdlib available (or disabling the relevant tests somehow)
-          doCheck = false;
-        });
-      });
+      # Allow power users to set this flake's agda
+      # as a drop-in replacement for nixpkgs's agda
+      # (including as a dependency of other nixpkgs packages)
+      # See https://flake.parts/overlays for more info
+      overlayAttrs.packages.haskellPackages.agda = agda-pkg;
+      # TODO: also replace each haskell.packages.ghcXXX.agda
     };
+    # Generate the overlays.default output from overlayAttrs above
+    # N.B. This overlay is EXPERIMENTAL and untested.
+    # Please report bugs to the Agda issue tracker.
+    imports = [ inputs.flake-parts.flakeModules.easyOverlay ];
   };
 }