Goodbye Agda
This commit is contained in:
parent
629829c2f9
commit
56a7f015e3
|
|
@ -34,8 +34,6 @@
|
|||
(local-set-key (kbd "C-n") 'comint-next-input)
|
||||
))
|
||||
|
||||
(require 'agda2)
|
||||
|
||||
(require 'bind-key)
|
||||
; (bind-key* "M-p" 'pixel-scroll-down)
|
||||
; (bind-key* "M-n" 'pixel-scroll-up)
|
||||
|
|
@ -154,16 +152,5 @@
|
|||
(put 'upcase-region 'disabled nil)
|
||||
(put 'narrow-to-region 'disabled nil)
|
||||
|
||||
(require 'agda-input)
|
||||
|
||||
(setq agda-input-tweak-all
|
||||
'(agda-input-compose
|
||||
(agda-input-prepend "!")
|
||||
(agda-input-nonempty))
|
||||
)
|
||||
(agda-input-setup)
|
||||
|
||||
(setq default-input-method "Agda")
|
||||
(add-to-list 'auto-mode-alist '("\\.lagda.md\\'" . agda2-mode))
|
||||
|
||||
; (setq ring-bell-function (lambda () (call-process "sh" nil 0 nil "-c" "find /Users/xenia/cloud/configs/resources -type f | egrep -v '/_' | shuf -n 1 | xargs afplay")))
|
||||
|
|
|
|||
67
flake.lock
67
flake.lock
|
|
@ -1,27 +1,5 @@
|
|||
{
|
||||
"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",
|
||||
|
|
@ -58,24 +36,6 @@
|
|||
"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"
|
||||
|
|
@ -177,11 +137,11 @@
|
|||
]
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1718222105,
|
||||
"narHash": "sha256-3hyVDQNIue0N505XlUGu9piUBlOYMPWaUk/iycVgNsU=",
|
||||
"lastModified": 1733339173,
|
||||
"narHash": "sha256-TGhQugZKrxz3Su5wcfC/muBwbPK2z8kGEdRzjUM1baY=",
|
||||
"ref": "refs/heads/main",
|
||||
"rev": "2da2cf21138f7de8e4238049f7bb3cdd97db9286",
|
||||
"revCount": 10457,
|
||||
"rev": "fc30e5e21fc6e8e2135ae164cd353a13501e643c",
|
||||
"revCount": 10465,
|
||||
"type": "git",
|
||||
"url": "https://githug.xyz/xenia/kakoune.git"
|
||||
},
|
||||
|
|
@ -246,24 +206,6 @@
|
|||
"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"
|
||||
}
|
||||
},
|
||||
"nixpkgs-unstable": {
|
||||
"locked": {
|
||||
"lastModified": 1733097829,
|
||||
|
|
@ -298,7 +240,6 @@
|
|||
},
|
||||
"root": {
|
||||
"inputs": {
|
||||
"agda": "agda",
|
||||
"ansi-utils": "ansi-utils",
|
||||
"home-manager": "home-manager",
|
||||
"kak": "kak",
|
||||
|
|
|
|||
|
|
@ -32,10 +32,6 @@
|
|||
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";
|
||||
# TODO: when nixos-24.11 drops, change this
|
||||
|
|
@ -43,7 +39,7 @@
|
|||
};
|
||||
};
|
||||
|
||||
outputs = { self, nixpkgs, nixpkgs-unstable, home-manager, nix-darwin, kak, unispect, ansi-utils, unambig-path, agda, nixos-apple-silicon }:
|
||||
outputs = { self, nixpkgs, nixpkgs-unstable, home-manager, nix-darwin, kak, unispect, ansi-utils, unambig-path, nixos-apple-silicon }:
|
||||
let
|
||||
mkPkgs = system: import nixpkgs { system = system; config.allowUnfree = true; };
|
||||
mkPkgsUnstable = system: import nixpkgs-unstable { system = system; config.allowUnfree = true; };
|
||||
|
|
@ -55,11 +51,9 @@
|
|||
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;
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
{ pkgs, username, home-dir, prompt-color, kak-pkg, unispect, ansi-utils, unambig-path, agda }:
|
||||
{ pkgs, username, home-dir, prompt-color, kak-pkg, unispect, ansi-utils, unambig-path }:
|
||||
|
||||
let
|
||||
kak = import ./kak.nix { kak = kak-pkg; inherit pkgs; };
|
||||
|
|
@ -12,8 +12,7 @@ in rec {
|
|||
home.stateVersion = "23.05";
|
||||
|
||||
home.packages =
|
||||
[ agda ] ++ (with pkgs.agdaPackages; [ standard-library cubical ])
|
||||
++ extras.all ++ (with pkgs; [
|
||||
extras.all ++ (with pkgs; [
|
||||
# Terminal utilities
|
||||
unispect
|
||||
ansi-utils.ansicols
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
{ pkgs, agda }:
|
||||
{ pkgs }:
|
||||
|
||||
let
|
||||
alacritty = import ./alacritty/alacritty.nix pkgs;
|
||||
|
|
@ -16,28 +16,6 @@ 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; [
|
||||
|
|
@ -52,7 +30,7 @@ in rec {
|
|||
programs.emacs = {
|
||||
package = pkgs.emacs;
|
||||
enable = true;
|
||||
extraPackages = epkgs: [agda2-mode] ++ (with epkgs; [
|
||||
extraPackages = epkgs: (with epkgs; [
|
||||
vterm bind-key rust-mode lsp-mode company meow haskell-mode
|
||||
terraform-mode nix-mode insert-kaomoji
|
||||
]);
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user