opam and pack config

emacs/.config/emacs/Emacs.org

@@ -111,6 +111,28 @@
     (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
@@ -122,12 +144,26 @@
 #+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
@@ -287,11 +323,18 @@
   )
 #+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
@@ -305,7 +348,18 @@
 #+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,8 +10,9 @@ return {
     {
         'tomtomjhj/vscoq.nvim',
         event = { 'BufReadPre *.v', 'BufNewFile *.v'},
+        filetypes = 'coq',
         opts = true,
-        dependencies = { 'whonore/Coqtail' },
+        dependencies = { 'whonore/Coqtail', 'neovim/nvim-lspconfig' },
     }
     -- {
     --     'tomtomjhj/coq-lsp.nvim',

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

@@ -0,0 +1,30 @@
+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,6 +18,14 @@ 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,5 +82,18 @@ 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,6 +28,7 @@ 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"
@@ -37,3 +38,4 @@ 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,6 +44,9 @@ 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)"