emacs/.config/emacs/Emacs.org

@@ -111,28 +111,6 @@
     (fontaine-set-preset 'regular))
 #+end_src
 
-** Ligatures
-#+begin_src emacs-lisp
-  (use-package ligature
-    :config
-    (ligature-set-ligatures 't '("www"))
-    (ligature-set-ligatures 'eww-mode '("ff" "fi" "ffi"))
-    (ligature-set-ligatures 'prog-mode '("|||>" "<|||" "<==>" "<!--" "####" "~~>" "***" "||=" "||>"
-                                         ":::" "::=" "=:=" "===" "==>" "=!=" "=>>" "=<<" "=/=" "!=="
-                                         "!!." ">=>" ">>=" ">>>" ">>-" ">->" "->>" "-->" "---" "-<<"
-                                         "<~~" "<~>" "<*>" "<||" "<|>" "<$>" "<==" "<=>" "<=<" "<->"
-                                         "<--" "<-<" "<<=" "<<-" "<<<" "<+>" "</>" "###" "#_(" "..<"
-                                         "..." "+++" "/==" "///" "_|_" "www" "&&" "^=" "~~" "~@" "~="
-                                         "~>" "~-" "**" "*>" "*/" "||" "|}" "|]" "|=" "|>" "|-" "{|"
-                                         "[|" "]#" "::" ":=" ":>" ":<" "$>" "==" "=>" "!=" "!!" ">:"
-                                         ">=" ">>" ">-" "-~" "-|" "->" "--" "-<" "<~" "<*" "<|" "<:"
-                                         "<$" "<=" "<>" "<-" "<<" "<+" "</" "#{" "#[" "#:" "#=" "#!"
-                                         "##" "#(" "#?" "#_" "%%" ".=" ".-" ".." ".?" "+>" "++" "?:"
-                                         "?=" "?." "??" ";;" "/*" "/=" "/>" "//" "__" "~~" "(*" "*)"
-                                         "\\\\" "://"))
-    (global-ligature-mode t))
-#+end_src
-
 ** Which key
 #+begin_src emacs-lisp
   (use-package which-key
@@ -144,26 +122,12 @@
 #+end_src
 
 ** Theme
-*** Catppuccin
 #+begin_src emacs-lisp
   (use-package catppuccin-theme
     :config
     (load-theme 'catppuccin :no-confirm))
 #+end_src
-*** Modus Themes
+
-#+begin_src emacs-lisp
-  ;; (use-package emacs
-  ;;   :config
-  ;;   (require-theme 'modus-themes)
-  ;;   (setq modus-themes-italic-constructs t
-  ;; 	modus-themes-bold-constructs t
-  ;; 	modus-themes-links '(no-underline background faint)
-  ;; 	modus-themes-prompts '(bold intense)
-  ;; 	modus-themes-mode-line '(borderless accented moody)
-  ;; 	modus-themes-org-blocks 'gray-background
-  ;; 	modus-themes-region '(bg-only no-extend))
-  ;;   (modus-themes-load-operandi))
-#+end_src
 * Completion
 
 ** Vertico
@@ -323,18 +287,11 @@
   )
 #+end_src
 
-* Lsp
-I'm not a fan of =lsp-mode=, but =lean4-mode= requires it as a dependency, so I might as well actually install it.
-#+begin_src emacs-lisp
-  (use-package lsp-ui)
-  (use-package lsp-mode)
-#+end_src
-
 * Languages
 ** Agda
 #+begin_src emacs-lisp
- (load-file (let ((coding-system-for-read 'utf-8))
+;  (load-file (let ((coding-system-for-read 'utf-8))
-                 (shell-command-to-string "agda-mode locate")))
+;                  (shell-command-to-string "agda-mode locate")))
 #+end_src
 
 ** Idris
@@ -348,18 +305,7 @@ I'm not a fan of =lsp-mode=, but =lean4-mode= requires it as a dependency, so I
 #+begin_src emacs-lisp
   (use-package haskell-mode)
 #+end_src
-** PG
+
-#+begin_src emacs-lisp
-  (use-package proof-general)
-#+end_src
-** Lean
-#+begin_src emacs-lisp
-  (use-package lean4-mode
-    :commands lean4-mode
-    :straight (lean4-mode :type git :host github
-                          :repo "leanprover-community/lean4-mode"
-                          :files ("*.el" "data")))
-#+end_src
 * Latex
 
 ** Auctex

nvim/.config/nvim/lua/plugins/languages/coq.lua

@@ -10,9 +10,8 @@ return {
     {
         'tomtomjhj/vscoq.nvim',
         event = { 'BufReadPre *.v', 'BufNewFile *.v'},
-        filetypes = 'coq',
         opts = true,
-        dependencies = { 'whonore/Coqtail', 'neovim/nvim-lspconfig' },
+        dependencies = { 'whonore/Coqtail' },
     }
     -- {
     --     'tomtomjhj/coq-lsp.nvim',

nvim/.config/nvim/lua/plugins/languages/sml.lua

@@ -1,30 +0,0 @@
-return {
-    {
-        'jez/vim-better-sml',
-        config = function()
-            vim.g.sml_smlnj_executable = 'smlnj'
-        end,
-        keys = {
-            {
-                '<leader>rs',
-                [[:SMLReplStart<CR>]],
-                desc = 'SML start repl'
-            },
-            {
-                '<leader>rc',
-                [[:SMLReplClear<CR>]],
-                desc = 'SML clear repl'
-            },
-            {
-                '<leader>rb',
-                [[:SMLReplBuild<CR>]],
-                desc = 'SML load current file/CM project in repl'
-            },
-            {
-                '<leader>ro',
-                [[:SMLReplOpen<CR>]],
-                desc = 'SML open current structure in repl'
-            },
-        }
-    }
-}

nvim/.config/nvim/lua/plugins/lsp.lua

@@ -18,14 +18,6 @@ return {
                 }
             })
 
-            lspconfig.millet.setup({
-                root_dir = function(fname)
-                    local util = require("lspconfig.util")
-                    return util.root_pattern(".cm", ".mlb")(fname)
-                        or util.path.dirname(fname)
-                end
-            })
-
             vim.api.nvim_create_autocmd('LspAttach', {
                 group = vim.api.nvim_create_augroup('UserLspConfig', {}),
                 callback = function(ev)

nvim/.config/nvim/lua/plugins/utils.lua

@@ -82,18 +82,5 @@ return {
             --     end
             -- }
         }
-    },
-    {
-        'stevearc/conform.nvim',
-        opts = {
-            formatters_by_ft = {
-                rust = { 'rustfmt', lsp_format = 'fallback' },
-                sml = { 'smlfmt' },
-            },
-            format_on_save = {
-                timeout_ms = 500,
-                lsp_format = 'fallback',
-            }
-        }
     }
 }

zsh/.config/zsh/.zprofile

@@ -28,7 +28,6 @@ export CARGO_HOME="$XDG_DATA_HOME/cargo"
 export GPG_TTY="$(tty)"
 export STACK_XDG=1
 export GHCUP_USE_XDG_DIRS=true
-export OPAMROOT="$XDG_DATA_HOME/opam"
 export JULIA_DEPOT_PATH="$XDG_DATA_HOME/julia:$JULIA_DEPOT_PATH"
 export JUPYTER_CONFIG_DIR="$XDG_CONFIG_HOME/jupyter"
 export RUSTUP_HOME="$XDG_DATA_HOME/rustup"
@@ -38,4 +37,3 @@ export AGDA_DIR="$HOME/.config/agda"
 export PACK_DIR="$HOME/.local/share/pack"
 export MIZFILES="$HOME/.local/share/mizar"
 export RLWRAP_HOME="$XDG_DATA_HOME/rlwrap"
-export PACK_DIR="$XDG_DATA_HOME/pack"

zsh/.config/zsh/.zshrc

@@ -44,9 +44,6 @@ zstyle ':completion:*' matcher-list 'm:{a-zA-Z}={A-Za-z}'
 source /usr/share/zsh/plugins/zsh-syntax-highlighting/zsh-syntax-highlighting.zsh
 source /usr/share/zsh/plugins/zsh-autosuggestions/zsh-autosuggestions.zsh
 
-# setup ocaml stuff
-[[ ! -r '/home/wball/.local/share/opam/opam-init/init.zsh' ]] || source '/home/wball/.local/share/opam/opam-init/init.zsh' > /dev/null 2> /dev/null
-
 # zoxide
 eval "$(zoxide init zsh)"