Build agda from source, install emacs lmao

flake.lock

@@ -1,5 +1,27 @@
 {
   "nodes": {
+    "agda": {
+      "inputs": {
+        "flake-parts": "flake-parts",
+        "nixpkgs": [
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1723809509,
+        "narHash": "sha256-aC0Vc/YV+rodv1qG839rqNFBqoqy/AkgvLdHxymCIu4=",
+        "owner": "agda",
+        "repo": "agda",
+        "rev": "df1a26d96683ebb06aa8476e4af6bbeddf23efbe",
+        "type": "github"
+      },
+      "original": {
+        "owner": "agda",
+        "ref": "v2.7.0",
+        "repo": "agda",
+        "type": "github"
+      }
+    },
     "ansi-utils": {
       "inputs": {
         "flake-utils": "flake-utils",
@@ -36,6 +58,24 @@
         "type": "github"
       }
     },
+    "flake-parts": {
+      "inputs": {
+        "nixpkgs-lib": "nixpkgs-lib"
+      },
+      "locked": {
+        "lastModified": 1701473968,
+        "narHash": "sha256-YcVE5emp1qQ8ieHUnxt1wCZCC3ZfAS+SRRWZ2TMda7E=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "34fed993f1674c8d06d58b37ce1e0fe5eebcb9f5",
+        "type": "github"
+      },
+      "original": {
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "type": "github"
+      }
+    },
     "flake-utils": {
       "inputs": {
         "systems": "systems"
@@ -194,11 +234,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1719956923,
+        "lastModified": 1726062281,
-        "narHash": "sha256-nNJHJ9kfPdzYsCOlHOnbiiyKjZUW5sWbwx3cakg3/C4=",
+        "narHash": "sha256-PyFVySdGj3enKqm8RQuo4v1KLJLmNLOq2yYOHsI6e2Q=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "706eef542dec88cc0ed25b9075d3037564b2d164",
+        "rev": "e65aa8301ba4f0ab8cb98f944c14aa9da07394f8",
         "type": "github"
       },
       "original": {
@@ -208,8 +248,27 @@
         "type": "github"
       }
     },
+    "nixpkgs-lib": {
+      "locked": {
+        "dir": "lib",
+        "lastModified": 1701253981,
+        "narHash": "sha256-ztaDIyZ7HrTAfEEUt9AtTDNoCYxUdSd6NrRHaYOIxtk=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "e92039b55bcd58469325ded85d4f58dd5a4eaf58",
+        "type": "github"
+      },
+      "original": {
+        "dir": "lib",
+        "owner": "NixOS",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
     "root": {
       "inputs": {
+        "agda": "agda",
         "ansi-utils": "ansi-utils",
         "home-manager": "home-manager",
         "kak": "kak",

flake.nix

@@ -29,13 +29,17 @@
       url = "git+https://git@githug.xyz/xenia/unambig-path";
       inputs.nixpkgs.follows = "nixpkgs";
     };
+    agda = {
+      url = "github:agda/agda?ref=v2.7.0";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
     nixos-apple-silicon = {
       url = "github:tpwrules/nixos-apple-silicon";
       inputs.nixpkgs.follows = "nixpkgs";
     };
   };
 
-  outputs = { self, nixpkgs, home-manager, nix-darwin, kak, unispect, ansi-utils, unambig-path, nixos-apple-silicon }:
+  outputs = { self, nixpkgs, home-manager, nix-darwin, kak, unispect, ansi-utils, unambig-path, agda, nixos-apple-silicon }:
     let
       mkPkgs = system: import nixpkgs { system = system; config.allowUnfree = true; };
       mkPkgsUnsupported = system: import nixpkgs { system = system; config.allowUnfree = true; config.allowUnsupportedSystem = true; };
@@ -46,9 +50,11 @@
         unispect = unispect.packages.${system}.unispect;
         ansi-utils = ansi-utils.packages.${system};
         unambig-path = unambig-path.packages.${system}.unambig-path;
+        agda = agda.packages.${system}.default;
       };
       mkPC = {system, pkgs} : import ./home/graphical.nix {
         inherit pkgs;
+        agda = agda.packages.${system}.default;
       };
       mkLaptop = {system, pkgs} : import ./home/apps.nix {
         inherit pkgs;

home/common.nix

@@ -1,4 +1,4 @@
-{ pkgs, username, home-dir, prompt-color, kak-pkg, unispect, ansi-utils, unambig-path }:
+{ pkgs, username, home-dir, prompt-color, kak-pkg, unispect, ansi-utils, unambig-path, agda }:
 
 let
   kak = import ./kak.nix { kak = kak-pkg; inherit pkgs; };
@@ -11,7 +11,9 @@ in rec {
 
   home.stateVersion = "23.05";
 
-  home.packages = with pkgs; extras.all ++ [
+  home.packages =
+    [ agda ] ++ (with pkgs.agdaPackages; [ standard-library cubical ])
+  ++ extras.all ++ (with pkgs; [
     # Terminal utilities
     unispect
     ansi-utils.ansicols
@@ -49,7 +51,7 @@ in rec {
     ngspice
 
     # (extras.challtools python311Packages)
-  ];
+  ]);
 
   # Let Home Manager install and manage itself.
   programs.home-manager.enable = true;

home/graphical.nix

@@ -1,4 +1,4 @@
-{ pkgs }:
+{ pkgs, agda }:
 
 let
   alacritty = import ./alacritty/alacritty.nix pkgs;
@@ -16,6 +16,28 @@ let
       cp -r Alloy.app $out/Applications
     '';
   };
+  agda2-mode = pkgs.emacsPackages.trivialBuild {
+    pname = "agda-mode";
+    version = agda.version;
+
+    dontUnpack = true;
+
+    # already byte-compiled by Agda builder
+    buildPhase = ''
+      agda=`${agda}/bin/agda-mode locate`
+      cp `dirname $agda`/*.el* .
+    '';
+
+    meta = {
+      inherit (agda.meta) homepage license;
+      description = "Agda2-mode for Emacs extracted from Agda package";
+      longDescription = ''
+        Wrapper packages that liberates init.el from `agda-mode locate` magic.
+        Simply add this to user profile or systemPackages and do `(require
+        'agda2)` in init.el.
+      '';
+    };
+  };
 
 in rec {
   home.packages = with pkgs; [
@@ -26,4 +48,13 @@ in rec {
   ;
 
   programs.alacritty = alacritty;
+  programs.emacs = {
+    package = pkgs.emacs;
+    enable = true;
+    extraPackages = epkgs: [agda2-mode] ++ (with epkgs; [
+      vterm bind-key rust-mode lsp-mode company meow haskell-mode
+      terraform-mode nix-mode insert-kaomoji
+    ]);
+    extraConfig = builtins.readFile ../dotfiles/init.el;
+  };
 }