Support for simultaneous lean3/lean4 (in separate windows/tabs)

README.rst

@@ -11,17 +11,18 @@ Prerequisites
 ``lean.nvim`` currently requires `neovim 0.5 HEAD / nightly
 <https://github.com/neovim/neovim/releases/tag/nightly>`_.
 
-For syntax highlighting and basic language support, you should either:
+NOTE: ``lean.nvim`` is incompatible with `lean.vim <https://github.com/leanprover/lean.vim>`_,
+as it implements its own kind filetype detection. 
+You should NOT have ``lean.vim`` installed if using ``lean.nvim``.
 
-    * Install the normal `lean.vim <https://github.com/leanprover/lean.vim>`_.
+For lean4 syntax highlighting and basic language support, you should
+try the experimental support present via `tree-sitter-lean
+<https://github.com/Julian/tree-sitter-lean>`_ by installing
+`nvim-treesitter <https://github.com/nvim-treesitter/nvim-treesitter>`_
 
-    * or try the experimental support present via `tree-sitter-lean
-      <https://github.com/Julian/tree-sitter-lean>`_ by installing
-      `nvim-treesitter <https://github.com/nvim-treesitter/nvim-treesitter>`_
-
-       Note that many simple syntactical things are not yet implemented
-       (help is of course welcome), and that ``tree-sitter-lean`` is lean
-       4-only.
+Note that many simple syntactical things are not yet implemented
+(help is of course welcome), and that ``tree-sitter-lean`` is lean
+4-only.
 
 Installation
 ------------
@@ -88,12 +89,32 @@ Configuration & Usage
 In e.g. your ``init.lua``:
 
 .. code-block:: lua
+      on_attach = function(client, bufnr)
+        -- See https://github.com/neovim/nvim-lspconfig#keybindings-and-completion
+        -- for detailed examples of what you may want to do here.
+        --
+        -- Mapping a key (typically K) to `vim.lsp.buf.hover()`
+        -- is highly recommended for Lean, since the hover LSP command
+        -- is where you'll see the current goal state.
+        --
+        -- You may furthermore want to add an `autocmd` to run it on
+        -- `CursorHoldI`, which will show the goal state any time the
+        -- cursor is unmoved in insert mode.
+        --
+        -- In the future, this plugin may offer a recommended "complete
+        -- setup" for easy enabling of the above.
+        local function buf_set_keymap(...) vim.api.nvim_buf_set_keymap(bufnr, ...) end
+        local function buf_set_option(...) vim.api.nvim_buf_set_option(bufnr, ...) end
+        buf_set_keymap('n', 'gd', '<Cmd>lua vim.lsp.buf.definition()<CR>', {noremap = true})
+        buf_set_keymap('n', 'K', '<Cmd>lua vim.lsp.buf.hover()<CR>', {noremap = true})
+        buf_set_option('omnifunc', 'v:lua.vim.lsp.omnifunc')
+    end
 
     require('lean').setup{
         -- Enable abbreviation support?
         --
         -- false to disable, otherwise a table of options described below
-        abbreviations = {,
+        abbreviations = {
             extra = {
                 -- Add a \wknight abbreviation to insert ♘
                 --
@@ -102,7 +123,7 @@ In e.g. your ``init.lua``:
                 -- this if so desired.
                 wknight = '♘',
             },
-        }
+        },
         -- Enable suggested mappings?
         --
         -- false by default, true to enable
@@ -112,35 +133,22 @@ In e.g. your ``init.lua``:
             -- Clip the infoview to a maximum width
             max_width = 79,
         },
-        -- Enable the Lean language server?
+        -- Enable the Lean3/Lean4 language servers?
         --
         -- false to disable, otherwise should be a table of options to pass to
         --  `leanls`. See https://github.com/neovim/nvim-lspconfig/blob/master/CONFIG.md#leanls
         -- for details though lean-language-server actually doesn't support all
         -- the options mentioned there yet.
         lsp = {
-            on_attach = function(client, bufnr)
-                -- See https://github.com/neovim/nvim-lspconfig#keybindings-and-completion
-                -- for detailed examples of what you may want to do here.
-                --
-                -- Mapping a key (typically K) to `vim.lsp.buf.hover()`
-                -- is highly recommended for Lean, since the hover LSP command
-                -- is where you'll see the current goal state.
-                --
-                -- You may furthermore want to add an `autocmd` to run it on
-                -- `CursorHoldI`, which will show the goal state any time the
-                -- cursor is unmoved in insert mode.
-                --
-                -- In the future, this plugin may offer a recommended "complete
-                -- setup" for easy enabling of the above.
-                local function buf_set_keymap(...) vim.api.nvim_buf_set_keymap(bufnr, ...) end
-                local function buf_set_option(...) vim.api.nvim_buf_set_option(bufnr, ...) end
-                buf_set_keymap('n', 'gd', '<Cmd>lua vim.lsp.buf.definition()<CR>', {noremap = true})
-                buf_set_keymap('n', 'K', '<Cmd>lua vim.lsp.buf.hover()<CR>', {noremap = true})
-                buf_set_option('omnifunc', 'v:lua.vim.lsp.omnifunc')
-            end,
+            on_attach = on_attach,
             cmd = {"lean-language-server", "--stdio", '--', "-M", "4096"},
         }
+
+        -- replace the path below with a path to your Lean4 executable
+        lsp4 = {
+            on_attach = on_attach,
+            cmd = {"/path/to/lean4/executable/lean", "--server"},
+        }
     }
 
 If you're using an ``init.vim``-only configuration setup, simply surround the

ftdetect/lean.vim

@@ -1 +1 @@
-autocmd BufRead,BufNewFile *.lean lua require'lean.lean3'.detect()
+autocmd BufRead,BufNewFile *.lean lua require'lean.ft'.detect(); require'lean.lean3'.detect()

ftplugin/lean/lean.vim

@@ -0,0 +1,31 @@
+if exists('b:did_ftplugin')
+  finish
+endif
+let b:did_ftplugin = 1
+
+set wildignore+=*.olean
+
+setlocal iskeyword=@,48-57,_,-,!,#,$,%
+
+setlocal comments=s0:/-,mb:\ ,ex:-/,:--
+setlocal commentstring=/-\ %s\ -/
+
+setlocal expandtab
+setlocal shiftwidth=2
+setlocal softtabstop=2
+
+function! lean#dotted2path(fname)
+  return substitute(a:fname, '\.', '/', 'g') . '.lean'
+endfunction
+setlocal includeexpr=lean#dotted2path(v:fname)
+
+setlocal matchpairs+=⟨:⟩
+
+" Matchit support
+if exists('loaded_matchit') && !exists('b:match_words')
+  let b:match_ignorecase = 0
+
+  let b:match_words =
+        \  '\<begin\>:\<end$' .
+        \ ',\<\%(namespace\|section\)\s\+\(.\{-}\)\>:\<end\s\+\1\>'
+endif

ftplugin/lean4/infoview.vim

@@ -0,0 +1,2 @@
+" required for infoview
+setlocal updatetime=100

ftplugin/lean4/switch.vim

@@ -0,0 +1,39 @@
+" This possibly belongs in lean.vim or switch.vim itself but putting it here
+" for now.
+
+if !exists("g:loaded_switch")
+  finish
+endif
+
+let b:switch_definitions = [
+    \ g:switch_builtins.true_false,
+    \ ["#check", "#eval", "#reduce"],
+    \ ["tidy", "suggest", "hint", "linarith", "library_search"],
+    \ ["rw", "simp", "simp?"],
+    \ ["cases", "rcases", "obtain"],
+    \ ["norm_cast", "push_cast"],
+    \ ["inl", "inr"],
+    \ ["tt", "ff"],
+    \ ["=", "≠"],
+    \ ["∈", "∉"],
+    \ ["∪", "∩"],
+    \ ["⋃", "⋂"],
+    \ ["⊆", "⊂", "⊃", "⊇"],
+    \ ["Σ", "∑"],
+    \ ["∀", "∃"],
+    \ ["∧", "∨"],
+    \ ["⊔", "⊓"],
+    \ ["⊥", "⊤"],
+    \ ["⋀", "⋁"],
+    \ ["×", "→"],
+    \ ["0", "₀", "⁰"],
+    \ ["1", "₁", "¹"],
+    \ ["2", "₂", "²"],
+    \ ["3", "₃", "³"],
+    \ ["4", "₄", "⁴"],
+    \ ["5", "₅", "⁵"],
+    \ ["6", "₆", "⁶"],
+    \ ["7", "₇", "⁷"],
+    \ ["8", "₈", "⁸"],
+    \ ["9", "₉", "⁹"],
+\ ]

indent/lean.vim

@@ -0,0 +1,6 @@
+if exists("b:did_indent")
+  finish
+endif
+let b:did_indent = 1
+
+setlocal indentkeys+==end,==begin

lua/lean/ft.lua

@@ -0,0 +1,21 @@
+local util = require'lean.util'
+
+-- Ideally this obviously would use a TOML parser but yeah choosing to
+-- do nasty things and not add the dependency for now.
+local _MARKER = '.*lean_version.*\".*lean4.*'
+
+local M = {}
+
+-- If a TOML file with a lean4 version string is found, use filetype "lean4".
+-- Otherwise use "lean" (lean3).
+function M.detect()
+  local toml_file = util.find_toml(vim.api.nvim_buf_get_name(0))
+  if not toml_file then vim.bo.ft = "lean" return end
+  local _, result = pcall(vim.fn.readfile, toml_file)
+  for _, line in ipairs(result) do
+    if line:match(_MARKER) then vim.bo.ft = "lean4" return end
+  end
+  vim.bo.ft = "lean"
+end
+
+return M

lua/lean/infoview.lua

@@ -1,6 +1,6 @@
 local lean3 = require('lean.lean3')
 
-local M = {_infoview = nil, _opts = {}}
+local M = {_infoviews = {}, _infoviews_open = {}, _opts = {}}
 
 local _INFOVIEW_BUF_NAME = 'lean://infoview'
 local _DEFAULT_BUF_OPTIONS = {
@@ -24,8 +24,51 @@ local _SEVERITY = {
   [4] = "hint",
 }
 
-function M.update(infoview_bufnr)
-  local _update = vim.b.lean3 and lean3.update_infoview or function(set_lines)
+function M.update(src_winnr)
+  -- grace period for server startup (prevents initial handler error for lean3 files)
+  local succeeded, _ = vim.wait(5000, vim.lsp.buf.server_ready)
+  if not succeeded then return end
+
+  if M._infoviews_open[src_winnr] == false then
+      return
+  end
+
+  local infoview_bufnr
+  local infoview = M._infoviews[src_winnr]
+  if not infoview then
+    M._infoviews[src_winnr] = {}
+
+    infoview_bufnr = vim.api.nvim_create_buf(false, true)
+    vim.api.nvim_buf_set_name(infoview_bufnr, _INFOVIEW_BUF_NAME .. infoview_bufnr)
+    for name, value in pairs(_DEFAULT_BUF_OPTIONS) do
+      vim.api.nvim_buf_set_option(infoview_bufnr, name, value)
+    end
+
+    local current_window = vim.api.nvim_get_current_win()
+
+    vim.cmd "botright vsplit"
+    vim.cmd(string.format("buffer %d", infoview_bufnr))
+
+    local window = vim.api.nvim_get_current_win()
+
+    for name, value in pairs(_DEFAULT_WIN_OPTIONS) do
+      vim.api.nvim_win_set_option(window, name, value)
+    end
+    vim.api.nvim_set_current_win(current_window)
+
+    local max_width = M._opts.max_width or 79
+    if vim.api.nvim_win_get_width(window) > max_width then
+      vim.api.nvim_win_set_width(window, max_width)
+    end
+
+    M._infoviews[src_winnr].buf = infoview_bufnr
+    M._infoviews[src_winnr].win = window
+
+  else
+    infoview_bufnr = infoview.buf
+  end
+
+  local _update = vim.bo.ft == "lean" and lean3.update_infoview or function(set_lines)
     local current_buffer = vim.api.nvim_get_current_buf()
     local cursor = vim.api.nvim_win_get_cursor(0)
     local params = vim.lsp.util.make_position_params()
@@ -73,73 +116,36 @@ end
 function M.enable(opts)
   M._opts = opts
   vim.api.nvim_exec([[
-    augroup LeanInfoViewOpen
+    augroup LeanInfoViewUpdate
       autocmd!
-      autocmd BufWinEnter *.lean lua require'lean.infoview'.ensure_open()
+      autocmd CursorHold *.lean lua require'lean.infoview'.update(vim.api.nvim_get_current_win())
+      autocmd CursorHoldI *.lean lua require'lean.infoview'.update(vim.api.nvim_get_current_win())
     augroup END
   ]], false)
 end
 
-function M.is_open() return M._infoview ~= nil end
-
-function M.ensure_open()
-  if M.is_open() then return M._infoview.bufnr end
-
-  local bufnr = vim.api.nvim_create_buf(false, true)
-  vim.api.nvim_buf_set_name(bufnr, _INFOVIEW_BUF_NAME)
-  for name, value in pairs(_DEFAULT_BUF_OPTIONS) do
-    vim.api.nvim_buf_set_option(bufnr, name, value)
-  end
-
-  local current_window = vim.api.nvim_get_current_win()
-
-  vim.cmd "botright vsplit"
-  vim.cmd(string.format("buffer %d", bufnr))
+function M.is_open() return M._infoviews_open[vim.api.nvim_get_current_win()] ~= false end
 
-  local window = vim.api.nvim_get_current_win()
-
-  for name, value in pairs(_DEFAULT_WIN_OPTIONS) do
-    vim.api.nvim_win_set_option(window, name, value)
-  end
-  vim.api.nvim_set_current_win(current_window)
-
-  local max_width = M._opts.max_width or 79
-  if vim.api.nvim_win_get_width(window) > max_width then
-    vim.api.nvim_win_set_width(window, max_width)
-  end
-
-  vim.api.nvim_exec(string.format([[
-    augroup LeanInfoViewUpdate
-      autocmd!
-      autocmd CursorHold *.lean lua require'lean.infoview'.update(%d)
-      autocmd CursorHoldI *.lean lua require'lean.infoview'.update(%d)
-    augroup END
-  ]], bufnr, bufnr), false)
-
-  M._infoview = { bufnr = bufnr, window = window }
-  return M._infoview
+function M.open()
+  M._infoviews_open[vim.api.nvim_get_current_win()] = true
+  return M._infoviews
 end
 
-M.open = M.ensure_open
-
 function M.close()
   if not M.is_open() then return end
+  local src_win = vim.api.nvim_get_current_win()
 
-  local infoview = M._infoview
-  M._infoview = nil
-
-  vim.api.nvim_exec([[
-    augroup LeanInfoViewOpen
-      autocmd!
-    augroup END
+  if M._infoviews[src_win].win then
+    vim.api.nvim_win_close(M._infoviews[src_win].win, true)
+  end
 
-    augroup LeanInfoViewUpdate
-      autocmd!
-    augroup END
-  ]], false)
+  -- NOTE: it seems this isn't necessary since unlisted buffers are deleted automatically?
+  --if M._infoviews[src_win].buf then
+  --  vim.api.nvim_buf_delete(M._infoviews[src_win].buf, { force = true })
+  --end
 
-  vim.api.nvim_win_close(infoview.window, true)
-  vim.api.nvim_buf_delete(infoview.bufnr, { force = true })
+  M._infoviews_open[src_win] = false
+  M._infoviews[src_win] = nil
 end
 
 function M.toggle()

lua/lean/init.lua

@@ -9,14 +9,17 @@ function lean.setup(opts)
   local abbreviations = opts.abbreviations or {}
   if abbreviations.enable ~= false then lean.abbreviations.enable(abbreviations) end
 
-  local infoview = opts.infoview or {}
-  if infoview.enable ~= false then require('lean.infoview').enable(infoview) end
+  local treesitter = opts.treesitter or {}
+  if treesitter.enable ~= false then require('lean.treesitter').enable(treesitter) end
 
   local lsp = opts.lsp or {}
   if lsp.enable ~= false then lean.lsp.enable(lsp) end
 
-  local treesitter = opts.treesitter or {}
-  if treesitter.enable ~= false then require('lean.treesitter').enable(treesitter) end
+  local lsp4 = opts.lsp4 or {}
+  if lsp4.enable ~= false then lean.lsp.enable4(lsp4) end
+
+  local infoview = opts.infoview or {}
+  if infoview.enable ~= false then require('lean.infoview').enable(infoview) end
 
   if opts.mappings == true then lean.use_suggested_mappings() end
 end