mirror/nix-community.nixvim
1
0
Fork 0
mirror of https://github.com/nix-community/nixvim.git synced 2025-06-21 08:35:43 +02:00
Code Issues Projects Releases Packages Wiki Activity Actions 1

plugins/lean: migrate to mkNeovimPlugin

Browse source
This commit is contained in:
Austin Horstman 2025-01-31 16:07:26 -06:00 • committed by nix-infra-bot
parent 0e92aaf3f2
commit c75e4ea37f
3 changed files with 256 additions and 263 deletions
Download patch file Download diff file Expand all files Collapse all files

317
plugins/by-name/lean/default.nix
View file

@ -1,81 +1,77 @@
{ {
lib, lib,
helpers,
config,
pkgs, pkgs,
... ...
}: }:
with lib;
let let
cfg = config.plugins.lean; inherit (lib.nixvim) defaultNullOpts mkNullOrOption;
inherit (lib) types;
in in
{ lib.nixvim.plugins.mkNeovimPlugin {
options.plugins.lean = lib.nixvim.plugins.neovim.extraOptionsOptions // { name = "lean";
enable = mkEnableOption "lean-nvim"; packPathName = "lean.nvim";
package = "lean-nvim";
package = lib.mkPackageOption pkgs "lean-nvim" { maintainers = [ lib.maintainers.khaneliman ];
default = [
"vimPlugins"
"lean-nvim"
];
};
extraOptions = {
leanPackage = lib.mkPackageOption pkgs "lean" { leanPackage = lib.mkPackageOption pkgs "lean" {
nullable = true; nullable = true;
default = "lean4"; default = "lean4";
}; };
};
lsp = helpers.defaultNullOpts.mkNullable ( settingsOptions = {
with types; lsp = defaultNullOpts.mkNullable (types.submodule {
submodule { freeformType = types.attrsOf types.anything;
freeformType = types.attrs; options = {
options = { enable = defaultNullOpts.mkBool true ''
enable = helpers.defaultNullOpts.mkBool true '' Whether to enable the Lean language server(s).
Whether to enable the Lean language server(s) ?
Set to `false` to disable, otherwise should be a table of options to pass to Set to `false` to disable, otherwise should be a table of options to pass to
`leanls`. `leanls`.
See https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#leanls
for details.
'';
on_attach = helpers.mkNullOrOption types.str '' See https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#leanls
The LSP handler. for details.
''; '';
init_options = helpers.mkNullOrOption (with types; attrsOf anything) '' on_attach = mkNullOrOption types.str ''
The options to configure the lean language server. The LSP handler.
See `Lean.Lsp.InitializationOptions` for details. '';
'';
};
}
) { } "LSP settings.";
init_options = mkNullOrOption (with types; attrsOf anything) ''
The options to configure the lean language server.
See `Lean.Lsp.InitializationOptions` for details.
'';
};
}) { } "LSP settings.";
ft = { ft = {
default = helpers.defaultNullOpts.mkStr "lean" '' default = defaultNullOpts.mkStr "lean" ''
The default filetype for Lean files. The default filetype for Lean files.
''; '';
nomodifiable = mkNullOrOption (types.listOf types.str) ''
nomodifiable = helpers.mkNullOrOption (with types; listOf str) ''
A list of patterns which will be used to protect any matching Lean file paths from being 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`). accidentally modified (by marking the buffer as `nomodifiable`).
By default, this list includes the Lean standard libraries, as well as files within By default, this list includes the Lean standard libraries, as well as files within
dependency directories (e.g. `_target`) dependency directories (e.g. `_target`)
Set this to an empty table to disable. Set this to an empty table to disable.
''; '';
}; };
abbreviations = { abbreviations = {
enable = helpers.defaultNullOpts.mkBool true '' enable = defaultNullOpts.mkBool true ''
Whether to enable expanding of unicode abbreviations. Whether to enable expanding of unicode abbreviations.
''; '';
extra = defaultNullOpts.mkAttrsOf' {
extra = helpers.defaultNullOpts.mkAttrsOf types.str { } '' type = types.str;
Additional abbreviations. pluginDefault = { };
description = ''
Example: Additional abbreviations.
``` '';
example = lib.literalExpression ''
```nix
{ {
# Add a \wknight abbreviation to insert ♘ # Add a \wknight abbreviation to insert ♘
# #
@ -84,87 +80,49 @@ in
# this if so desired. # this if so desired.
wknight = "♘"; wknight = "♘";
} }
''; '';
};
leader = helpers.defaultNullOpts.mkStr "\\" '' leader = defaultNullOpts.mkStr "\\" ''
Change if you don't like the backslash. Change if you don't like the backslash.
(comma is a popular choice on French keyboards)
''; '';
}; };
mappings = defaultNullOpts.mkBool false ''
mappings = helpers.defaultNullOpts.mkBool false ''
Whether to enable suggested mappings. Whether to enable suggested mappings.
''; '';
infoview = { infoview = {
autoopen = helpers.defaultNullOpts.mkBool true '' autoopen = defaultNullOpts.mkBool true ''
Automatically open an infoview on entering a Lean buffer? Automatically open an infoview on entering a Lean buffer.
Should be a function that will be called anytime a new Lean file is opened. Should be a function that will be called anytime a new Lean file is opened.
Return true to open an infoview, otherwise false. 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 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`, Lean file, or setting it to `false` is the same as `function() return false end`,
i.e. never autoopen. i.e. never autoopen.
''; '';
autopause = defaultNullOpts.mkBool false "Set whether a new pin is automatically paused.";
autopause = helpers.defaultNullOpts.mkBool false ""; width = defaultNullOpts.mkPositiveInt 50 ''
width = helpers.defaultNullOpts.mkPositiveInt 50 ''
Set infoview windows' starting width. Set infoview windows' starting width.
Windows are opened horizontally or vertically depending on spacing.
''; '';
height = defaultNullOpts.mkPositiveInt 20 ''
height = helpers.defaultNullOpts.mkPositiveInt 20 ''
Set infoview windows' starting height. Set infoview windows' starting height.
Windows are opened horizontally or vertically depending on spacing.
''; '';
horizontal_position = defaultNullOpts.mkEnumFirstDefault [ "bottom" "top" ] ''
horizontalPosition = Put the infoview on the top or bottom when horizontal.
helpers.defaultNullOpts.mkEnum '';
[ separate_tab = defaultNullOpts.mkBool false ''
"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. 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 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. in the terminal at the same time.
Note that `height` and `width` will be ignored in this case. Note that `height` and `width` will be ignored in this case.
''; '';
indicators = defaultNullOpts.mkEnumFirstDefault [ "auto" "always" "never" ] ''
indicators = Show indicators for pin locations when entering an infoview window.
helpers.defaultNullOpts.mkEnum '';
[ show_processing = defaultNullOpts.mkBool true "";
"always" show_no_info_message = defaultNullOpts.mkBool false "";
"never" use_widgets = defaultNullOpts.mkBool true "Whether to use widgets.";
"auto" mappings = defaultNullOpts.mkAttrsOf types.str {
]
"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.mkAttrsOf types.str {
K = "click"; K = "click";
"<CR>" = "click"; "<CR>" = "click";
gd = "go_to_def"; gd = "go_to_def";
@ -177,126 +135,59 @@ in
"<LocalLeader><Tab>" = "goto_last_window"; "<LocalLeader><Tab>" = "goto_last_window";
} "Mappings."; } "Mappings.";
}; };
progress_bars = {
progressBars = { enable = defaultNullOpts.mkBool true ''
enable = helpers.defaultNullOpts.mkBool true ''
Whether to enable the progress bars. Whether to enable the progress bars.
''; '';
priority = defaultNullOpts.mkUnsignedInt 10 ''
priority = helpers.defaultNullOpts.mkUnsignedInt 10 ''
Use a different priority for the signs. Use a different priority for the signs.
''; '';
}; };
stderr = { stderr = {
enable = helpers.defaultNullOpts.mkBool true '' enable = defaultNullOpts.mkBool true ''
Redirect Lean's stderr messages somewhere (to a buffer by default). Redirect Lean's stderr messages somewhere (to a buffer by default).
''; '';
height = defaultNullOpts.mkPositiveInt 5 "Height of the window.";
height = helpers.defaultNullOpts.mkPositiveInt 5 "Height of the window."; on_lines = defaultNullOpts.mkLuaFn "nil" ''
onLines = helpers.defaultNullOpts.mkLuaFn "nil" ''
A callback which will be called with (multi-line) stderr output. 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 ( settingsExample = {
with types; settings = {
submodule { lsp = {
freeformType = types.attrs; enable = true;
options = { };
enable = helpers.defaultNullOpts.mkBool true '' ft = {
Whether to enable the legacy Lean 3 language server ? default = "lean";
nomodifiable = [ "_target" ];
Set to `false` to disable, otherwise should be a table of options to pass to };
`lean3ls`. abbreviations = {
See https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#lean3ls enable = true;
for details. extra = {
''; wknight = "♘";
on_attach = helpers.mkNullOrOption types.str "The LSP handler.";
}; };
} };
) { } "Legacy Lean3 LSP settings."; mappings = false;
}; infoview = {
horizontal_position = "top";
config = mkIf cfg.enable { separate_tab = true;
extraPlugins = [ cfg.package ]; indicators = "always";
};
assertions = lib.nixvim.mkAssertions "plugins.lean" { progress_bars = {
assertion = enable = false;
!( };
# leanls lsp server is disabled in nvim-lspconfig stderr = {
config.plugins.lsp.servers.leanls.enable on_lines.__raw = "function(lines) vim.notify(lines) end";
# lsp is not explicitly disabled in the lean.nvim plugin };
&& (cfg.lsp.enable != false)
);
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 = [ 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 = onLines;
};
inherit lsp3;
}
// cfg.extraOptions;
in
''
require("lean").setup(${lib.nixvim.toLuaObject setupOptions})
'';
}; };
extraConfig = cfg: {
extraPackages = [ cfg.leanPackage ];
};
# TODO: Deprecated in 2025-01-31
inherit (import ./deprecations.nix) deprecateExtraOptions optionsRenamedToSettings;
} }

109
plugins/by-name/lean/deprecations.nix Normal file
View file

@ -0,0 +1,109 @@
{
deprecateExtraOptions = true;
optionsRenamedToSettings = [
"lsp"
[
"ft"
"default"
]
[
"ft"
"nomodifiable"
]
[
"abbreviations"
"enable"
]
[
"abbreviations"
"extra"
]
[
"abbreviations"
"leader"
]
"mappings"
[
"infoview"
"autoopen"
]
[
"infoview"
"autopause"
]
[
"infoview"
"width"
]
[
"infoview"
"height"
]
[
"infoview"
"horizontalPosition"
]
[
"infoview"
"separateTab"
]
[
"infoview"
"indicators"
]
[
"infoview"
"lean3"
"showFilter"
]
[
"infoview"
"lean3"
"mouseEvents"
]
[
"infoview"
"showProcessing"
]
[
"infoview"
"showNoInfoMessage"
]
[
"infoview"
"useWidgets"
]
[
"infoview"
"mappings"
]
[
"progressBars"
"enable"
]
[
"progressBars"
"priority"
]
[
"stderr"
"enable"
]
[
"stderr"
"height"
]
[
"stderr"
"onLines"
]
[
"lsp3"
"enable"
]
[
"lsp3"
"onAttach"
]
];
}

93
tests/test-sources/plugins/by-name/lean/default.nix
View file

@ -23,8 +23,7 @@ lib.optionalAttrs doRun {
lean = { lean = {
enable = true; enable = true;
settings.lsp.enable = false;
lsp.enable = false;
}; };
}; };
}; };
@ -35,58 +34,52 @@ lib.optionalAttrs doRun {
lean = { lean = {
enable = true; enable = true;
settings = {
lsp = { }; lsp = { };
ft = { ft = {
default = "lean"; default = "lean";
nomodifiable = null; nomodifiable = null;
};
abbreviations = {
enable = true;
extra = {
wknight = "♘";
}; };
leader = "\\"; abbreviations = {
}; enable = true;
mappings = false; extra = { };
infoview = { leader = "\\";
autoopen = true;
autopause = false;
width = 50;
height = 20;
horizontalPosition = "bottom";
separateTab = false;
indicators = "auto";
lean3 = {
showFilter = true;
mouseEvents = false;
}; };
showProcessing = true; mappings = false;
showNoInfoMessage = false; infoview = {
useWidgets = true; autoopen = true;
mappings = { autopause = false;
K = "click"; width = 50;
"<CR>" = "click"; height = 20;
gd = "go_to_def"; horizontal_position = "bottom";
gD = "go_to_decl"; separate_tab = false;
gy = "go_to_type"; indicators = "auto";
I = "mouse_enter"; show_processing = true;
i = "mouse_leave"; show_no_info_message = false;
"<Esc>" = "clear_all"; use_widgets = true;
C = "clear_all"; mappings = {
"<LocalLeader><Tab>" = "goto_last_window"; K = "click";
"<CR>" = "click";
gd = "go_to_def";
gD = "go_to_decl";
gy = "go_to_type";
I = "mouse_enter";
i = "mouse_leave";
"<Esc>" = "clear_all";
C = "clear_all";
"<LocalLeader><Tab>" = "goto_last_window";
};
};
progress_bars = {
enable = true;
priority = 10;
};
stderr = {
enable = true;
height = 5;
on_lines.__raw = "function(lines) vim.notify(lines) end";
}; };
}; };
progressBars = {
enable = true;
priority = 10;
};
stderr = {
enable = true;
height = 5;
onLines = "function(lines) vim.notify(lines) end";
};
lsp3 = { };
}; };
}; };
}; };