mirror of
https://github.com/nix-community/nixvim.git
synced 2025-06-21 08:35:43 +02:00
317 lines
10 KiB
Nix
317 lines
10 KiB
Nix
|
{
|
||
|
|
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";
|
||
|
|
"<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";
|
||
|
|
}
|
||
|
|
''
|
||
|
|
"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})
|
||
|
|
'';
|
||
|
|
};
|
||
|
|
}
|