Merge pull request #52 from rish987/simul_lean3_lean4

Implement simultaneous lean3 and lean4 support with minimal lean4 syntax support.

README.rst

@@ -8,6 +8,10 @@ lean.nvim
 Prerequisites
 -------------
 
+NOTE: ``lean.nvim`` is incompatible with ``lean.vim``,
+as it implements its own kind of filetype detection.
+If using ``lean.nvim``, you should NOT have ``lean.vim`` installed.
+
 ``lean.nvim`` currently requires `neovim 0.5 HEAD / nightly
 <https://github.com/neovim/neovim/releases/tag/nightly>`_.
 
@@ -90,6 +94,18 @@ Configuration & Usage
 In e.g. your ``init.lua``:
 
 .. code-block:: lua
+    local function on_attach(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')
+    }
 
     require('lean').setup{
         -- Abbreviation support
@@ -120,26 +136,24 @@ In e.g. your ``init.lua``:
             -- Clip the infoview to a maximum width
             max_width = 79,
         },
-        -- Enable the Lean language server?
+
+        -- Enable the Lean 3/Lean 4 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,
+
+        -- Lean 3
+        lsp3 = {
+            on_attach = on_attach
             cmd = {"lean-language-server", "--stdio", '--', "-M", "4096"},
+        },
+
+        -- Lean 4
+        lsp = {
+            on_attach = on_attach
+            cmd = {"lean", "--server"},
         }
     }
 

ftplugin/lean3/infoview.vim

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

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

@@ -2,9 +2,23 @@ local M = {}
 
 local lean3 = require("lean.lean3")
 
+local find_project_root = require('lspconfig.util').root_pattern('leanpkg.toml')
+
+-- 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.*'
+
 function M.detect()
-  vim.api.nvim_command("setfiletype lean")
-  if lean3.is_lean3_project() then lean3.init() end
+  local ft = "lean"
+  local project_root = find_project_root(vim.api.nvim_buf_get_name(0))
+  if project_root then
+    local result = vim.fn.readfile(project_root .. '/leanpkg.toml')
+    for _, line in ipairs(result) do
+      if line:match(_MARKER) then ft = "lean3" end
+    end
+  end
+  vim.api.nvim_command("setfiletype " .. ft)
+  if vim.bo.ft == "lean3" then lean3.init() end
 end
 
 return M

lua/lean/init.lua

@@ -23,6 +23,9 @@ function lean.setup(opts)
   opts.infoview = opts.infoview or {}
   if opts.infoview.enable ~= false then require('lean.infoview').enable(opts.infoview) end
 
+  opts.lsp3 = opts.lsp3 or {}
+  if opts.lsp3.enable ~= false then require('lspconfig').lean3ls.setup(opts.lsp3) end
+
   opts.lsp = opts.lsp or {}
   if opts.lsp.enable ~= false then lean.lsp.enable(opts.lsp) end
 
@@ -31,6 +34,7 @@ function lean.setup(opts)
 
   if opts.mappings == true then
     vim.api.nvim_exec([[
+      autocmd FileType lean3 lua require'lean'.use_suggested_mappings(true)
       autocmd FileType lean lua require'lean'.use_suggested_mappings(true)
     ]], false)
   end

lua/lean/lean3.lua

@@ -1,26 +1,10 @@
 local M = {}
 
--- 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 find_project_root = require('lspconfig.util').root_pattern('leanpkg.toml')
-
 function M.init()
   pcall(vim.cmd, 'TSBufDisable highlight')  -- tree-sitter-lean is lean4-only
   vim.b.lean3 = true
 end
 
-function M.is_lean3_project()
-  local project_root = find_project_root(vim.api.nvim_buf_get_name(0))
-  if not project_root then return false end
-  local result = vim.fn.readfile(project_root .. '/leanpkg.toml')
-  for _, line in ipairs(result) do
-    if line:match(_MARKER) then return true end
-  end
-  return false
-end
-
 function M.update_infoview(set_lines)
   local params = vim.lsp.util.make_position_params()
   return vim.lsp.buf_request(0, "textDocument/hover", params, function(_, _, result)

lua/tests/helpers.lua

@@ -18,6 +18,9 @@ local default_config = {
   infoview = {
     enable = false
   },
+  lsp3 = {
+    enable = false
+  },
   lsp = {
     enable = false
   }
@@ -57,13 +60,13 @@ function helpers.clean_buffer(contents, callback)
   return function()
     local bufnr = vim.api.nvim_create_buf(false, true)
     set_unique_name_so_we_always_have_a_separate_fake_file(bufnr)
-    api.nvim_buf_set_option(bufnr, 'filetype', 'lean')
+    api.nvim_buf_set_option(bufnr, 'filetype', 'lean3')
 
     api.nvim_buf_call(bufnr, function()
       -- FIXME: For now all tests are against Lean 3
       require 'lean.lean3'.init()
 
-      if lean.config.lsp.enable ~= false then
+      if lean.config.lsp3.enable ~= false then
         local succeeded, _ = vim.wait(timeout, vim.lsp.buf.server_ready)
         assert.message("LSP server was never ready.").True(succeeded)
       end

lua/tests/sorry_spec.lua

@@ -2,7 +2,7 @@ local helpers = require('tests.helpers')
 local clean_buffer = helpers.clean_buffer
 
 describe('sorry', function()
-  helpers.setup { lsp = { enable = true } }
+  helpers.setup { lsp3 = { enable = true } }
   it('inserts sorries for each remaining goal', clean_buffer([[
 def foo (n : nat) : n = n := begin
   induction n with d hd,

lua/tests/trythis_spec.lua

@@ -1,7 +1,7 @@
 local helpers = require('tests.helpers')
 
 describe('trythis', function()
-  helpers.setup { lsp = { enable = true } }
+  helpers.setup { lsp3 = { enable = true } }
   it('replaces a single try this', helpers.clean_buffer([[
 meta def whatshouldIdo := (do tactic.trace "Try this: existsi 2; refl\n")
 example : ∃ n, n = 2 := by whatshouldIdo]], function()

scripts/minimal_init.lua

@@ -7,7 +7,7 @@ local packpath = lean_nvim_dir .. '/packpath/*'
 vim.o.runtimepath = vim.o.runtimepath .. ',' .. packpath .. ',' .. lean_nvim_dir
 
 vim.api.nvim_exec([[
-  autocmd BufNewFile,BufRead *.lean setlocal filetype=lean
+  autocmd BufNewFile,BufRead *.lean setlocal filetype=lean3
 
   runtime! plugin/lspconfig.vim
   runtime! plugin/plenary.vim