mirror of
https://github.com/nix-community/nixvim.git
synced 2025-06-24 09:48:42 +02:00
plugins/lean: init + test
This commit is contained in:
Gaetan Lepage
Gaétan Lepage
parent
05d21678da
commit
19654ffed2
3 changed files with 402 additions and 0 deletions
316
plugins/languages/lean.nix
Normal file
316
plugins/languages/lean.nix
Normal file
|
|
@ -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";
|
||||
"<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})
|
||||
'';
|
||||
};
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue