468 current 2025-07-05 16:16:07 25.05.20250424.f771eb4 6.12.24 *

home/home.nix

@@ -103,6 +103,7 @@ in {
       cmatrix
       pipes-rs
       gimp
+      file
       # direnv
       # emacs # haha
 

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)) 

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
+       (company +childframe)           ; the ultimate code completion backend
-       (corfu +orderless)  ; complete with cap(f), cape and a flying feather!
+       ;; (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
+       latex             ; writing papers in Emacs has never been so fun
-       ;;lean              ; for folks with too much to prove
+       (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))
+

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() {

system/networking/blockers.sh

@@ -3,6 +3,7 @@ set -euo pipefail
 
 blacklist=(
   "NUwave"
+  "BostonPublicLibrary"
 )
 
 should_block=false