{ pkgs, extra, ... }:
{
  programs.neovim = {
    defaultEditor = true;
    enable = true;
    vimAlias = true;
    extraLuaConfig = ''
      require('tmux').setup({ copy_sync = { redirect_to_clipboard = true } });
      require('Comment').setup()
      require('nvim-surround').setup()
      require('numb').setup()
      local lspcfg = require('lspconfig')
      lspcfg.typst_lsp.setup({
        cmd = { '${pkgs.typst-lsp}/bin/typst-lsp' },
      })
      lspcfg.rust_analyzer.setup({})
      lspcfg.hls.setup({})
      lspcfg.pyright.setup({
        cmd = { '${pkgs.nodePackages.pyright}/bin/pyright-langserver', '--stdio' },
      })
      lspcfg.nixd.setup({
        cmd = { '${pkgs.nixd}/bin/nixd' },
      })
      lspcfg.ltex.setup({
        cmd = { '${pkgs.ltex-ls}/bin/ltex-ls' },
        filetypes = { 'bib', 'gitcommit', 'markdown', 'plaintext', 'tex', 'pandoc', 'typst' },
        settings = {
          ltex = {
            language = 'auto'
          }
        }
      })
      lspcfg.clangd.setup({
        cmd = { '${pkgs.clang-tools}/bin/clangd' },
      })
      lspcfg.ocamllsp.setup({})
      lspcfg.purescriptls.setup({})
      require('orgmode').setup({})
      require('lean').setup({
        mappings = true,
      })
      require('lualine').setup {
        options = {
          icons_enabled = true,
          theme = 'gruvbox',
          component_separators = { left = "", right = ""},
          section_separators = { left = "", right = ""},
          always_divide_middle = true,
          globalstatus = false,
          refresh = {
            statusline = 1000,
            tabline = 1000,
            winbar = 1000,
          }
        },
        sections = {
          lualine_a = {'mode'},
          lualine_b = { { 
            'diagnostics', 
            always_visible = true,
            on_click = function(n,b,m)
              vim.diagnostic.goto_next()
            end
          } },
          lualine_c = {'filename'},
          lualine_x = {'encoding', 'filetype'},
          lualine_y = {'progress'},
          lualine_z = {'location'}
        },
        inactive_sections = {
          lualine_a = {},
          lualine_b = {},
          lualine_c = {'filename'},
          lualine_x = {'location'},
          lualine_y = {},
          lualine_z = {}
        },
      }

      vim.api.nvim_create_autocmd('LspAttach', {
        callback = function(args)
          local opts = { buffer = args.buf }
          vim.keymap.set('n', 'K', vim.lsp.buf.hover, opts)
          vim.keymap.set('n', '<localleader>r', vim.lsp.buf.rename, opts)
          vim.keymap.set('n', '<localleader>a', vim.lsp.buf.code_action, opts)
          vim.keymap.set('n', '<localleader>gd', vim.lsp.buf.definition, opts)
          vim.keymap.set('n', '<localleader>gi', vim.lsp.buf.implementation, opts)
          vim.keymap.set('n', '<localleader>gr', vim.lsp.buf.references, opts)
          vim.keymap.set('n', '<localleader>e', vim.diagnostic.open_float, opts)
          vim.keymap.set('n', '<localleader>n', vim.diagnostic.goto_next, opts)
          vim.keymap.set('n', '<localleader>N', vim.diagnostic.goto_prev, opts)
          vim.keymap.set('i', '<C-n>', vim.lsp.omnifunc, opts)
        end,
      })

      vim.api.nvim_create_autocmd({ "BufNew"
                                  , "TextChanged"
                                  , "TextChangedI"
                                  , "TextChangedP"
                                  , "TextChangedT"
                                  }, {
        callback = function(args)
          vim.diagnostic.disable(args.buf)
        end
      })

      vim.api.nvim_create_autocmd({"BufWrite"}, {
        callback = function(args)
          vim.diagnostic.enable(args.buf)
        end
      })
    '';
    extraConfig = ''
      set rnu nu
      set ts=2 sw=2 expandtab
      set clipboard=unnamedplus
      set laststatus=3 noshowmode
      set signcolumn=no
      set linebreak
      let g:cornelis_use_global_binary = 1
      set conceallevel=2 concealcursor=nc
      colorscheme gruvbox
      hi Normal guibg=NONE ctermbg=NONE

      let maplocalleader="!"
      let g:bqn_prefix_key="!"
      runtime agda-input.vim
      call cornelis#bind_input(" ", "!")
      call cornelis#bind_input("exc", "!")

      inoremap <C-Space> <Esc>

      nnoremap j gj
      nnoremap k gk
      nnoremap gj j
      nnoremap gk k

      au BufRead,BufNewFile *.agda call AgdaFiletype()
      au BufRead,BufNewFile *.lagda.* call AgdaFiletype()
      function! AgdaFiletype()
          nnoremap <buffer> <C-c><C-l> :CornelisLoad<CR>
          nnoremap <buffer> <C-c><C-r> :CornelisRefine<CR>
          nnoremap <buffer> <C-c><C-c> :CornelisMakeCase<CR>
          nnoremap <buffer> <C-c>,     :CornelisTypeContext<CR>
          nnoremap <buffer> <C-c>.     :CornelisTypeContextInfer<CR>
          nnoremap <buffer> <C-c><C-d> :CornelisTypeInfer<CR>
          nnoremap <buffer> <C-c><C-s> :CornelisSolve<CR>
          nnoremap <buffer> <C-c><C-a> :CornelisAuto<CR>
          nnoremap <buffer> gd         :CornelisGoToDefinition<CR>
          nnoremap <buffer> <C-c><C-b> :CornelisPrevGoal<CR>
          nnoremap <buffer> <C-c><C-f> :CornelisNextGoal<CR>
          nnoremap <buffer> <C-c><C-u> :CornelisIgnoreAbstract<CR>
          nnoremap <buffer> <C-c><space> :CornelisGive<CR>
      endfunction
    '';
    plugins = (with pkgs.vimPlugins; [
      nvim-surround
      comment-nvim
      vimtex
      gruvbox-nvim
      tmux-nvim
      nvim-lspconfig
      idris2-vim
      numb-nvim
      typst-vim
      orgmode
      vim-obsession
      lean-nvim
      lualine-nvim
    ]) ++ [
      extra.cornelis-vim
      extra.bqn-vim
      extra.bqn-nvim
    ];
  };
}