Skip to content

Commit 19654ff

Browse files
GaetanLepageGaetanLepage
committed
plugins/lean: init + test
1 parent 05d2167 commit 19654ff

File tree

3 files changed

+402
-0
lines changed

3 files changed

+402
-0
lines changed

Diff for: ‎plugins/default.nix

+1
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,7 @@
4343

4444
./languages/clangd-extensions.nix
4545
./languages/julia/julia-cell.nix
46+
./languages/lean.nix
4647
./languages/ledger.nix
4748
./languages/markdown-preview.nix
4849
./languages/nix.nix

Diff for: ‎plugins/languages/lean.nix

+316
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,316 @@
1+
{
2+
lib,
3+
helpers,
4+
config,
5+
pkgs,
6+
...
7+
}:
8+
with lib; let
9+
cfg = config.plugins.lean;
10+
in {
11+
options.plugins.lean =
12+
helpers.extraOptionsOptions
13+
// {
14+
enable = mkEnableOption "lean-nvim";
15+
16+
package = helpers.mkPackageOption "lean-nvim" pkgs.vimPlugins.lean-nvim;
17+
18+
leanPackage = mkOption {
19+
type = with types; nullOr package;
20+
default = pkgs.lean4;
21+
description = "Which package to use for lean.";
22+
example = null;
23+
};
24+
25+
lsp =
26+
helpers.defaultNullOpts.mkNullable
27+
(
28+
with types;
29+
submodule {
30+
freeformType = types.attrs;
31+
options = {
32+
enable = helpers.defaultNullOpts.mkBool true ''
33+
Whether to enable the Lean language server(s) ?
34+
35+
Set to `false` to disable, otherwise should be a table of options to pass to
36+
`leanls`.
37+
See https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#leanls
38+
for details.
39+
'';
40+
41+
on_attach = helpers.mkNullOrOption types.str ''
42+
The LSP handler.
43+
'';
44+
45+
init_options = helpers.mkNullOrOption (with types; attrsOf anything) ''
46+
The options to configure the lean language server.
47+
See `Lean.Lsp.InitializationOptions` for details.
48+
'';
49+
};
50+
}
51+
)
52+
"{}"
53+
"LSP settings.";
54+
55+
ft = {
56+
default = helpers.defaultNullOpts.mkStr "lean" ''
57+
The default filetype for Lean files.
58+
'';
59+
60+
nomodifiable = helpers.mkNullOrOption (with types; listOf str) ''
61+
A list of patterns which will be used to protect any matching Lean file paths from being
62+
accidentally modified (by marking the buffer as `nomodifiable`).
63+
64+
By default, this list includes the Lean standard libraries, as well as files within
65+
dependency directories (e.g. `_target`)
66+
Set this to an empty table to disable.
67+
'';
68+
};
69+
70+
abbreviations = {
71+
enable = helpers.defaultNullOpts.mkBool true ''
72+
Whether to enable expanding of unicode abbreviations.
73+
'';
74+
75+
extra = helpers.defaultNullOpts.mkNullable (with types; attrsOf str) "{}" ''
76+
Additional abbreviations.
77+
78+
Example:
79+
```
80+
{
81+
# Add a \wknight abbreviation to insert ♘
82+
#
83+
# Note that the backslash is implied, and that you of
84+
# course may also use a snippet engine directly to do
85+
# this if so desired.
86+
wknight = "♘";
87+
}
88+
'';
89+
90+
leader = helpers.defaultNullOpts.mkStr "\\" ''
91+
Change if you don't like the backslash.
92+
(comma is a popular choice on French keyboards)
93+
'';
94+
};
95+
96+
mappings = helpers.defaultNullOpts.mkBool false ''
97+
Whether to enable suggested mappings.
98+
'';
99+
100+
infoview = {
101+
autoopen = helpers.defaultNullOpts.mkBool true ''
102+
Automatically open an infoview on entering a Lean buffer?
103+
Should be a function that will be called anytime a new Lean file is opened.
104+
Return true to open an infoview, otherwise false.
105+
Setting this to `true` is the same as `function() return true end`, i.e. autoopen for any
106+
Lean file, or setting it to `false` is the same as `function() return false end`,
107+
i.e. never autoopen.
108+
'';
109+
110+
autopause = helpers.defaultNullOpts.mkBool false "";
111+
112+
width = helpers.defaultNullOpts.mkPositiveInt 50 ''
113+
Set infoview windows' starting width.
114+
Windows are opened horizontally or vertically depending on spacing.
115+
'';
116+
117+
height = helpers.defaultNullOpts.mkPositiveInt 20 ''
118+
Set infoview windows' starting height.
119+
Windows are opened horizontally or vertically depending on spacing.
120+
'';
121+
122+
horizontalPosition = helpers.defaultNullOpts.mkEnum ["top" "bottom"] "bottom" ''
123+
Put the infoview on the top or bottom when horizontal.
124+
'';
125+
126+
separateTab = helpers.defaultNullOpts.mkBool false ''
127+
Always open the infoview window in a separate tabpage.
128+
Might be useful if you are using a screen reader and don't want too many dynamic updates
129+
in the terminal at the same time.
130+
Note that `height` and `width` will be ignored in this case.
131+
'';
132+
133+
indicators = helpers.defaultNullOpts.mkEnum ["always" "never" "auto"] "auto" ''
134+
Show indicators for pin locations when entering an infoview window.
135+
`"auto"` = only when there are multiple pins.
136+
'';
137+
138+
lean3 = {
139+
showFilter = helpers.defaultNullOpts.mkBool true "";
140+
141+
mouseEvents = helpers.defaultNullOpts.mkBool false ''
142+
Setting this to `true` will simulate mouse events in the Lean 3 infoview, this is buggy
143+
at the moment so you can use the I/i keybindings to manually trigger these.
144+
'';
145+
};
146+
147+
showProcessing = helpers.defaultNullOpts.mkBool true "";
148+
149+
showNoInfoMessage = helpers.defaultNullOpts.mkBool false "";
150+
151+
useWidgets = helpers.defaultNullOpts.mkBool true "Whether to use widgets.";
152+
153+
mappings =
154+
helpers.defaultNullOpts.mkNullable
155+
(with types; attrsOf str)
156+
''
157+
{
158+
K = "click";
159+
"<CR>" = "click";
160+
gd = "go_to_def";
161+
gD = "go_to_decl";
162+
gy = "go_to_type";
163+
I = "mouse_enter";
164+
i = "mouse_leave";
165+
"<Esc>" = "clear_all";
166+
C = "clear_all";
167+
"<LocalLeader><Tab>" = "goto_last_window";
168+
}
169+
''
170+
"Mappings.";
171+
};
172+
173+
progressBars = {
174+
enable = helpers.defaultNullOpts.mkBool true ''
175+
Whether to enable the progress bars.
176+
'';
177+
178+
priority = helpers.defaultNullOpts.mkUnsignedInt 10 ''
179+
Use a different priority for the signs.
180+
'';
181+
};
182+
183+
stderr = {
184+
enable = helpers.defaultNullOpts.mkBool true ''
185+
Redirect Lean's stderr messages somehwere (to a buffer by default).
186+
'';
187+
188+
height = helpers.defaultNullOpts.mkPositiveInt 5 "Height of the window.";
189+
190+
onLines = helpers.mkNullOrOption types.str ''
191+
A callback which will be called with (multi-line) stderr output.
192+
193+
e.g., use:
194+
```nix
195+
onLines = "function(lines) vim.notify(lines) end";
196+
```
197+
if you want to redirect stderr to `vim.notify`.
198+
The default implementation will redirect to a dedicated stderr
199+
window.
200+
'';
201+
};
202+
203+
lsp3 =
204+
helpers.defaultNullOpts.mkNullable
205+
(
206+
with types;
207+
submodule {
208+
freeformType = types.attrs;
209+
options = {
210+
enable = helpers.defaultNullOpts.mkBool true ''
211+
Whether to enable the legacy Lean 3 language server ?
212+
213+
Set to `false` to disable, otherwise should be a table of options to pass to
214+
`lean3ls`.
215+
See https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#lean3ls
216+
for details.
217+
'';
218+
219+
on_attach = helpers.mkNullOrOption types.str "The LSP handler.";
220+
};
221+
}
222+
)
223+
"{}"
224+
"Legacy Lean3 LSP settings.";
225+
};
226+
227+
config = mkIf cfg.enable {
228+
extraPlugins = [cfg.package];
229+
230+
assertions = [
231+
{
232+
assertion =
233+
!(
234+
# leanls lsp server is disabled in nvim-lspconfig
235+
config.plugins.lsp.servers.leanls.enable
236+
# lsp is not (!) disabled in the lean.nvim plugin
237+
&& !(
238+
# lsp is explicitly set to `false`.
239+
(isBool cfg.lsp.enable)
240+
&& !cfg.lsp.enable
241+
)
242+
);
243+
message = ''
244+
You have not explicitly set `plugins.lean.lsp` to `false` while having `plugins.lsp.servers.leanls.enable` set to `true`.
245+
You need to either
246+
247+
- Remove the configuration in `plugins.lsp.servers.leanls` and move it to `plugins.lean.lsp`.
248+
- Explicitly disable the autoconfiguration of the lsp in the lean.nvim plugin by setting `plugins.lean.lsp` to `false`.
249+
250+
https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#leanls
251+
'';
252+
}
253+
];
254+
255+
extraPackages = optional (cfg.leanPackage != null) cfg.leanPackage;
256+
257+
extraConfigLua = let
258+
setupOptions = with cfg;
259+
{
260+
inherit lsp;
261+
ft = with ft; {
262+
inherit
263+
default
264+
nomodifiable
265+
;
266+
};
267+
abbreviations = with abbreviations; {
268+
inherit
269+
enable
270+
extra
271+
leader
272+
;
273+
};
274+
inherit mappings;
275+
infoview = with infoview; {
276+
inherit
277+
autoopen
278+
autopause
279+
width
280+
height
281+
;
282+
horizontal_position = horizontalPosition;
283+
separate_tab = separateTab;
284+
inherit indicators;
285+
lean3 = with lean3; {
286+
show_filter = showFilter;
287+
mouse_events = mouseEvents;
288+
};
289+
show_processing = showProcessing;
290+
show_no_info_message = showNoInfoMessage;
291+
use_widgets = useWidgets;
292+
inherit mappings;
293+
};
294+
progress_bars = with progressBars; {
295+
inherit
296+
enable
297+
priority
298+
;
299+
};
300+
stderr = with stderr; {
301+
inherit
302+
enable
303+
height
304+
;
305+
on_lines =
306+
helpers.ifNonNull' onLines
307+
(helpers.mkRaw onLines);
308+
};
309+
inherit lsp3;
310+
}
311+
// cfg.extraOptions;
312+
in ''
313+
require("lean").setup(${helpers.toLuaObject setupOptions})
314+
'';
315+
};
316+
}

0 commit comments

Comments
 (0)