Minimal VSCode config.

vscode.md

The most important setting

The VSCode binary available on the official website IS NOT FREE SOFTWARE ("free" as in "freedom"). The binary there is under a proprietary license. VSCode's source code is under the MIT license, but the MIT license allows binaries to be redistributed under a proprietary license.

Free distributions of VSCode exist, namely Code OSS and VSCodium. However, Code OSS ships the default VSCode configuration, meaning it comes with telemetry enabled and SENDS USAGE DATA TO MICROSOFT. VSCodium comes with telemetry disabled. Therefore, I recommend using VSCodium.

With that in mind, whatever VSCode distribution you choose, the most important setting in this guide is:

"telemetry.telemetryLevel": "off"

Appearance

The fonts are the ones recommended by vscode-lean because of their good Unicode support.

"window.titleBarStyle": "custom",
"workbench.colorTheme": "Default Dark+",
"editor.fontFamily": "Source Code Pro Medium, DejaVu Sans Mono",
"editor.bracketPairColorization.enabled": false,
"editor.guides.indentation": false

Vim mode

Install VSCode Neovim to make VSCodium behave like Vim. Setting keyboard.dispath to keyCode is necessary if you have custom keybindings (e.g. binding caps lock to escape).

"vscode-neovim.neovimExecutablePaths.linux": "/usr/bin/nvim",
"keyboard.dispatch": "keyCode"

To make ctrl+j and ctrl+m behave properly, some custom keybindings are necessary (see this issue).

{
    "key": "ctrl+j",
    "command": "editor.action.insertSnippet",
    "when": "editorTextFocus && neovim.mode == 'insert'",
    "args": {
        "snippet": "\n"
    }
},
{
    "key": "ctrl+m",
    "command": "editor.action.insertSnippet",
    "when": "editorTextFocus && neovim.mode == 'insert'",
    "args": {
        "snippet": "\n"
    }
},
{
    "key": "ctrl+j",
    "command": "vscode-neovim.send",
    "when": "neovim.mode != 'insert' && neovim.mode != 'normal'",
    "args": "<NL>"
},
{
    "key": "ctrl+m",
    "command": "vscode-neovim.send",
    "when": "neovim.mode != 'insert'",
    "args": "<CR>"
}

Lean mode

Install vscode-lean to enable support for the Lean programming language and theorem prover. I recommend binding the input leader to something more ergonomic.

"lean.input.leader": ";"

I also recommend a keybinding for pausing the information view.

{
    "key": "ctrl+k",
    "command": "lean.infoView.toggleUpdating"
}