normalising whitespace

Stream: lean4

[Scott Morrison]

@Mac Malone @Marc Huisinga

In Mathlib we have a .vscode/settings.json file containing:

{
  "editor.insertSpaces": true,
  "editor.tabSize": 2,
  "editor.rulers" : [100],
  "files.encoding": "utf8",
  "files.eol": "\n",
  "files.insertFinalNewline": true,
  "files.trimFinalNewlines": true,
  "files.trimTrailingWhitespace": true,
}

Mostly this is basic whitespace normalisation. I would really like to see this effortlessly become the defaults in all new projects.

Take a moment, for example, to look at @Patrick Massot trying to help Terry Tao, but there are spurious whitespace changes everywhere: https://github.com/teorth/symmetric_project/pull/8/files. Not cool!

It seems there are two ways we could achieve this:

• Can the VSCode extension just change the defaults to these for Lean files?
• If not, can the standard lake new template include these?

We need some fix for this.

[Mac Malone]

@Scott Morrison One question here is what about users using other editors (e.g., EMACS or neovim)? Having inconsistency between editor configurations seems like it would cause just as much confusion.

[Scott Morrison]

I think I'd just quote Leo's recent statement about the primacy of VSCode. :-)

[Scott Morrison]

I mean, of course we can suggest that the maintainers of those editor extensions coordinate.

[Scott Morrison]

But I don't think we should wait on them.

[Scott Morrison]

I admit I don't know who maintains the emacs and neovim extensions; anyone who does know could ping them here!

[Mac Malone]

I believe @Julian Berman is responsible for the neovim extension and I believe @Sebastian Ullrich is at least a major contributor to the EMACS extension.

[Julian Berman]

lean.nvim already defaults to all of that besides auto-trimming whitespace FWIW.

[Mac Malone]

One other concern I have is there exist a number of pitfalls when it comes to committing the .vscode folder. Folder settings cannot be extended and override user settings. Thus, if a user has extensions that need to be configured via the settings.json and are local to a machine it is hard to do so. The only workaround I know for this is to create VSCode workspace for the file (i.e., a .codw-workspace file) -- though I am not sure if there are any limitations to that solution. See, for example, this StackOverflow question which has some extensive discussion of the pros and cons of this in the anwers and comments.

[Julian Berman]

We have some control over extensions installed during VSCode setup right? Maybe installing the editorconfig extension and putting those settings there solves some of that (though I haven't read that thread fully honestly)

[Siddhartha Gadgil]

Scott Morrison said:

But I don't think we should wait on them.

To state the obvious, we can safely assume that users of editors other than VScode are experts (i.e., computer experts, not necessarily Lean experts) so changes to reduce errors can prioritize VS code.

[Marc Huisinga]

vscode-lean4#341 adjusts the defaults for whitespace.

[Marc Huisinga]

If we find that users commonly have user settings configured that override these defaults in undesirable ways, we can revisit the question of whether we want to generate a settings.jsonthat overrides their own settings entirely.

[David Thrane Christiansen]

Generating a default editorconfig file with the desired settings seems like a nice improvement as well

[Marc Huisinga]

I think that an editorconfig file may be better generated in lake, because users of other editors are unlikely to use VS Code to initialize their project.

[David Thrane Christiansen]

I agree - I had thought that VSCode used Lake to set up the projects, but I suppose I was wrong

[Marc Huisinga]

David Thrane Christiansen said:

I agree - I had thought that VSCode used Lake to set up the projects, but I suppose I was wrong

VS Code uses Lake to set up projects, but the new VS Code commands do a few other things beyond just calling the lake command. One of these things could be to also initialize it with a settings.json (vscode-lean4#325), but if we go the editorconfig route, it should definitely be lake that sets it up.

[Mac Malone]

I think editorconfig route sounds like a good idea. However, I have never used it before. What do we want the default file to look like?

[Marc Huisinga]

Mac Malone said:

I think editorconfig route sounds like a good idea. However, I have never used it before. What do we want the default file to look like?

The editorconfig extension supports six properties, which are coincidentally almost exactly those that are used by mathlib4, so we should probably just assign them in this way.