Default editor settings in lakefile

Stream: lean4

[Patrick Massot]

Various Lean project ship with defaut VSCode settings, for instance saying whether the “expected type” panel is open by default, or whether to emphasize the first goal. See for instance https://github.com/leanprover-community/mathematics_in_lean/blob/master/.vscode/settings.json#L38-L39. This is especially relevant to projects aimed at beginners. We could try to ship those projects with a file talking to emacs and one talking to vim.

But maybe it would be nicer to have something editor-agnostic, for instance in the lakefile. I’m really not sure, but I think this is worth discussing. Note that with lakefile.toml when we don’t even need much cooperation from Lean itself, we could simply drop some editor_settings configuration section and let editors read it, after defining a couple of fields that can be in this section. It could even be open-ended, with editors ignoring settings they don’t understand.

@Mac Malone @Marc Huisinga

[Marc Huisinga]

I don't think editor plugins should standardize on a set of configuration options for Lean 4. It doesn't seem like much of a benefit anyways, given that the only two plugins with extensive support are the VS Code and NeoVim plugins.

[Marc Huisinga]

In any case, something like this should definitely not be part of the Lakefile. The semantics of the Lakefile depend on the Lean version of your project. The semantics of editor plugin settings depend on the plugin version.

[Patrick Massot]

Ok, that’s a good point.

[Patrick Massot]

But, as far as I know, we do nothing to enforce an editor plugin version when writing those .vscode/settings.json.