From e6f909b4ce89287c1e4228e68b1fa983cf5372dc Mon Sep 17 00:00:00 2001 From: Jake Ginesin Date: Sat, 5 Jul 2025 16:16:45 -0400 Subject: [PATCH] 468 current 2025-07-05 16:16:07 25.05.20250424.f771eb4 6.12.24 * --- home/home.nix | 1 + home/programs/emacs/cfg/config.el | 41 ++++++++++++++++++++++++++++++- home/programs/emacs/cfg/init.el | 19 ++++++++------ home/programs/zsh/zshrc | 2 ++ system/networking/blockers.sh | 1 + 5 files changed, 55 insertions(+), 9 deletions(-) diff --git a/home/home.nix b/home/home.nix index e1c35a9..16912e9 100644 --- a/home/home.nix +++ b/home/home.nix @@ -103,6 +103,7 @@ in { cmatrix pipes-rs gimp + file # direnv # emacs # haha diff --git a/home/programs/emacs/cfg/config.el b/home/programs/emacs/cfg/config.el index 9746b74..b29504c 100644 --- a/home/programs/emacs/cfg/config.el +++ b/home/programs/emacs/cfg/config.el @@ -32,7 +32,8 @@ ;; There are two ways to load a theme. Both assume the theme is installed and ;; available. You can either set `doom-theme' or manually load a theme with the ;; `load-theme' function. This is the default: -(setq doom-theme 'doom-one) +; (setq doom-theme 'doom-one) +(setq doom-theme 'doom-ayu-dark) ;; This determines the style of line numbers in effect. If set to `nil', line ;; numbers are disabled. For relative line numbers, set this to `relative'. @@ -74,3 +75,41 @@ ;; ;; You can also try 'gd' (or 'C-c c d') to jump to their definition and see how ;; they are implemented. + +(after! proof-general + ;; Display proof state in a dedicated buffer on the right + (setq proof-three-window-mode-policy 'hybrid + proof-script-fly-past-comments t + proof-electric-terminator-enable t)) + +(after! company-coq + (setq company-coq-disabled-features '(hello))) ; silence “Hello” banner + +;; If you enabled +lsp, prefer LSP diagnostics over PG’s fringe marks +(setq lsp-coq-defeault-semantic-highlighting t) + + +(after! proof-general ; wait until PG is loaded + (map! :map coq-mode-map + :localleader ; first press your leader key + "RET" #'proof-goto-point)) + + +(after! proof-general + ;; , RET → jump to cursor + (map! :map coq-mode-map + :localleader ; starts with your "," key + :desc "Goto point" ; label for which-key + :n "RET" #'proof-goto-point ; Normal state + :v "RET" #'proof-goto-point ; Visual (optional) + :i "RET" #'proof-goto-point)) ; Insert (optional) + +(map! :after proof-general + :localleader + "RET" #'proof-goto-point) + +(map! :after proof-general + :leader + "RET" #'proof-goto-point) + +(setq doom-font (font-spec :family "Fira Code" :size 16)) diff --git a/home/programs/emacs/cfg/init.el b/home/programs/emacs/cfg/init.el index fbfa765..7a28785 100644 --- a/home/programs/emacs/cfg/init.el +++ b/home/programs/emacs/cfg/init.el @@ -1,6 +1,6 @@ ;;; init.el -*- lexical-binding: t; -*- -(setq doom-leader-key "," ;; global leader +(setq doom-leader-key "SPC" ;; global leader doom-localleader-key ",") ;; local-leader (setq x-super-keysym 'meta @@ -27,8 +27,8 @@ ;;layout ; auie,ctsrnm is the superior home row :completion - ;;company ; the ultimate code completion backend - (corfu +orderless) ; complete with cap(f), cape and a flying feather! + (company +childframe) ; the ultimate code completion backend + ;; (corfu +orderless) ; complete with cap(f), cape and a flying feather! ;;helm ; the *other* search engine for love and life ;;ido ; the other *other* search engine... ;;ivy ; a search engine for love and life @@ -119,12 +119,12 @@ ;;tty ; improve the terminal Emacs experience :lang - ;;agda ; types of types of types of types... + (agda +lsp) ; types of types of types of types... ;;beancount ; mind the GAAP ;;(cc +lsp) ; C > C++ == 1 ;;clojure ; java with a lisp ;;common-lisp ; if you've seen one lisp, you've seen them all - ;;coq ; proofs-as-programs + (coq +lsp) ; proofs-as-programs ;;crystal ; ruby at the speed of c ;;csharp ; unity, .NET, and mono shenanigans ;;data ; config/data formats @@ -139,7 +139,7 @@ ;;faust ; dsp, but you get to keep your soul ;;fortran ; in FORTRAN, GOD is REAL (unless declared INTEGER) ;;fsharp ; ML stands for Microsoft's Language - ;;fstar ; (dependent) types and (monadic) effects and Z3 + (fstar +lsp) ; (dependent) types and (monadic) effects and Z3 ;;gdscript ; the language you waited for ;;(go +lsp) ; the hipster dialect ;;(graphql +lsp) ; Give queries a REST @@ -152,8 +152,8 @@ ;;javascript ; all(hope(abandon(ye(who(enter(here)))))) ;;julia ; a better, faster MATLAB ;;kotlin ; a better, slicker Java(Script) - ;;latex ; writing papers in Emacs has never been so fun - ;;lean ; for folks with too much to prove + latex ; writing papers in Emacs has never been so fun + (lean +lsp) ; for folks with too much to prove ;;ledger ; be audit you can be ;;lua ; one-based indices? one-based indices markdown ; writing docs for people to ignore @@ -199,3 +199,6 @@ :config ;;literate (default +bindings +smartparens)) + +(add-to-list 'auto-mode-alist '("\\.v\\'" . coq-mode)) + diff --git a/home/programs/zsh/zshrc b/home/programs/zsh/zshrc index b79d32d..2fb38b8 100644 --- a/home/programs/zsh/zshrc +++ b/home/programs/zsh/zshrc @@ -199,6 +199,7 @@ alias nix-shell="nix-shell --run zsh" alias nix-snippets="echo 'flake-devshell, nix-default'" alias snippets="cd /home/synchronous/.config/nvim/snippets" alias emacs-cfg="cd /home/synchronous/nix-cfg/home/programs/emacs/cfg" +alias doom-cfg="cd /home/synchronous/nix-cfg/home/programs/emacs/cfg" alias nrc="cd /home/synchronous/nix-cfg/home/programs/nvim" @@ -211,6 +212,7 @@ alias htop="btop" # of course alias top="btop" # of course alias activecon="nmcli -t -f name connection show --active" alias dnsblock-clear="echo 'attemping to clear blocked dns...'; ls /var/lib/dnsmasq/conf.d; sudo rm -rf /var/lib/dnsmasq/conf.d/*; sudo systemctl restart dnsmasq;" +alias dnsblock-add="nvim /home/synchronous/nix-cfg/system/networking/blockers.sh" alias focus-wifi="nvim /home/synchronous/nix-cfg/system/networking/blockers.sh" stack() { diff --git a/system/networking/blockers.sh b/system/networking/blockers.sh index be0b33a..fa0737b 100644 --- a/system/networking/blockers.sh +++ b/system/networking/blockers.sh @@ -3,6 +3,7 @@ set -euo pipefail blacklist=( "NUwave" + "BostonPublicLibrary" ) should_block=false