leanprover-community
add nice VSCode settings
some people have useful settings in their local VSCode config, while the rest of us don't touch it because we don't want to break anything. can anyone that has nice local settings propose them in a PR?
see this zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/VSCode.3A.20apostrophe.20is.20part.20of.20a.20word/near/202055397
Some settings (like wordSeparators) could potentially go in the vscode-lean repo instead so that people have access to them by default when working on Lean projects outside mathlib.
There's also a thread with some useful snippets which should be shared in one of these places: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/vscode.20snippets
Having \<\> missing from wordSeparators has caused me a lot of frustration - since it's a language feature, it seems like it's fair game to put in vscode-lean.
Can we have "editor.acceptSuggestionOnEnter": "off", --- it's useless in Lean, as far as I understand.
I'm not sure where to put this --- somewhere in the vscode-lean repository?
Oh, that's actually a good question. I guess we could write a command in the VS Code extension that copies some convenient settings to the users settings.json or a per-project settings.json?
If there's anything that can be done in the vscode-lean extension, please file a PR!
Having
\<\>missing fromwordSeparatorshas caused me a lot of frustration
We already exclude ⟨ and ⟩ from the wordPattern. I'm not sure what else we can do in the extension. If you know how to fix it, please file a PR!
I guess we could write a command in the VS Code extension that copies some convenient settings to the users
settings.json
I think we could start with a more low-tech solution: how about we collect these settings in the mathlib repository and tell people to copy&paste it from here?
Opened https://github.com/microsoft/vscode/issues/102942 about what the recommended way to provide setting defaults from language extensions is.