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

README.rst

@@ -11,17 +11,22 @@ 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 of filetype detection.
+You should NOT have ``lean.vim`` installed if using ``lean.nvim``.
 
-    * Install the normal `lean.vim <https://github.com/leanprover/lean.vim>`_.
+Syntax highlighting and basic language support is included, for Lean 4 you can also
+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.
+``lean.nvim`` currently supports both Lean 3 and Lean 4,
+which can be used simultaneously in a single session.
+However, support for Lean 3 may be removed in the future.
 
 Installation
 ------------
@@ -64,9 +69,11 @@ Features
 
     * ``<LocalLeader>i``: toggle infoview
 
-    * ``<LocalLeader>s``: ``sorry`` insertion corresponding to the number of open goals
+    * ``<LocalLeader>pt``: set infoview per-tab mode
+
+    * ``<LocalLeader>pw``: set infoview per-window mode
 
-    * ``<LocalLeader>3``: force a buffer into Lean 3 mode
+    * ``<LocalLeader>s``: ``sorry`` insertion corresponding to the number of open goals
 
 * A basic infoview which can show persistent goal, term & tactic state
 
@@ -88,12 +95,34 @@ You may find browsing `my own dotfiles
 <https://github.com/Julian/dotfiles/tree/main/.config/nvim>`_ useful for
 seeing how I use this plugin myself.
 
+Infoview
+---------------------
+
+Infoviews can be used on a per-tab or per-window basis.
+You can use the commands ``LeanInfoPerTab`` and ``LeanInfoPerWin`` to choose between them.
+
+The "correct" way to exit a Lean source window is to use ``:q`` with your cursor in that window.
+This will automatically close its corresponding infoview. Closing the source window directly
+using, for example, ``CTRL-W + c``, will close the source window and leave the infoview in a "detached"
+state - this is a feature, not a bug!
+
 Configuration & Usage
 ---------------------
 
 In e.g. your ``init.lua``:
 
 .. code-block:: lua
+    -- If you don't already have an existing LSP setup, you may want
+    -- to reference the keybindings section of the nvim-lspconfig
+    -- documentation, which can be found at:
+    -- https://github.com/neovim/nvim-lspconfig#keybindings-and-completion
+    on_attach = function(client, bufnr)
+      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{
         -- Abbreviation support
@@ -124,26 +153,20 @@ In e.g. your ``init.lua``:
             -- Clip the infoview to a maximum width
             max_width = 79,
         },
-        -- Enable the Lean language server?
+        -- Enable the Lean3(lsp3)/Lean4(lsp) 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)
-                -- If you don't already have an existing LSP setup, you
-                -- may want to reference the keybindings section of the
-                -- aforementioned nvim-lspconfig documentation, which
-                -- can be found at:
-                -- https://github.com/neovim/nvim-lspconfig#keybindings-and-completion
-                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,
+        lsp3 = {
+            on_attach = on_attach,
             cmd = {"lean-language-server", "--stdio", '--', "-M", "4096"},
+        },
+
+        lsp = {
+            on_attach = on_attach,
+            cmd = {"lean", "--server"},
         }
     }
 
@@ -179,6 +202,17 @@ you're interested in. Below is a (hopelessly incomplete) list of a few:
     * `lsp-trouble <https://github.com/folke/lsp-trouble.nvim>`_ for
       showing a grouped view of diagnostics to pair with the "infauxview"
 
+Roadmap
+-------------
+
+Some features we plan to implement in the near future:
+
+* Pinnable and pausable infoview messages (à la VSCode)
+
+* Connection to true HTML infoviews (in a separate browser window)
+
+* ... suggestions welcome!
+
 Contributing
 ------------
 

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,30 @@
+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 =
+        \ ',\<\%(namespace\|section\)\s\+\(.\{-}\)\>:\<end\s\+\1\>'
+endif

ftplugin/lean/switch.vim

@@ -8,11 +8,6 @@ endif
 let b:switch_definitions = [
     \ g:switch_builtins.true_false,
     \ ["#check", "#eval", "#reduce"],
-    \ ['\(begin\n\s*\)\@<!sorry', 'begin\r  sorry\rend'],
-    \ ["tidy", "suggest", "hint", "linarith", "library_search"],
-    \ ["rw", "simp", "simp?"],
-    \ ["cases", "rcases", "obtain"],
-    \ ["norm_cast", "push_cast"],
     \ ["inl", "inr"],
     \ ["tt", "ff"],
     \ ["=", "≠"],

ftplugin/lean3/infoview.vim

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

ftplugin/lean3/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/lean3/switch.vim

@@ -0,0 +1,40 @@
+" 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"],
+    \ ['\(begin\n\s*\)\@<!sorry', 'begin\r  sorry\rend'],
+    \ ["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,4 @@
+if exists("b:did_indent")
+  finish
+endif
+let b:did_indent = 1

indent/lean3.vim

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

lua/lean/_compe.lua

@@ -19,7 +19,7 @@ end
 Source.get_metadata = function(_)
   return {
     priority = 100;
-    filetypes = {'lean'};
+    filetypes = {'lean3', 'lean'};
     dup = true;
     sort = true;
     menu = '[LA]';

lua/lean/abbreviations.lua

@@ -33,6 +33,7 @@ local function snippets_nvim_enable(snippets, lean_abbreviations)
   end
 
   local all_snippets = snippets.snippets or {}
+  all_snippets.lean3 = lean_abbreviations
   all_snippets.lean = lean_abbreviations
   snippets.snippets = all_snippets
 end

lua/lean/ft.lua

@@ -0,0 +1,22 @@
+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.*\".*:3.*'
+
+
+local M = {}
+
+-- If a TOML file with a lean3 version string is found, use filetype "lean3".
+-- Otherwise use "lean" (lean4).
+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 = "lean3" return end
+  end
+  vim.bo.ft = "lean"
+end
+
+return M