fish

fish/.config/fish/conf.d/nix.fish

@@ -0,0 +1,2 @@
+
+if test -e /home/wball/.nix-profile/etc/profile.d/nix.fish; . /home/wball/.nix-profile/etc/profile.d/nix.fish; end # added by Nix installer

fish/.config/fish/config.fish

@@ -30,10 +30,11 @@ fish_add_path $HOME/.local/share/rustup/toolchains/stable-x86_64-unknown-linux-g
 fish_add_path /usr/lib/smlnj/bin
 fish_add_path $HOME/.config/emacs/bin
 fish_add_path $HOME/.elan/bin
-fish_add_path $HOME/go/bin
+fish_add_path $HOME/.pack/bin
 
 # set some environment variables 
-set -x MANPAGER "sh -c 'col -bx | bat -l man -p'"
+#set -x MANPAGER "sh -c 'col -bx | bat -l man -p'"
+set -x MANPAGER "less -R --use-color -Dd+r -Du+b"
 set -x INPUTRC $HOME/.config/readline/inputrc
 set -x EDITOR nvim
 set -x VISUAL nvim
@@ -54,6 +55,8 @@ set -x JUPYTER_CONFIG_DIR $XDG_CONFIG_HOME/jupyter
 set -x RUSTUP_HOME $XDG_DATA_HOME/rustup
 set -x DOT_SAGE $XDG_CONFIG_HOME/sage
 set -x OCAMLPATH $HOME/.opam/default/lib
+set -x AGDA_DIR $HOME/.config/agda
+set -x MIZFILES $HOME/.local/share/mizar
 
 function vicd
     set dst "$(command vifm --choose-dir - $argv[2..-1])"
@@ -64,6 +67,8 @@ function vicd
     cd "$dst"
 end
 
-eval (opam env --switch=default)
+eval (opam env)
+
+eval (direnv hook fish)
 
 set -q GHCUP_INSTALL_BASE_PREFIX[1]; or set GHCUP_INSTALL_BASE_PREFIX $HOME ; set -gx PATH $HOME/.cabal/bin $PATH /home/wball/.local/bin # ghcup-env

fish/.config/fish/fish_variables

@@ -12,15 +12,15 @@ SETUVAR _fisher_jorgebucaran_2F_fisher_files:\x7e/\x2econfig/fish/functions/fish
 SETUVAR _fisher_patrickf1_2F_fzf_2E_fish_files:\x7e/\x2econfig/fish/functions/_fzf_configure_bindings_help\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_extract_var_info\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_preview_changed_file\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_preview_file\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_report_diff_type\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_report_file_type\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_search_directory\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_search_git_log\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_search_git_status\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_search_history\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_search_processes\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_search_variables\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_wrapper\x2efish\x1e\x7e/\x2econfig/fish/functions/fzf_configure_bindings\x2efish\x1e\x7e/\x2econfig/fish/conf\x2ed/fzf\x2efish\x1e\x7e/\x2econfig/fish/completions/fzf_configure_bindings\x2efish
 SETUVAR _fisher_plugins:jorgebucaran/fisher\x1ejethrokuan/z\x1epatrickf1/fzf\x2efish
 SETUVAR _fisher_upgraded_to_4_4:\x1d
-SETUVAR fish_color_autosuggestion:brblack
+SETUVAR fish_color_autosuggestion:8e908c
 SETUVAR fish_color_cancel:\x2d\x2dreverse
-SETUVAR fish_color_command:blue
-SETUVAR fish_color_comment:red
+SETUVAR fish_color_command:8959a8
+SETUVAR fish_color_comment:eab700
 SETUVAR fish_color_cwd:green
 SETUVAR fish_color_cwd_root:red
-SETUVAR fish_color_end:green
-SETUVAR fish_color_error:brred
-SETUVAR fish_color_escape:brcyan
+SETUVAR fish_color_end:8959a8
+SETUVAR fish_color_error:c82829
+SETUVAR fish_color_escape:00a6b2
 SETUVAR fish_color_gray:6c7086
 SETUVAR fish_color_history_current:\x2d\x2dbold
 SETUVAR fish_color_host:normal
@@ -28,11 +28,11 @@ SETUVAR fish_color_host_remote:\x1d
 SETUVAR fish_color_keyword:\x1d
 SETUVAR fish_color_match:\x2d\x2dbackground\x3dbrblue
 SETUVAR fish_color_normal:normal
-SETUVAR fish_color_operator:brcyan
+SETUVAR fish_color_operator:00a6b2
 SETUVAR fish_color_option:\x1d
-SETUVAR fish_color_param:cyan
-SETUVAR fish_color_quote:yellow
-SETUVAR fish_color_redirection:cyan\x1e\x2d\x2dbold
+SETUVAR fish_color_param:4271ae
+SETUVAR fish_color_quote:718c00
+SETUVAR fish_color_redirection:3e999f
 SETUVAR fish_color_search_match:bryellow\x1e\x2d\x2dbackground\x3dbrblack
 SETUVAR fish_color_selection:white\x1e\x2d\x2dbold\x1e\x2d\x2dbackground\x3dbrblack
 SETUVAR fish_color_status:f38ba8
@@ -41,16 +41,16 @@ SETUVAR fish_color_valid_path:\x2d\x2dunderline
 SETUVAR fish_key_bindings:fish_hybrid_key_bindings
 SETUVAR fish_pager_color_background:\x1d
 SETUVAR fish_pager_color_completion:normal
-SETUVAR fish_pager_color_description:yellow\x1e\x2d\x2ditalics
+SETUVAR fish_pager_color_description:B3A06D
 SETUVAR fish_pager_color_prefix:normal\x1e\x2d\x2dbold\x1e\x2d\x2dunderline
 SETUVAR fish_pager_color_progress:brwhite\x1e\x2d\x2dbackground\x3dcyan
 SETUVAR fish_pager_color_secondary_background:\x1d
 SETUVAR fish_pager_color_secondary_completion:\x1d
 SETUVAR fish_pager_color_secondary_description:\x1d
 SETUVAR fish_pager_color_secondary_prefix:\x1d
-SETUVAR fish_pager_color_selected_background:\x2d\x2dreverse
+SETUVAR fish_pager_color_selected_background:\x2d\x2dbackground\x3dbrblack
 SETUVAR fish_pager_color_selected_completion:\x1d
 SETUVAR fish_pager_color_selected_description:\x1d
 SETUVAR fish_pager_color_selected_prefix:\x1d
-SETUVAR fish_user_paths:/usr/lib/smlnj/bin\x1e/home/wball/go/bin\x1e/home/wball/\x2eelan/bin\x1e/home/wball/\x2econfig/emacs/bin\x1e/home/wball/j9\x2e5/bin\x1e/home/wball/\x2elocal/smlnj/bin\x1e/home/wball/\x2elocal/share/rustup/toolchains/stable\x2dx86_64\x2dunknown\x2dlinux\x2dgnu/bin\x1e/home/wball/code/j/j9\x2e4/bin\x1e/usr/lib/j9/bin\x1e/home/wball/\x2ecabal/bin\x1e/home/wball/\x2eghcup/bin\x1e/home/wball/\x2elocal/share/cargo/bin\x1e/home/wball/\x2elocal/bin\x1e/home/wball/\x2ecargo/bin\x1e/home/wball/\x2escripts
+SETUVAR fish_user_paths:/home/wball/\x2epack/bin\x1e/usr/lib/smlnj/bin\x1e/home/wball/go/bin\x1e/home/wball/\x2eelan/bin\x1e/home/wball/\x2econfig/emacs/bin\x1e/home/wball/j9\x2e5/bin\x1e/home/wball/\x2elocal/smlnj/bin\x1e/home/wball/\x2elocal/share/rustup/toolchains/stable\x2dx86_64\x2dunknown\x2dlinux\x2dgnu/bin\x1e/home/wball/code/j/j9\x2e4/bin\x1e/usr/lib/j9/bin\x1e/home/wball/\x2ecabal/bin\x1e/home/wball/\x2eghcup/bin\x1e/home/wball/\x2elocal/share/cargo/bin\x1e/home/wball/\x2elocal/bin\x1e/home/wball/\x2ecargo/bin\x1e/home/wball/\x2escripts
 SETUVAR grc_plugin_execs:cat\x1ecvs\x1edf\x1ediff\x1edig\x1egcc\x1eg\x2b\x2b\x1els\x1eifconfig\x1emake\x1emount\x1emtr\x1enetstat\x1eping\x1eps\x1etail\x1etraceroute\x1ewdiff\x1eblkid\x1edu\x1ednf\x1edocker\x1edocker\x2dcompose\x1edocker\x2dmachine\x1eenv\x1eid\x1eip\x1eiostat\x1ejournalctl\x1ekubectl\x1elast\x1elsattr\x1elsblk\x1elspci\x1elsmod\x1elsof\x1egetfacl\x1egetsebool\x1eulimit\x1euptime\x1enmap\x1efdisk\x1efindmnt\x1efree\x1esemanage\x1esar\x1ess\x1esysctl\x1esystemctl\x1estat\x1eshowmount\x1etcpdump\x1etune2fs\x1evmstat\x1ew\x1ewho\x1esockstat

nvim/.config/nvim/lua/options.lua

@@ -23,6 +23,10 @@ opt.conceallevel = 2
 opt.breakindent = true
 opt.linebreak = true
 
+opt.foldmethod = 'marker'
+-- opt.foldmethod = 'expr'
+-- opt.foldexpr = 'nvim_treesitter#foldexpr()'
+
 vim.api.nvim_create_autocmd('TermOpen', {
     pattern = '*',
     callback = function()

nvim/.config/nvim/lua/plugins/keys.lua

@@ -3,21 +3,14 @@ return {
         'folke/which-key.nvim',
         event = 'VeryLazy',
         config = function()
-            -- set up groups
+            -- set up some groups
             local wk = require('which-key')
             wk.add({
                 { '<leader>f', group = 'find' },
                 { '<leader>h', group = 'help' },
+                { '<leader>e', group = 'explore' },
+                { '<leader>ee', ':Lexplore<CR>', desc='netrw cwd' },
             })
         end,
-        keys = {
-            {
-                "<leader>?",
-                function()
-                    require("which-key").show({ global = false })
-                end,
-                desc = "Buffer Local Keymaps (which-key)",
-            },
-        },
     }
 }

nvim/.config/nvim/lua/plugins/languages/agda.lua

@@ -0,0 +1,10 @@
+return {
+    {
+        'isovector/cornelis',
+        dependencies = {
+            'kana/vim-textobj-user',
+            'neovimhaskell/nvim-hs.vim',
+        },
+        build = 'stack build',
+    }
+}

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

@@ -5,14 +5,21 @@ return {
         init = function()
             vim.g.loaded_coqtail = 1
             vim.g['coqtail#supported'] = 0
+            vim.cmd([[call digraph_set('|-', '⊢')]])
         end
     },
     {
-        'tomtomjhj/coq-lsp.nvim',
+        'tomtomjhj/vscoq.nvim',
         event = { 'BufReadPre *.v', 'BufNewFile *.v'},
-        opts = {
-            autostart = true,
-        },
-        dependencies = { 'whonore/Coqtail' }
+        opts = true,
+        dependencies = { 'whonore/Coqtail' },
     }
+    -- {
+    --     'tomtomjhj/coq-lsp.nvim',
+    --     event = { 'BufReadPre *.v', 'BufNewFile *.v' },
+    --     opts = {
+    --         autostart = true,
+    --     },
+    --     dependencies = { 'whonore/Coqtail' }
+    -- }
 }

nvim/.config/nvim/lua/plugins/languages/idris.lua

@@ -0,0 +1,80 @@
+return {
+    {
+        'ShinKage/idris2-nvim',
+        event = { 'BufReadPre *.idr', 'BufNewFile *.idr' },
+        dependencies = {
+            'neovim/nvim-lspconfig',
+            'MunifTanjim/nui.nvim',
+            'folke/which-key.nvim'
+        },
+        config = function()
+            local wk = require('which-key')
+            local action = require('idris2.code_action')
+            local hover = require('idris2.hover')
+            local meta = require('idris2.metavars')
+            local browse = require('idris2.browse')
+            local repl = require('idris2.repl')
+
+            require('idris2').setup({
+                client = {
+                    hover = {
+                        use_split = false,
+                        split_size = '30%',
+                        auto_resize_split = false,
+                        split_position = 'bottom',
+                        with_history = true,
+                    },
+                },
+                autostart_semantic = true,
+                code_action_post_hook = save_hook,
+                use_default_semantic_hl_groups = true,
+                server = {
+                    init_options = {
+                        logFile = "~/.cache/idris2-lsp/server.log",
+                        longActionTimeout = 2000,
+                    },
+                    on_attach = function(...)
+                        wk.add({
+                            { '<leader>c', action.case_split, desc = 'Split case' },
+
+                            { '<leader>i', group = 'idris action' },
+                            { '<leader>ic', action.make_case, desc = 'Make case' },
+                            { '<leader>iw', action.make_with, desc = 'Make with' },
+                            { '<leader>il', action.make_lemma, desc = 'Make lemma' },
+                            { '<leader>ia', action.add_clause, desc = 'Add clause' },
+                            { '<leader>io', action.expr_search, desc = 'Expr search' },
+                            { '<leader>ig', action.generate_def, desc = 'Generate definition' },
+                            { '<leader>ir', action.refine_hole, desc = 'Refine hole' },
+                            { '<leader>ib', browse.browse, desc = 'Browse' },
+
+                            { '<leader>s', group = 'idris split' },
+                            { '<leader>so', hover.open_split, desc = 'Open' },
+                            { '<leader>sc', hover.close_split, desc = 'Close' },
+
+                            { '<leader>m', group = 'idris metavariables' },
+                            { '<leader>mm', meta.request_all, desc = 'Request all' },
+                            { '<leader>mn', meta.goto_next, desc = 'Next' },
+                            { '<leader>mp', meta.goto_prev, desc = 'Previous' },
+
+                            { '<leader>e', group = 'idris evaluate' },
+                            { '<leader>ee', repl.evaluate, desc = 'Expression' },
+                            {
+                                '<leader>ev',
+                                function() repl.evaluate({ visual = true}) end,
+                                desc = 'Visual selection',
+                                mode = 'v',
+                                group = 'idris evaluate'
+                            },
+                            {
+                                '<leader>er',
+                                function() repl.evaluate({ visual = true, sub = true}) end,
+                                desc = 'Replace selection',
+                                mode = 'v'
+                            },
+                        })
+                    end
+                }
+            })
+        end
+    }
+}

nvim/.config/nvim/lua/plugins/languages/mizar.lua

@@ -0,0 +1,5 @@
+return {
+    {
+        'andy-morris/mizar.vim',
+    }
+}

nvim/.config/nvim/lua/plugins/languages/perga.lua

@@ -0,0 +1,7 @@
+return {
+    {
+        -- "https://forgejo.ballcloud.cc/wball/perga.nvim",
+        url = "/home/wball/repos/perga.nvim",
+        config = true,
+    },
+}

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

@@ -13,10 +13,14 @@ return {
             vim.api.nvim_create_autocmd('LspAttach', {
                 group = vim.api.nvim_create_augroup('UserLspConfig', {}),
                 callback = function(ev)
+                    local builtin = require('telescope.builtin')
                     wk.add({
                         { 'gD', vim.lsp.buf.declaration, desc = 'Go to declaration' },
+                        { 'gR', builtin.lsp_references, desc = 'Go to references' },
+                        { 'gd', builtin.lsp_definitions, desc = 'Go to definition' },
 
-                        { '<leader>la', vim.lsp.buf.code_action, desc = 'See available code actions' },
+                        { '<leader>l', group = 'lsp' },
+                        { '<leader>la', vim.lsp.buf.code_action, desc = 'Code actions' },
                         { '<leader>lr', vim.lsp.buf.rename, desc = 'Rename' },
                         { '<leader>lf', vim.lsp.buf.format, desc = 'Format' },
                         { '<leader>le', vim.diagnostic.open_float, desc = 'Show line diagnostics' },

nvim/.config/nvim/lua/plugins/telescope.lua

@@ -25,52 +25,52 @@ return {
             {
                 "<leader>ff",
                 require('telescope.builtin').find_files,
-                desc = 'Telescope find files'
+                desc = 'find files'
             },
             {
                 "<leader>fg",
                 require('telescope.builtin').live_grep,
-                desc = 'Telescope live grep'
+                desc = 'live grep'
             },
             {
                 "<leader>fb",
                 require('telescope.builtin').buffers,
-                desc = 'Telescope buffers'
+                desc = 'buffers'
             },
             {
                 "<leader>fh",
                 require('telescope.builtin').help_tags,
-                desc = 'Telescope help tags'
+                desc = 'help tags'
             },
             {
                 "<leader>fo",
                 require('telescope.builtin').oldfiles,
-                desc = 'Telescope old files'
+                desc = 'old files'
             },
             {
                 "<leader>fc",
                 require('telescope.builtin').commands,
-                desc = 'Telescope commands'
+                desc = 'commands'
             },
             {
                 "<leader>fm",
                 require('telescope.builtin').marks,
-                desc = 'Telescope marks'
+                desc = 'marks'
             },
             {
                 "<leader>fq",
                 require('telescope.builtin').quickfix,
-                desc = 'Telescope quickfix'
+                desc = 'quickfix'
             },
             {
                 "<leader>fl",
                 require('telescope.builtin').loclist,
-                desc = 'Telescope loclist'
+                desc = 'loclist'
             },
             {
                 "<leader>fr",
                 require('telescope.builtin').registers,
-                desc = 'Telescope registers'
+                desc = 'registers'
             },
         }
     },

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

@@ -23,8 +23,8 @@ return {
             local neogit = require('neogit')
             wk.add({
                 { '<leader>g', group = 'git' },
-                { '<leader>gn', neogit.open, desc = 'Neogit' },
-                { '<leader>gd', ':DiffviewOpen<CR>', desc = 'Diffview' },
+                { '<leader>gn', neogit.open, desc = 'neogit' },
+                { '<leader>gd', ':DiffviewOpen<CR>', desc = 'diffview' },
             })
             neogit.setup({})
         end,
@@ -51,5 +51,36 @@ return {
 
             cmp.event:on('confirm_done', cmp_autopairs.on_confirm_done())
         end
+    },
+    {
+        'akinsho/toggleterm.nvim',
+        version = '*',
+        event = 'VeryLazy',
+        opts = {
+            open_mapping = [[<C-\>]]
+        }
+    },
+    {
+        'numToStr/Navigator.nvim',
+        config = function()
+            local navigator = require('Navigator')
+            vim.keymap.set({'n', 't'}, '<A-h>', navigator.left)
+            vim.keymap.set({'n', 't'}, '<A-j>', navigator.down)
+            vim.keymap.set({'n', 't'}, '<A-k>', navigator.up)
+            vim.keymap.set({'n', 't'}, '<A-l>', navigator.right)
+            vim.keymap.set({'n', 't'}, '<A-p>', navigator.previous)
+            navigator.setup()
+        end
+    },
+    {
+        'echasnovski/mini.align',
+        version = false,
+        opts = {
+            -- modifiers = {
+            --     i = function(steps, _)
+            --         table.insert(steps.pre_split, align.gen_step.ignore_split({ '".-"', "'.-'", '(.-)' }))
+            --     end
+            -- }
+        }
     }
 }