Extension makes unhelpful automatic whitespace edits

[Coda-Coda]

Description

In certain circumstances (see steps to reproduce), the Lean 4 VSCode extension makes automatic changes to the whitespace in a .lean file, and there appears to be no option to disable this. While these typically may be helpful, when making changes to code that is under version control this can be unhelpful because it can introduce unnecessary changes (and would show up in pull requests etc). Ideally, being able to disable this in the Lean 4 VSCode settings would be ideal (if there is already an option, please point me to it - thanks). So far, I've found it necessary to temporarily disable the whole extension in order to make commits without these whitespace changes.

Context

This has come up for me while working on the NethermindEth/Clear code-base.

Steps to Reproduce

1. Run Lean 4: Project: Create Standalone Project... in VSCode.
2. Disable the Lean 4 Extension
3. Edit the file Basic.lean to contain the following:

theorem example₁ :
  42 < 100 := by
  sorry
  
theorem example₂ :
  False → True := by
  sorry

Note the two space characters on line 4.
4. Commit the changes
5. Enable the Lean 4 Extension
6. Add a space at the end of line 1
7. Lean 4 will have deleted the two spaces on line 4 automatically.
8. Revert the changes and repeat step 6 without the Lean 4 extension enabled (the spaces are not deleted).

Expected behavior:

The Lean 4 Extension should make these sorts of automatic whitespace changes optional, or not make them.

Actual behavior:

The whitespace changes happen automatically, with no documentation easy to find about how to disable them.

Versions

0.0.183
Lean (version 4.12.0, x86_64-unknown-linux-gnu, commit dc2533473114, Release)
NixOS unstable

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

---

Aside from this, I really do love the Lean VSCode extension, thanks for all your hard work on it!

[mhuisi]

You can override the defaults of the Lean 4 extension by opening your settings view in VS Code (File > Preferences > Settings), entering @lang:lean4 into the search bar at the top and then overriding the respective settings. In the 'Workspace' tab, you can also override these on a per-workspace basis.

I'll add a note in the manual about this.

Generally speaking, I would still recommend keeping these settings at their defaults - once the code in your project has been normalized once, you are less likely to see redundant whitespace changes in your PRs and diffs. Experience shows that having this setting enabled is a no-brainer in languages where trailing whitespace isn't semantically relevant.

[Coda-Coda]

Awesome! Thank you so much @mhuisi for the timely and thorough response. Works perfectly. Much appreciated 😃