From e17d331a8f7b05d6817f8b7f139d2e51df1afa2c Mon Sep 17 00:00:00 2001 From: Gaetan Lepage Date: Sat, 11 Nov 2023 23:40:32 +0100 Subject: [PATCH 1/2] plugins/lsp: add leanls, the language server for lean --- plugins/lsp/language-servers/default.nix | 5 +++++ tests/test-sources/plugins/lsp/nvim-lsp.nix | 1 + 2 files changed, 6 insertions(+) diff --git a/plugins/lsp/language-servers/default.nix b/plugins/lsp/language-servers/default.nix index df06093389..2ed522f81d 100644 --- a/plugins/lsp/language-servers/default.nix +++ b/plugins/lsp/language-servers/default.nix @@ -237,6 +237,11 @@ with lib; let description = "Enable kotlin language server"; serverName = "kotlin_language_server"; } + { + name = "leanls"; + description = "Enable leanls, for Lean"; + package = pkgs.lean; + } { name = "ltex"; description = "Enable ltex-ls, for LanguageTool"; diff --git a/tests/test-sources/plugins/lsp/nvim-lsp.nix b/tests/test-sources/plugins/lsp/nvim-lsp.nix index d282e86f91..cc1f769f75 100644 --- a/tests/test-sources/plugins/lsp/nvim-lsp.nix +++ b/tests/test-sources/plugins/lsp/nvim-lsp.nix @@ -99,6 +99,7 @@ jsonls.enable = true; julials.enable = true; kotlin-language-server.enable = true; + leanls.enable = true; ltex.enable = true; lua-ls.enable = true; metals.enable = true; From 54a6c49902e3b3c019f3f5e020ee17e3bd8aa9ff Mon Sep 17 00:00:00 2001 From: Gaetan Lepage Date: Sat, 11 Nov 2023 23:40:39 +0100 Subject: [PATCH 2/2] plugins/lean: init + test --- plugins/default.nix | 1 + plugins/languages/lean.nix | 316 ++++++++++++++++++ tests/test-sources/plugins/languages/lean.nix | 85 +++++ 3 files changed, 402 insertions(+) create mode 100644 plugins/languages/lean.nix create mode 100644 tests/test-sources/plugins/languages/lean.nix diff --git a/plugins/default.nix b/plugins/default.nix index 5049fd9f50..3739e46294 100644 --- a/plugins/default.nix +++ b/plugins/default.nix @@ -43,6 +43,7 @@ ./languages/clangd-extensions.nix ./languages/julia/julia-cell.nix + ./languages/lean.nix ./languages/ledger.nix ./languages/markdown-preview.nix ./languages/nix.nix diff --git a/plugins/languages/lean.nix b/plugins/languages/lean.nix new file mode 100644 index 0000000000..12297833b9 --- /dev/null +++ b/plugins/languages/lean.nix @@ -0,0 +1,316 @@ +{ + lib, + helpers, + config, + pkgs, + ... +}: +with lib; let + cfg = config.plugins.lean; +in { + options.plugins.lean = + helpers.extraOptionsOptions + // { + enable = mkEnableOption "lean-nvim"; + + package = helpers.mkPackageOption "lean-nvim" pkgs.vimPlugins.lean-nvim; + + leanPackage = mkOption { + type = with types; nullOr package; + default = pkgs.lean4; + description = "Which package to use for lean."; + example = null; + }; + + lsp = + helpers.defaultNullOpts.mkNullable + ( + with types; + submodule { + freeformType = types.attrs; + options = { + enable = helpers.defaultNullOpts.mkBool true '' + Whether to enable the Lean language server(s) ? + + Set to `false` to disable, otherwise should be a table of options to pass to + `leanls`. + See https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#leanls + for details. + ''; + + on_attach = helpers.mkNullOrOption types.str '' + The LSP handler. + ''; + + init_options = helpers.mkNullOrOption (with types; attrsOf anything) '' + The options to configure the lean language server. + See `Lean.Lsp.InitializationOptions` for details. + ''; + }; + } + ) + "{}" + "LSP settings."; + + ft = { + default = helpers.defaultNullOpts.mkStr "lean" '' + The default filetype for Lean files. + ''; + + nomodifiable = helpers.mkNullOrOption (with types; listOf str) '' + A list of patterns which will be used to protect any matching Lean file paths from being + accidentally modified (by marking the buffer as `nomodifiable`). + + By default, this list includes the Lean standard libraries, as well as files within + dependency directories (e.g. `_target`) + Set this to an empty table to disable. + ''; + }; + + abbreviations = { + enable = helpers.defaultNullOpts.mkBool true '' + Whether to enable expanding of unicode abbreviations. + ''; + + extra = helpers.defaultNullOpts.mkNullable (with types; attrsOf str) "{}" '' + Additional abbreviations. + + Example: + ``` + { + # Add a \wknight abbreviation to insert ♘ + # + # Note that the backslash is implied, and that you of + # course may also use a snippet engine directly to do + # this if so desired. + wknight = "♘"; + } + ''; + + leader = helpers.defaultNullOpts.mkStr "\\" '' + Change if you don't like the backslash. + (comma is a popular choice on French keyboards) + ''; + }; + + mappings = helpers.defaultNullOpts.mkBool false '' + Whether to enable suggested mappings. + ''; + + infoview = { + autoopen = helpers.defaultNullOpts.mkBool true '' + Automatically open an infoview on entering a Lean buffer? + Should be a function that will be called anytime a new Lean file is opened. + Return true to open an infoview, otherwise false. + Setting this to `true` is the same as `function() return true end`, i.e. autoopen for any + Lean file, or setting it to `false` is the same as `function() return false end`, + i.e. never autoopen. + ''; + + autopause = helpers.defaultNullOpts.mkBool false ""; + + width = helpers.defaultNullOpts.mkPositiveInt 50 '' + Set infoview windows' starting width. + Windows are opened horizontally or vertically depending on spacing. + ''; + + height = helpers.defaultNullOpts.mkPositiveInt 20 '' + Set infoview windows' starting height. + Windows are opened horizontally or vertically depending on spacing. + ''; + + horizontalPosition = helpers.defaultNullOpts.mkEnum ["top" "bottom"] "bottom" '' + Put the infoview on the top or bottom when horizontal. + ''; + + separateTab = helpers.defaultNullOpts.mkBool false '' + Always open the infoview window in a separate tabpage. + Might be useful if you are using a screen reader and don't want too many dynamic updates + in the terminal at the same time. + Note that `height` and `width` will be ignored in this case. + ''; + + indicators = helpers.defaultNullOpts.mkEnum ["always" "never" "auto"] "auto" '' + Show indicators for pin locations when entering an infoview window. + `"auto"` = only when there are multiple pins. + ''; + + lean3 = { + showFilter = helpers.defaultNullOpts.mkBool true ""; + + mouseEvents = helpers.defaultNullOpts.mkBool false '' + Setting this to `true` will simulate mouse events in the Lean 3 infoview, this is buggy + at the moment so you can use the I/i keybindings to manually trigger these. + ''; + }; + + showProcessing = helpers.defaultNullOpts.mkBool true ""; + + showNoInfoMessage = helpers.defaultNullOpts.mkBool false ""; + + useWidgets = helpers.defaultNullOpts.mkBool true "Whether to use widgets."; + + mappings = + helpers.defaultNullOpts.mkNullable + (with types; attrsOf str) + '' + { + K = "click"; + "" = "click"; + gd = "go_to_def"; + gD = "go_to_decl"; + gy = "go_to_type"; + I = "mouse_enter"; + i = "mouse_leave"; + "" = "clear_all"; + C = "clear_all"; + "" = "goto_last_window"; + } + '' + "Mappings."; + }; + + progressBars = { + enable = helpers.defaultNullOpts.mkBool true '' + Whether to enable the progress bars. + ''; + + priority = helpers.defaultNullOpts.mkUnsignedInt 10 '' + Use a different priority for the signs. + ''; + }; + + stderr = { + enable = helpers.defaultNullOpts.mkBool true '' + Redirect Lean's stderr messages somehwere (to a buffer by default). + ''; + + height = helpers.defaultNullOpts.mkPositiveInt 5 "Height of the window."; + + onLines = helpers.mkNullOrOption types.str '' + A callback which will be called with (multi-line) stderr output. + + e.g., use: + ```nix + onLines = "function(lines) vim.notify(lines) end"; + ``` + if you want to redirect stderr to `vim.notify`. + The default implementation will redirect to a dedicated stderr + window. + ''; + }; + + lsp3 = + helpers.defaultNullOpts.mkNullable + ( + with types; + submodule { + freeformType = types.attrs; + options = { + enable = helpers.defaultNullOpts.mkBool true '' + Whether to enable the legacy Lean 3 language server ? + + Set to `false` to disable, otherwise should be a table of options to pass to + `lean3ls`. + See https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#lean3ls + for details. + ''; + + on_attach = helpers.mkNullOrOption types.str "The LSP handler."; + }; + } + ) + "{}" + "Legacy Lean3 LSP settings."; + }; + + config = mkIf cfg.enable { + extraPlugins = [cfg.package]; + + assertions = [ + { + assertion = + !( + # leanls lsp server is disabled in nvim-lspconfig + config.plugins.lsp.servers.leanls.enable + # lsp is not (!) disabled in the lean.nvim plugin + && !( + # lsp is explicitly set to `false`. + (isBool cfg.lsp.enable) + && !cfg.lsp.enable + ) + ); + message = '' + You have not explicitly set `plugins.lean.lsp` to `false` while having `plugins.lsp.servers.leanls.enable` set to `true`. + You need to either + + - Remove the configuration in `plugins.lsp.servers.leanls` and move it to `plugins.lean.lsp`. + - Explicitly disable the autoconfiguration of the lsp in the lean.nvim plugin by setting `plugins.lean.lsp` to `false`. + + https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#leanls + ''; + } + ]; + + extraPackages = optional (cfg.leanPackage != null) cfg.leanPackage; + + extraConfigLua = let + setupOptions = with cfg; + { + inherit lsp; + ft = with ft; { + inherit + default + nomodifiable + ; + }; + abbreviations = with abbreviations; { + inherit + enable + extra + leader + ; + }; + inherit mappings; + infoview = with infoview; { + inherit + autoopen + autopause + width + height + ; + horizontal_position = horizontalPosition; + separate_tab = separateTab; + inherit indicators; + lean3 = with lean3; { + show_filter = showFilter; + mouse_events = mouseEvents; + }; + show_processing = showProcessing; + show_no_info_message = showNoInfoMessage; + use_widgets = useWidgets; + inherit mappings; + }; + progress_bars = with progressBars; { + inherit + enable + priority + ; + }; + stderr = with stderr; { + inherit + enable + height + ; + on_lines = + helpers.ifNonNull' onLines + (helpers.mkRaw onLines); + }; + inherit lsp3; + } + // cfg.extraOptions; + in '' + require("lean").setup(${helpers.toLuaObject setupOptions}) + ''; + }; +} diff --git a/tests/test-sources/plugins/languages/lean.nix b/tests/test-sources/plugins/languages/lean.nix new file mode 100644 index 0000000000..f887ec2d74 --- /dev/null +++ b/tests/test-sources/plugins/languages/lean.nix @@ -0,0 +1,85 @@ +{ + empty = { + plugins.lean.enable = true; + }; + + # Enable the `leanls` LSP directly from `plugins.lsp`. This implies explicitly disabling the lsp + # in the `lean` plugin configuration. + lspDisabled = { + plugins = { + lsp = { + enable = true; + + servers.leanls.enable = true; + }; + + lean = { + enable = true; + + lsp.enable = false; + }; + }; + }; + + default = { + plugins = { + lsp.enable = true; + + lean = { + enable = true; + + lsp = {}; + ft = { + default = "lean"; + nomodifiable = null; + }; + abbreviations = { + enable = true; + extra = { + wknight = "♘"; + }; + leader = "\\"; + }; + mappings = false; + infoview = { + autoopen = true; + autopause = false; + width = 50; + height = 20; + horizontalPosition = "bottom"; + separateTab = false; + indicators = "auto"; + lean3 = { + showFilter = true; + mouseEvents = false; + }; + showProcessing = true; + showNoInfoMessage = false; + useWidgets = true; + mappings = { + K = "click"; + "" = "click"; + gd = "go_to_def"; + gD = "go_to_decl"; + gy = "go_to_type"; + I = "mouse_enter"; + i = "mouse_leave"; + "" = "clear_all"; + C = "clear_all"; + "" = "goto_last_window"; + }; + }; + progressBars = { + enable = true; + priority = 10; + }; + stderr = { + enable = true; + height = 5; + onLines = "function(lines) vim.notify(lines) end"; + }; + lsp3 = {}; + }; + }; + }; +}