Emacs configuration
;; -*- lexical-binding: t; -*- (load-file "~/.config/sensitive.el")
Package Configuration
Add MELPA to the list of recognized archives
(require 'package) (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
Installs use-package if I don't have it already and enables verbose messages
(unless (package-installed-p 'use-package) (package-install 'use-package)) (require 'use-package) (setq use-package-verbose t)
Use-package always installs packages
(setq use-package-always-ensure t)
GNU keys to enable downloading packages
(use-package gnu-elpa-keyring-update)
Appearance
Define font style and height
(modify-all-frames-parameters '((font . "Roboto Mono 22"))) (modify-all-frames-parameters '((background-color . "#34293E")))
Set theme (currently Shades of Purple).
(setq custom-safe-themes t) (use-package doom-themes) (load-theme 'doom-shades-of-purple)
Disables a bunch of needless UI noise.
(cond ((> emacs-major-version 20) (tool-bar-mode -1) ; introduced in emacs 21 (menu-bar-mode -1) (scroll-bar-mode -1) (menu-bar-showhide-fringe-menu-customize-disable) (blink-cursor-mode -1) ))
Use Emacs to display the battery level.
(setq battery-update-interval 10)
(display-battery-mode 1)
Pretty mode line
(use-package doom-modeline)
(doom-modeline-mode 1)
(doom-modeline-def-modeline 'main
'(bar matches buffer-info buffer-position)
'(time major-mode battery))
Display time in mode line
(display-time-mode 1)
Allows me to see the column number as well as the line number.
(column-number-mode)
Cute icon for notifications
(setq alert-default-icon "/home/tiago/.dot-files/doom-cute.png")
utf-8
(set-locale-environment "UTF-8")
Conveniences
Don't use ui dialogs
(setq use-dialog-box nil)
Suppress annoying message any time you start a new frame
(setq server-client-instructions nil)
Enable recentf mode to remember recently opened files
(setq recentf-max-saved-items 10000) (recentf-mode 1) (add-to-list 'recentf-exclude (lambda (s) (cl-search "/test/" s))) (add-to-list 'recentf-exclude (lambda (s) (cl-search "/tmp/" s))) (add-to-list 'recentf-exclude (lambda (s) (cl-search "/sudo:" s)))
Every time a file is visited, update the list of recently visited files.
(add-hook 'find-file-hook 'recentf-save-list)
Undo and redo modifications to the window configuration. Use repeat mode to easily undo multiple modifications.
(winner-mode) (global-set-key "\C-xp" 'winner-undo) (global-set-key "\C-xn" 'winner-redo) (repeat-mode 1) (setq winner-repeat-map (let ((map (make-sparse-keymap))) (define-key map (kbd "p") 'winner-undo) (define-key map (kbd "n") 'winner-redo) map))
Disable repeat mode in Dired
(setq dired-jump-map nil)
Set scratch buffer major mode to org-mode
(setq initial-major-mode 'org-mode) (setq initial-scratch-message "")
Better keybinding to run a shell command
(global-set-key (kbd "M-s s") #'async-shell-command)
When running a shell command, do not display the command buffer until there is output.
(setq async-shell-command-display-buffer nil)
Minibuffer history persists across multiple sessions
(savehist-mode)
Ensures that backups and auto-saves go to a separate directory instead of stinking up the working directory.
(defvar backup-dir (expand-file-name "~/.emacs.d/backup/")) (defvar autosave-dir (expand-file-name "~/.emacs.d/autosave/")) (setq backup-directory-alist (list (cons ".*" backup-dir))) (setq auto-save-list-file-prefix autosave-dir) (setq auto-save-file-name-transforms `((".*" ,autosave-dir t)))
Package for using connecting and pairing Bluetooth devices
(use-package bluetooth)
Package for restoring and reading from the trash folder
(use-package trashed)
Package that displays when I am in Emacs on discord
(use-package elcord) (setq elcord-display-buffer-details nil) (setq elcord-editor-icon "doom_cute_icon") (elcord-mode)
Updates the PATH according to the environment in which Emacs is running
(use-package exec-path-from-shell) (when (daemonp) (exec-path-from-shell-initialize))
Normal scroll
(save-place-mode 1)
(setq mouse-wheel-progressive-speed nil)
(use-package flash) (bind-key "M-j" #'flash-jump)
(defun my-split-window-right (&optional arg) "Split the current window 70/30 rather than 50/50. A single-digit prefix argument gives the top window arg*10%. We use window-total-width to account for writeroom-mode." (interactive "P") (let ((proportion (* (or arg 6) .1))) (split-window-right (round (* proportion (window-total-width)))))) (global-set-key (kbd "C-x 3") 'my-split-window-right)
Editing Buffers
Enable creation of pairs of brackets or quotes when one is inserted.
(setq skeleton-pair t) (bind-key "(" 'skeleton-pair-insert-maybe) (bind-key "{" 'skeleton-pair-insert-maybe) (bind-key "[" 'skeleton-pair-insert-maybe) (bind-key (char-to-string 34) 'skeleton-pair-insert-maybe)
Enable Emacs to track changes made to files by different programs.
(setq auto-revert-interval 1)
(global-auto-revert-mode 1)
Delete trailing white spaces after saving a file.
(add-hook 'before-save-hook
'delete-trailing-whitespace)
Multiple cursors
(use-package multiple-cursors) (global-set-key (kbd "C->") 'mc/mark-next-like-this) (global-set-key (kbd "C-<") 'mc/mark-previous-like-this) (global-set-key (kbd "C-c C-<") 'mc/mark-all-like-this) (global-set-key (kbd "C-x x SPC") 'set-rectangular-region-anchor)
Yanking a string replaces the current selection
(delete-selection-mode 1)
Command to insert the current file name
(global-set-key (kbd "C-c w") (lambda () (interactive) (insert (buffer-file-name (window-buffer (minibuffer-selected-window))))))
Command to consult and insert from kill-ring
(global-set-key (kbd "C-c y") #'consult-yank-from-kill-ring) (global-set-key (kbd "C-x C-SPC") #'consult-mark)
Functions to shutdown and reboot the system.
(defun shutdown () (interactive) (async-shell-command "shutdown -h now")) (defun reboot () (interactive) (async-shell-command "shutdown -r now"))
#+endsrc
Popup windows
This makes it so every pop up window appears in the current window. We add special rules for the minor and major modes that are allowed to perform splits on the current window layout.
(add-to-list 'display-buffer-alist
'(""
(display-buffer-same-window)))
(add-to-list 'display-buffer-alist
'("magit-diff"
(display-buffer-no-window)))
(add-to-list 'display-buffer-alist
'((derived-mode
coq-response-mode coq-goals-mode mu4e-view-mode)
(display-buffer-no-window)))
GPG
;; let's get encryption established (use-package pinentry) (setenv "GPG_AGENT_INFO" nil) ;; use emacs pinentry (setq auth-source-debug t) (setq epg-gpg-program "gpg2") ;; not necessary (require 'epa-file) (epa-file-enable) (setq epa-pinentry-mode 'loopback) (setq epg-pinentry-mode 'loopback) (pinentry-start) (require 'org-crypt) (org-crypt-use-before-save-magic) (setq epa-file-encrypt-to email1) (setq epa-file-select-keys 1)
Coding Packages
Compilation
(use-package compile)
Jump to first error after compiling.
(setq compilation-auto-jump-to-first-error 'first-known)
Kill compilation buffer and window
(keymap-set compilation-mode-map "q" #'kill-buffer-and-window)
Flymake
Package used by Eglot for highlighting errors
(use-package flymake) (add-hook 'prog-mode-hook #'flymake-mode) (keymap-set flymake-mode-map "C-c C-x" #'flymake-goto-next-error)
Corfu
Package for completion suggestions
(use-package corfu) (setq corfu-auto t) (global-corfu-mode 1) (corfu-popupinfo-mode 1) (setq corfu-popupinfo-delay nil) (keymap-set corfu-popupinfo-map "C-M-i" #'corfu-popupinfo-toggle) (use-package nerd-icons-corfu) (add-to-list 'corfu-margin-formatters #'nerd-icons-corfu-formatter)
OCaml packages
(use-package tuareg :vc (:url "https://github.com/mrjazzybread/tuareg" :rev :newest))
Compile at root of directory
(keymap-set tuareg-mode-map "C-c C-c" #'project-compile)
Use dune build to compile OCaml projects
(add-hook 'tuareg-mode-hook
(lambda ()
(if (eq (project-current) nil)
(setq-local compile-command
(concat "ocaml " (buffer-file-name)))
(setq-local compile-command "dune build && dune install"))))
(add-hook 'dune-mode-hook
(lambda () (setq-local compile-command "dune build && dune install")))
Format OCaml code after saving the buffer
(use-package ocamlformat) (setq ocamlformat-enable 'enable-outside-detected-project) (setq ocamlformat-show-errors nil) (add-hook 'before-save-hook #'ocamlformat-before-save)
Dune package
(use-package dune)
Rust packages
(use-package rustic) (setq rustic-lsp-client #'eglot)
Eglot
Prevent Eglot from being using when writing Rocq.
(defun lsp-no-coq () (interactive) (unless (eq major-mode 'coq-mode) (eglot-ensure))) (use-package eglot) (add-hook 'prog-mode-hook #'lsp-no-coq) (add-hook 'LaTeX-mode-hook #'eglot-ensure)
Eldoc popup. Useful for displaying documentation and errors. I have it set to a keybinding and not a timer since I prefer to control what pop ups appear.
(use-package eldoc-box) (setq eldoc-box-only-multi-line t) (bind-key "\C-hj" #'eldoc-box-help-at-point)
Git packages
Folks… It's Magit.
(use-package magit) (keymap-set magit-mode-map "C-c C-p" #'magit-section-up) (setq magit-display-buffer-function #'magit-display-buffer-traditional) (setq magit-bury-buffer-function 'magit-restore-window-configuration) (bind-key "C-x g" #'magit-status)
Automatically save files when entering Magit.
(setq magit-save-repository-buffers 'dontask)
Commit on every file save. I use this to sync my agenda files automatically.
(use-package git-auto-commit-mode) (setq gac-automatically-add-new-files-p t)
Miscellaneous Coding packages
(use-package yaml-mode) (use-package boogie-friends) (setq flycheck-dafny-executable "/usr/bin/dafny")
Dired
By default, deleting a file removes it from your file system. This makes it so that deleting files moves them to the trash folder.
(setq delete-by-moving-to-trash t)
dired presents a bunch of details about each file that I don't file
particularly useful. This makes it so dired only presents the name of
the file.
(add-hook 'dired-mode-hook #'dired-hide-details-mode)
By default, dired shows hidden files. By enabling dired-omit-mode,
dired we can hide them.
(add-hook 'dired-mode-hook #'dired-omit-mode)
Sometimes we might want to see hidden files. This makes it so that
pressing o reveals them.
(keymap-set dired-mode-map "o" #'dired-omit-mode)
The files that I want to omit with dired-omit-mode.
(setq dired-omit-files (rx (or (seq bol (? ".") "#") ;; emacs autosave files (seq bol ".") ;; dot-files (seq "~" eol) ;; backup-files (seq bol "CVS" eol) ;; CVS dirs )))
Disable "Omit N files" message that appears in the minibuffer after
enabling dired-omit-mode.
(setq dired-omit-verbose nil)
Pressing the b key moves you up the directory hierarchy.
(keymap-set dired-mode-map "b" #'dired-up-directory)
Opening a lot of dired buffers can lead to extreme clutter your buffer
list. This option makes it so that whenever you go into a new
directory from a dired buffer, Emacs kills the current dired buffer.
(setq dired-kill-when-opening-new-dired-buffer t)
Dired buffers update when there is a change in one of the files in the directory
(setq global-auto-revert-non-file-buffers t)
Adds icons to dired buffers for each file. Note that you may need to
install extra fonts for this to work correctly. For instructions on
how to do this, go to the GitHub for all-the-icons.
;This package requires additional fonts (use-package all-the-icons) (use-package all-the-icons-dired :hook (dired-mode . all-the-icons-dired-mode))
Change ls switches to use human readable file sizes and to list
directories first.
(setq dired-listing-switches "-alh --group-directories-first")
When copying a file, have it so if there is another dired buffer open in another window in the same frame, it selects that buffer by default
(setq dired-dwim-target t)
Use mu4e to manage emails. Naturally, requires mu4e to already be installed.
(require 'mu4e)
Fancy dashboard for mu4e. Requires local file
(use-package async) (load "~/.mu4e-dashboard/mu4e-dashboard.el")
This is necessary so that mu4e won't print an annoying error message
(setq user-mail-address email1)
Function to use for sending emails.
(setq message-send-mail-function 'smtpmail-send-it)
Quitting mu4e returns to the dashboard
(keymap-set mu4e-headers-mode-map "q" #'mu4e-dashboard)
Avoids mail syncing issues
(setq mu4e-change-filenames-when-moving t) (setq mu4e-context-policy "pick-first")
Refreshes email every minute
(setq mu4e-update-interval 60) (setq mu4e-get-mail-command "mbsync -a")
Set mail directory
(setq mu4e-maildir "~/mail")
Creates two contexts for my two work emails.
(setq mu4e-contexts (list ;; Work account (make-mu4e-context :name "FCT" :match-func (lambda (msg) (when msg (string-prefix-p "/gmail" (mu4e-message-field msg :maildir)))) :vars `((user-mail-address . ,email1) (user-full-name . "Tiago Soares") (smtpmail-smtp-server . "smtp.gmail.com") (smtpmail-smtp-service . 465) (smtpmail-stream-type . ssl) (mu4e-drafts-folder . "/gmail/[Gmail]/Drafts") (mu4e-sent-folder . "/gmail/[Gmail]/Sent Mail") (mu4e-refile-folder . "/gmail/[Gmail]/All Mail") (mu4e-trash-folder . "/gmail/[Gmail]/Trash"))) (make-mu4e-context :name "Inria" :match-func (lambda (msg) (when msg (string-prefix-p "/inria" (mu4e-message-field msg :maildir)))) :vars `((user-mail-address . ,email2) (user-full-name . "Tiago Soares") (smtpmail-smtp-server . "smtp.inria.fr") (smtpmail-smtp-service . 587) (smtpmail-stream-type . nil) (mu4e-drafts-folder . "/inria/Drafts") (mu4e-sent-folder . "/inria/Sent") (mu4e-trash-folder . "/inria/Trash"))) ) )
Notifications for mu4e
(use-package mu4e-alert) (mu4e-alert-set-default-style 'libnotify) (mu4e-alert-enable-notifications) (setq mu4e-alert-icon "/home/tiago/.dot-files/email.png")
Human readable header fields
(setq mu4e-headers-fields '((:human-date . 12) (:from . 22) (:subject)))
Better reading and writing experience for emails
(add-hook 'mu4e-view-mode-hook #'writeroom-mode) (add-hook 'mu4e-headers-mode-hook #'writeroom-mode) (add-hook 'message-mode-hook #'auto-fill-mode)
Suppress annoying "Indexing… message"
(setq mu4e-hide-index-messages t)
Fold threads at startup
(add-hook 'mu4e-thread-mode-hook #'mu4e-thread-fold-all)
Start mu4e
(mu4e)
Org
Some Basic Bookkeeping
Automatically commit changes to org files.
(setq-default gac-automatically-push-p t)
Some helpful variables
(defun org-directory (file) (concat "~/roam/daily/personal/" file)) (defvar todo-file (org-directory "todo.org.gpg")) (defvar agenda-file (org-directory "appoint.org.gpg")) (defvar log-file (org-directory "albums.org.gpg")) (defvar papers-file (org-directory "papers.org.gpg"))
My agenda files:
(setq org-agenda-file-regexp "\\`[^.].*\\.org\\\(\\.gpg\\\)?\\'") (setq org-agenda-files (list todo-file agenda-file log-file papers-file))
Settings for exporting Org files with citations to TeX.
(setq org-cite-export-processors '((t biblatex "numeric" "numeric"))) (setq org-cite-global-bibliography '("~/.dot-files/latex/english.bib")) (setq org-export-with-sub-superscripts nil)
Restore the window configuration when quitting the agenda view
(setq org-agenda-restore-windows-after-quit t)
Enable notifications for Org agenda items
(use-package org-alert) (setq alert-default-style 'libnotify) (setq org-alert-interval 300) (setq org-alert-notify-cutoff 10) (setq org-alert-notify-after-event-cutoff 0) (org-alert-enable)
Add menu item to list only items with a TODO keyword.
(add-to-list 'org-agenda-custom-commands
'("t" "List all PhD tasks" ((todo "TODO"))
((org-agenda-files (list todo-file)))))
Add menu item to list albums I haven't listened yet.
(add-to-list 'org-agenda-custom-commands
'("l" "List all unlistened albums" ((todo "TODO"))
((org-agenda-files (list log-file)))))
Add menu item to list unread papers
(add-to-list 'org-agenda-custom-commands
'("p" "List all unread papers" ((todo "TODO"))
((org-agenda-files (list papers-file)))))
Add Markdown as a an export backend
(require 'ox-md) (add-to-list 'org-export-backends 'md)
Update agenda on startup
(start-process-shell-command "update" nil "cd $HOME/roam/daily && git pull")
List TODO items in column-view-mode
(setq org-agenda-view-columns-initially t)
Do not list sub tasks
(setq org-agenda-todo-list-sublevels nil)
In column view mode only show the name of the heading by default
(setq org-columns-default-format "%70ITEM")
Appearance
Hide emphasis markers and macro braces
(setq org-hide-emphasis-markers t) (setq org-hide-macro-markers t)
Make it there is only one star visible in each heading.
(setq org-hide-leading-stars t)
Use LaTeX like syntax to insert special symbols
(setq org-pretty-entities t)
Start Org files with each heading folded.
(setq org-startup-folded 'content)
Enable Org indentation
(setq org-startup-indented t)
Center Org agenda
(add-hook 'org-agenda-mode-hook #'writeroom-mode)
Don't show items that are marked as done.
(setq org-agenda-skip-timestamp-if-done t
org-agenda-skip-deadline-if-done t
org-agenda-skip-scheduled-if-done t
org-agenda-skip-scheduled-if-deadline-is-shown t
org-agenda-skip-timestamp-if-deadline-is-shown t)
Automatic latex preview in Org mode
(setq org-startup-with-latex-preview t)
Package for editing latex snippets in Org-mode.
(use-package org-fragtog)
(add-hook 'org-mode-hook #'org-fragtog-mode)
Scale up latex preview in Org mode
(setq org-format-latex-options (plist-put org-format-latex-options :scale 3))
Org agenda takes up the full window
(setq org-agenda-window-setup 'only-window)
Org agenda does not display the files in which items are written in.
(setq org-agenda-prefix-format '((agenda . "%?-12t% s") (todo . "%-12:c") (tags . "%-12:c") (search . "%-12:c")))
Org agenda starts on the current day
(setq org-agenda-start-on-weekday nil)
Add Rocq and Gospel to the list of languages that Org is aware of
(add-to-list 'org-babel-tangle-lang-exts '("rocq" . "v")) (add-to-list 'org-babel-tangle-lang-exts '("gospel" . "mli")) (add-to-list 'org-src-lang-modes '("gospel" . tuareg)) (add-to-list 'org-src-lang-modes '("rocq" . coq))
Add "WONT-DO" to the todo tags.
(setq org-todo-keywords '((sequence "TODO(t)" "|" "DONE(d!)" "WONT-DO(w@/!)")))
TODO tag colors
(setq org-todo-keyword-faces '(("TODO" . (:foreground "GoldenRod" :weight bold)) ("DONE" . (:foreground "LimeGreen" :weight bold)) ("WONT-DO" . (:foreground "Firebrick" :weight bold))))
Org Pretty Symbols
Function for adding pretty symbols for Org mode. Most of these are just so that Org mode environments aren't awful to look at.
;; Pretty Symbols for Org (defun add-symbols () (push '("#+end_example" . ? ) prettify-symbols-alist) (push '("#+end_src" . ? ) prettify-symbols-alist) (push '("#+begin_src ocaml" . ?🐫) prettify-symbols-alist) (push '("#+begin_src gospel" . ?🛐) prettify-symbols-alist) (push '("#+begin_src rocq" . ?🦅) prettify-symbols-alist) (push '("#+begin_example ocaml :why3" . ?❔) prettify-symbols-alist) (push '("#+begin_src emacs-lisp" . ?🗿) prettify-symbols-alist) (push '("->" . ?→) prettify-symbols-alist) (push '("<->" . ?↔) prettify-symbols-alist) (push '("|-" . ?⊢) prettify-symbols-alist) (push '("/\\" . ?∧) prettify-symbols-alist) (push '("\\/" . ?∨) prettify-symbols-alist) (push '("<-" . ?←) prettify-symbols-alist) (prettify-symbols-mode 1)) (add-hook 'org-mode-hook #'add-symbols)
Search for albums
This function searches for albums in my personal list from a certain
artist (this can probably be simplified with org-ql).
(defun list-albums-by-artist () (interactive) (with-current-buffer "art.org.gpg" (let* ((value (completing-read "Value: " (mapcar #'list (org-property-values "ARTIST"))))) (unless (string-match "\\`{.*}\\'" value) (setq value (concat "\"" value "\""))) (switch-to-buffer "art.org.gpg") (org-match-sparse-tree nil (concat "ARTIST=" value)) )))
Remove Spell Checking in Code Blocks
(add-to-list 'ispell-skip-region-alist '("^#\\+BEGIN_SRC" . "#\\+END_SRC")) (add-to-list 'ispell-skip-region-alist '("^#\\+BEGIN_EXAMPLE" . "#\\+END_EXAMPLE")) (add-to-list 'ispell-skip-region-alist '("^#\\+begin_src" . "#\\+end_src")) (add-to-list 'ispell-skip-region-alist '("^#\\+begin_example" . "#\\+end_example")) (add-to-list 'ispell-skip-region-alist '("^#\\+" . "\n")) (add-to-list 'ispell-skip-region-alist '("~" . "~")) (add-to-list 'ispell-skip-region-alist '("/" . "/")) (add-to-list 'ispell-skip-region-alist '("{{{" . "}}}")) (add-to-list 'ispell-skip-region-alist '("<<" . ">>"))
Org Key Bindings and Hooks
Global key bindings to access and update the agenda.
(global-set-key "\C-ca" 'org-agenda) (global-set-key "\C-cc" 'org-capture)
Keybindings to navigate agenda view
(keymap-set org-agenda-keymap "n" #'org-agenda-next-item) (keymap-set org-agenda-keymap "p" #'org-agenda-previous-item)
Org Roam
(use-package org-roam) (setq org-roam-directory (file-truename "~/roam")) (setq org-roam-file-exclude-regexp '("data/" "daily/")) (setq org-roam-completion-everywhere t) (keymap-global-set "C-c n l" #'org-roam-buffer-toggle) (keymap-global-set "C-c n f" #'org-roam-node-find) (keymap-global-set "C-c n g" #'org-roam-graph) (keymap-global-set "C-c n i" #'org-roam-node-insert) (keymap-global-set "C-c n c" #'org-roam-capture) (keymap-global-set "C-c n j" #'org-roam-dailies-capture-today) (org-roam-db-autosync-mode)
Capture templates for org roam.
(setq org-roam-capture-templates '(("t" "travel" plain "%?" :if-new (file+head "travel/%<%Y%m%d%H%M%S>-${slug}.org" "#+title: ${title}\n") :unnarrowed t) ("r" "Reading note" plain (file "~/roam/templates/reading_template.org") :if-new (file+head "research/%<%Y%m%d%H%M%S>-${slug}.org.gpg" "#+title: ${title}\n") :unnarrowed t) ("p" "PhD Note" plain "%?" :if-new (file+head "research/%<%Y%m%d%H%M%S>-${slug}.org.gpg" "#+title: ${title}\n") :unnarrowed t :jump-to-captured t) ))
Capture template for org roam dailies
(setq org-roam-dailies-capture-templates '(("d" "default" plain "* %?" :target (file+head "%<%Y-%m-%d>.org.gpg" "#+title: %<%Y-%m-%d> ") :jump-to-captured t)))
PDFs
Opens the current file in zathura and kills the Doc View buffer.
(defun zathura () (when (equal (file-name-extension (buffer-file-name)) "pdf") (start-process "zathura" nil "zathura" (buffer-file-name)) (let ((b (current-buffer))) (add-to-list 'recentf-list (buffer-file-name)) (recentf-save-list) (previous-buffer) (kill-buffer b) )))
When we open a PDF in Emacs, open it in zathura instead.
(add-hook 'doc-view-mode-hook #'zathura)
Function to run a latex process in the background.
(defun run-latex () (interactive) (async-shell-command "latexmk -pdf -pdflatex='pdflatex -interaction=nonstopmode' -pvc --synctex=1 -use-make main.tex" "LaTeX"))
Proof General
Package for working with Rocq
(use-package proof-general)
Removes the EXTREMELY annoying proof general splash screen
(setq proof-splash-enable nil)
When starting a proof, splits windows so that the goals window is larger than the response window
(setq proof-three-window-mode-policy 'hybrid)
Weird arrow :/
(setq overlay-arrow-string "")
Function to generate a Rocq Makefile
(defun coq-makefile-gen () (interactive) (async-shell-command "coq_makefile -f _CoqProject -o Makefile"))
Why3 configuration
(setq opam-share (if (boundp 'opam-share) opam-share (ignore-errors (car (process-lines "opam" "var" "share"))))) (setq why3-share (if (boundp 'why3-share) why3-share (ignore-errors (car (process-lines "why3" "--print-datadir"))))) (setq why3el (let ((f (expand-file-name "emacs/why3.elc" why3-share))) (if (file-readable-p f) f (when (and opam-share (file-directory-p opam-share)) (let ((f (expand-file-name "emacs/site-lisp/why3.elc" opam-share))) (if (file-readable-p f) f nil)))))) (when why3el (require 'why3 why3el))
Unicode Symbols for Iris
;; Input of unicode symbols (use-package math-symbol-lists) ; Automatically use math input method for Coq files (add-hook 'coq-mode-hook (lambda () (set-input-method "math"))) (add-hook 'tuareg-mode-hook (lambda () (set-input-method "math"))) ; Input method for the minibuffer ;; (defun my-inherit-input-method () ;; "Inherit input method from `minibuffer-selected-window'." ;; (let* ((win (minibuffer-selected-window)) ;; (buf (and win (window-buffer win)))) ;; (when buf ;; (activate-input-method (buffer-local-value 'current-input-method buf))))) ;; (add-hook ' ;; minibuffer-setup-hook #'my-inherit-input-method) ; Define the actual input method (quail-define-package "math" "UTF-8" "Ω" t) (quail-define-rules ; add whatever extra rules you want to define here... ("\\fun" ?λ) ("\\mult" ?⋅) ("\\ent" ?⊢) ("\\valid" ?✓) ("\\diamond" ?◇) ("\\box" ?□) ("\\bbox" ?■) ("\\later" ?▷) ("\\pred" ?φ) ("\\and" ?∧) ("\\or" ?∨) ("\\comp" ?∘) ("\\ccomp" ?◎) ("\\all" ?∀) ("\\ex" ?∃) ("\\to" ?→) ("\\sep" ?∗) ("\\lc" ?⌜) ("\\rc" ?⌝) ("\\Lc" ?⎡) ("\\Rc" ?⎤) ("\\lam" ?λ) ("\\empty" ?∅) ("\\Lam" ?Λ) ("\\Sig" ?Σ) ("\\-" ?∖) ("\\aa" ?●) ("\\af" ?◯) ("\\auth" ?●) ("\\frag" ?◯) ("\\iff" ?↔) ("\\gname" ?γ) ("\\incl" ?≼) ("\\latert" ?▶) ("\\update" ?⇝) ("\\nin" ?∉) ("\\u" ?∪) ("\\points" ?↦) ;; accents (for iLöb) ("\\o" ?ö) ;; subscripts and superscripts ("^^+" ?⁺) ("__+" ?₊) ("^^-" ?⁻) ("__0" ?₀) ("__1" ?₁) ("__2" ?₂) ("__3" ?₃) ("__4" ?₄) ("__5" ?₅) ("__6" ?₆) ("__7" ?₇) ("__8" ?₈) ("__9" ?₉) ("__a" ?ₐ) ("__e" ?ₑ) ("__h" ?ₕ) ("__i" ?ᵢ) ("__k" ?ₖ) ("__l" ?ₗ) ("__m" ?ₘ) ("__n" ?ₙ) ("__o" ?ₒ) ("__p" ?ₚ) ("__r" ?ᵣ) ("__s" ?ₛ) ("__t" ?ₜ) ("__u" ?ᵤ) ("__v" ?ᵥ) ("__x" ?ₓ) ) (mapc (lambda (x) (if (cddr x) (quail-defrule (cadr x) (car (cddr x))))) ; need to reverse since different emacs packages disagree on whether ; the first or last entry should take priority... ; see <https://mattermost.mpi-sws.org/iris/pl/46onxnb3tb8ndg8b6h1z1f7tny> for discussion (reverse (append math-symbol-list-basic math-symbol-list-extended)))
Settings for Text Mode
Enable auto-fill.
(add-hook 'text-mode-hook #'auto-fill-mode)
(setq fill-column 80)
Enable Writeroom mode for a more comfortable writing experience.
(use-package writeroom-mode) (add-hook 'text-mode-hook #'writeroom-mode) (setq writeroom-mode-line t) (setq writeroom-maximize-window nil)
Use aspell as default spell checking program (should be default, but
something is changing it)
(setq ispell-program-name "/usr/bin/aspell")
Enable Flyspell for spell checking
(use-package flyspell) (add-hook 'text-mode-hook #'flyspell-mode) (add-hook 'prog-mode-hook #'flyspell-prog-mode) (use-package flyspell-correct) (keymap-set flyspell-mode-map "M-$" #'flyspell-correct-wrapper)
Removes completion at point from flyspell so that I can use it for
completing org roam nodes.
(require 'flyspell) (keymap-unset flyspell-mode-map "C-M-i")
Disable word completion in text-mode
(setq text-mode-ispell-word-completion nil)
Automatic insertion of right brace in Latex-mode
(setq LaTeX-electric-left-right-brace t)
Hide Markdown markup
(setq markdown-hide-markup t)
Minibuffer completion w/Vertico
(use-package vertico)
(vertico-mode 1)
Allows using minibuffer commands within the minibuffer.
(setq enable-recursive-minibuffers t)
M-TAB expands the prefix of candidates (TAB completion).
(keymap-set vertico-map "M-TAB" #'minibuffer-complete)
Completion at point uses Vertico
(setq completion-in-region-function #'consult-completion-in-region)
Orderless allows for more flexible completion styles.
(use-package orderless) (setq completion-styles '(orderless basic)) (setq completion-category-overrides '((file (styles partial-completion)))) (setq completion-category-defaults nil) ;; Disable defaults, use orderless settings (setq completion-pcm-leading-wildcard t) ;; Emacs 31: partial-completion behaves like substring
More information in minibuffer
(use-package marginalia)
Icons in minibuffer
(use-package all-the-icons) (use-package all-the-icons-completion) (add-hook 'marginalia-mode-hook #'all-the-icons-completion-marginalia-setup) (all-the-icons-completion-mode) (marginalia-mode)
Keybindings for switch to buffer.
(global-set-key (kbd "C-x b") #'consult-project-buffer) (global-set-key (kbd "C-x C-b") #'consult-buffer)
No live preview when switching buffers
(setq consult-preview-excluded-buffers t)
Replace I-search with consult-line. Vertico cycle is set to t so that
we can go to candidates in lines previous to the one we started in.
(setq vertico-cycle t) (global-set-key (kbd "C-s") #'consult-line)
Eshell
(use-package eshell)
Fish like suggestions for eshell
(use-package capf-autosuggest)
(add-hook 'eshell-mode-hook #'capf-autosuggest-mode)
Increase the history size. This is helpful when using capf-autosuggest
since that package checks the history for completion candidates.
(setq eshell-history-size 50000)
Pretty eshell prompt
(load-file "/home/tiago/.config/prompt.el") (setq eshell-prompt-function #'epe-theme-dakrone)
Function for clearing the shell
(defun eshell-clear () (interactive) "Clear the eshell buffer." (let ((inhibit-read-only t)) (erase-buffer) (eshell-send-input) (beginning-of-buffer) (kill-line) (end-of-buffer) ))
Always spawns eshell on a new terminal
(defun multi-eshell () (interactive) (let ((b (current-buffer))) (when (seq-find (lambda (val) (equal "*eshell*" (buffer-name val))) (buffer-list)) (switch-to-buffer "*eshell*") (rename-uniquely)) (switch-to-buffer b) (eshell)))
Delete duplicates in the eshell history
(setq eshell-hist-ignoredups t)
Augments eshell's completion framework so that it behaves more like
fish (e.g. "pacman -S …" completes the name of the package)
(use-package fish-completion)
(global-fish-completion-mode 1)
I never know man
(setq eshell-cmpl-dir-ignore "\\`\\(CVS\\)/\\'")
Add rust packages to path
(add-to-list 'exec-path "~/.cargo/bin")
Buffer name matches eshell directory
(defun sync-dir-in-buffer-name () (rename-buffer (concat "*eshell* " default-directory) t)) (add-hook 'eshell-mode-hook #'sync-dir-in-buffer-name) (add-hook 'eshell-directory-change-hook #'sync-dir-in-buffer-name)
No message when starting eshell
(setq eshell-banner-message "")
Keybinding to clear the shell
(keymap-set eshell-mode-map "C-l" #'eshell-clear)
We use eat to run any commands that require visuals
(use-package eat) (setq eat-kill-buffer-on-exit t) (add-hook 'eshell-mode-hook #'eat-eshell-mode)
Typst
(use-package typst-ts-mode)
Command to compile a Typst project.
(defun run-typst () (interactive) (async-shell-command "typst watch main.typ" "Typst"))
Elfeed
Package to read RSS feeds.
(use-package elfeed)
Update RSS on startup and every 2 hours.
(elfeed-update) (run-at-time nil (* 2 60 60) #'elfeed-update)
RSS feed database
(setq elfeed-feeds '("https://rss.arxiv.org/atom/cs.PL" "https://www.worldpoliticsreview.com/feed/" "https://www.reddit.com/r/emacs.rss" "https://www.patreon.com/rss/chapotraphouse?auth=2TG4bQg76BCEXmj_RpOzlvax9O8TUffh"))
Multimedia
Loads my music library onto EMMS (Emacs Multimedia System)
(use-package emms) (emms-all) (emms-add-file "~/music") (emms-shuffle)
Set MPV as my default music player.
(setq emms-player-list '(emms-player-mpv))
Makes it so playerctl works with EMMS.
(emms-mpris-enable)
Gospel Specific Things
Some macros to help writing Rocq proofs of Gospel signatures.
(defun gospel-abstract (var) (interactive "sName:") (insert (format "Global Instance _%s_inst : _%s_sig :=" var var)) (newline 1 t) (insert (format "{ %s := }." var)) (backward-char 3)) (defun gospel-lemma (var) (interactive "sName:") (insert (format "#[refine] Global Instance _%s_inst : _%s_sig := { }." var var var)) (newline 1 t) (insert "Proof.") (newline 1 t))
Function to insert Gospel header
(defun gospel-header () (interactive) (insert "(**************************************************************************) (* *) (* GOSPEL -- A Specification Language for OCaml *) (* *) (* Copyright (c) 2018- The VOCaL Project *) (* *) (* This software is free software, distributed under the MIT license *) (* (as described in file LICENSE enclosed). *) (**************************************************************************) "))
Add the preamble necessary to write math symbols in a latex Gospel code block.
(defun gospel-unicode () (interactive) (tag-word-or-region "*?$" "$?*")) (require 'latex) (keymap-set LaTeX-mode-map "C-c C-x C-m" #'gospel-unicode)
Remove escaped Latex code
(defun delete-until-end () (while (and (< (point) (- (point-max) 1)) (not (and (eq (char-after) ?\?) (eq (char-after (+ (point) 1)) ?*)))) (delete-char 1)) (delete-char 2)) (defun delete-gospel-escape () (beginning-of-buffer) (while (< (point) (- (point-max) 1)) (if (and (eq (char-after) ?*) (eq (char-after (+ (point) 1)) ?\?)) (delete-until-end) (forward-char))) (save-buffer)) (add-hook 'org-babel-post-tangle-hook #'delete-gospel-escape)
-e * EXWM
(use-package exwm)
Setting the initial workspace number
(setq exwm-workspace-number 5)
Make it so that EXWM buffers are named after the window they are managing
(add-hook 'exwm-update-class-hook
(lambda () (exwm-workspace-rename-buffer exwm-class-name)))
In an EXWM buffer, the bindings on the left are mapped to the bindings on the right. This way, we can use Emacs keybindings in X windows.
(setq exwm-input-simulation-keys
'(([?\C-b] . [left])
([?\C-f] . [right])
([?\M-f] . [C-right])
([?\M-b] . [C-left])
([?\C-p] . [up])
([?\C-n] . [down])
([?\C-a] . [home])
([?\C-e] . [end])
([?\M-v] . [prior])
([?\M-w] . [C-c])
([?\C-y] . [C-v])
([?\C-_] . [C-z])
([?\C-v] . [next])
([?\C-d] . [delete])
([?\C-s] . [C-f])
([?\C-k] . [S-end delete])
([?\C- ] . [C-a])
([?\C-g] . [escape])
([?\C-j] . [S-return])
([?\C-w] . [C-x])
))
Minor mode to rename Firefox EXWM buffers to the names of the respective tabs.
(use-package exwm-firefox-core) (load-file "~/exwm-firefox.el") (exwm-firefox-mode 1)
Better splitting of windows
(defun my-split-window-right (&optional arg) "Split the current window 70/30 rather than 50/50. A single-digit prefix argument gives the top window arg*10%. We use window-total-width to account for writeroom-mode." (interactive "P") (let ((proportion (* (or arg 6) .1))) (split-window-right (round (* proportion (window-total-width)))))) (global-set-key (kbd "C-x 3") 'my-split-window-right)
Sometimes when switching to an X window, EXWM does not focus on it. This piece of code prevents this.
(advice-add #'exwm-layout--hide
:after (lambda (id)
(with-current-buffer (exwm--id->buffer id)
(setq exwm--ewmh-state
(delq xcb:Atom:_NET_WM_STATE_HIDDEN exwm--ewmh-state))
(exwm-layout--set-ewmh-state id)
(xcb:flush exwm--connection))))
Functions to shutdown and reboot the system
(defun efs/shutdown () (interactive) (org-save-all-org-buffers) (async-shell-command "shutdown -h now")) (defun efs/reboot () (interactive) (org-save-all-org-buffers) (async-shell-command "shutdown -r now"))
Mouse follows focus
(use-package exwm-mff)
(add-hook 'exwm-init-hook #'exwm-mff-mode)
Inner "Gaps"
(window-divider-mode 1) (setq window-divider-default-bottom-width 6) (setq window-divider-default-right-width 6) (menu-bar-bottom-and-right-window-divider)
EXWM allows switching to X windows in a different workspace.
(setq exwm-workspace-show-all-buffers 1) (setq exwm-layout-show-all-buffers 1)
Transparent emacs frames.
(set-frame-parameter (selected-frame) 'alpha '(80 . 80)) (add-to-list 'default-frame-alist '(alpha . (70 . 70)))
Update dot files.
(start-process-shell-command "update" nil "cd $HOME/.dot-files && git pull")
Battery Notifications
Id for critical notifications.
(defvar notification-id nil)
This variable is t if the battery was previously charging.
(defvar was-charging t)
This variable is t if the battery was previously fully charged.
(defvar was-full nil)
Notifications for different battery states
(defun battery-critical-notification (charge) (setq notification-id (notifications-notify :timeout 0 :urgency 'high :title (format "Battery level critical %d%%!" charge) :app-icon "/home/tiago/.dot-files/low-battery.png" :replaces-id notification-id))) (defun battery-charging-notification () (setq notification-id (notifications-notify :urgency 'medium :title "Battery charging!" :app-icon "/home/tiago/.dot-files/battery-charging.png" :replaces-id notification-id))) (defun battery-discharging-notification () (setq notification-id (notifications-notify :urgency 'medium :title "Battery discharging!" :app-icon "/home/tiago/.dot-files/battery-charging.png" :replaces-id notification-id))) (defun battery-charged-notification () (setq notification-id (notifications-notify :urgency 'medium :title "Battery charged!" :app-icon "/home/tiago/.dot-files/battery-charged.png" :replaces-id notification-id))) (defun is-charging (data) (equal (alist-get ?L data) "on-line")) (defun is-connected (data) (or (equal (alist-get ?L data) "N/A") (is-charging data))) (defun dcharge (data) (string-to-number (alist-get ?p data))) (defun critical-battery (data) (when (and (not (is-connected data)) (< (dcharge data) 10)) (battery-critical-notification (dcharge data)))) (defun battery-charging (data) (when (and was-charging (not (is-connected data))) (battery-discharging-notification)) (when (and (not was-charging) (is-charging data)) (battery-charging-notification)) (setq was-charging (is-connected data))) (defun battery-full (data) (if (and (eq (dcharge data) 100) (is-charging data)) (unless was-full (setq was-full t) (battery-charged-notification)) (setq was-full nil))) (add-hook 'exwm-init-hook (lambda () (setq battery-update-functions '(critical-battery battery-charging battery-full))))
Keybindings for desktop utilities
We use the desktop-environment package to help us change the volume,
adjust brightness, etc…
(use-package desktop-environment)
(desktop-environment-mode 1)
Disable the keybinding for locking the screen as we use this binding for window navigation
(define-key desktop-environment-mode-map (kbd "s-l") nil t)
Command for muting the volume
(setq desktop-environment-volume-toggle-command "amixer -D pulse set Master 1+ toggle")
Command for setting the volume
(setq desktop-environment-volume-set-command "~/.config/vol_set.sh %s")
Command for getting the current value of the volume
(setq desktop-environment-volume-get-command "amixer -D pulse get Master")
Command for screenshots
(setq desktop-environment-screenshot-directory "~/pictures")
Locking the screen also pauses any media
(setq desktop-environment-screenlock-command "~/.config/lock.sh")
Background processes
Helper function to run a program in the background
(defun efs/run-in-background (command) (let ((command-parts (split-string command "[ ]+"))) (apply #'call-process `(,(car command-parts) nil 0 nil ,@(cdr command-parts)))))
Sound display
(use-package volume)
Run applications after EXWM has initialized.
(defun startup-apps () (interactive) (efs/run-in-background "discord --start-minimized") (efs/run-in-background "dunst") (efs/run-in-background "picom")) (add-hook 'exwm-init-hook #'startup-apps)
Update config files
(start-process-shell-command "config" nil "~/.update.sh")
Auto-pause media when headphones are disconnected
(start-process-shell-command "autopause" nil "~/.config/autopause.sh")
Multiple monitors
Set the initial workspace for each display
(setq exwm-randr-workspace-monitor-plist '(1 "eDP-1" 2 "HDMI-1-0"))
Mouse warping
(setq exwm-workspace-warp-cursor t)
Focus follows mouse
(setq mouse-atuoselect-window t
focus-follows-mouse t)
Have autorandr running in the background to ensure that extra monitors are correctly configured.
(defun efs/update-displays () (efs/run-in-background "autorandr --change --force") (message "Display config: %s" (string-trim (shell-command-to-string "autorandr --current"))) (start-process-shell-command "feh" nil "feh --bg-scale ~/.dot-files/.config/bg/lain-hands.jpeg --bg-scale ~/.dot-files/.config/bg/lain.jpeg")) (add-hook 'exwm-randr-screen-change-hook #'efs/update-displays) (exwm-randr-mode 1)
Keybindings
Keybindings to switch the current workspace
(setq exwm-input-global-keys `(([?\s-r] . exwm-reset) ;; s-r: Reset (to line-mode). ([?\s-w] . exwm-workspace-switch) ;; s-w: Switch workspace. ([?\s-&] . (lambda (cmd) ;; s-&: Launch application. (interactive (list (read-shell-command "$ "))) (start-process-shell-command cmd nil cmd))) ;; s-N: Switch to certain workspace. ,@(mapcar (lambda (i) `(,(kbd (format "s-%d" i)) . (lambda () (interactive) (exwm-workspace-switch-create ,i)))) (number-sequence 0 9)))) (add-hook #'exwm-init-hook (lambda () (interactive) (exwm-workspace-switch-create 1)))
Kills the current buffer.
(exwm-input-set-key (kbd "s-c") 'kill-current-buffer)
Window movement
(exwm-input-set-key (kbd "s-l") 'windmove-right) (exwm-input-set-key (kbd "s-j") 'windmove-left) (exwm-input-set-key (kbd "s-i") 'windmove-up) (exwm-input-set-key (kbd "s-k") 'windmove-down)
Window management
(exwm-input-set-key (kbd "s-L") 'windmove-swap-states-right) (exwm-input-set-key (kbd "s-J") 'windmove-swap-states-left) (exwm-input-set-key (kbd "s-I") 'windmove-swap-states-up) (exwm-input-set-key (kbd "s-K") 'windmove-swap-states-down)
Start a desktop application using switch to buffer
(use-package xdg-launcher :vc (:url "https://github.com/emacs-exwm/xdg-launcher")) (with-eval-after-load 'consult (push 'xdg-launcher-consult-source (cdr (memq 'consult-source-buffer consult-buffer-sources))))
Suspend the computer
(exwm-input-set-key (kbd "s-<escape>") 'desktop-environment-lock-screen)
Open web browser
(defun run-firefox () (interactive) (efs/run-in-background "firefox")) (exwm-input-set-key (kbd "s-<return>") 'run-firefox)
Lists all of my firefox tabs
(defun list-firefox () (interactive) (minibuffer-with-setup-hook (lambda () (insert "firefox ")) (call-interactively #'consult-buffer))) (exwm-input-set-key (kbd "s-f") #'list-firefox)
Enable EXWM
I call scratch-buffer first so that each new workspace opens in a
scratch buffer. I then call server-start to turn the Emacs instance
into a daemon. This is so that when a program tries to open a text
editor, it can connect to the Emacs instance without reloading the
config. The call to exwm-wm-mode is what actually starts EXWM.
(scratch-buffer) (server-start) (exwm-wm-mode)
For some reason autorandr doesn't work on one of my monitors so I have to put this in.
(start-process-shell-command "aaa" nil "xrandr --output eDP-1 --auto --output HDMI-1-0 --auto --primary --above eDP-1")