VSCode Lean 4 Code Actions

Installation

Note: a custom language configuration is available as a separate extension.

Actions

Disclaimer: the commands currently operate directly on text. As such, they have many limitations - for example, sometimes they don't properly detect Lean names. We have plans to reimplement the commands as proper code actions within LSP that operate on Syntax instead of text.

Snippets

  • imp - expands to configured imports
  • op - expands to configured opens
  • ns - expands to namespace ${currentFileName}
  • nsp - expands to namespace ${currentFilePath}
  • var - expands to variable (${name} : ${Type})
  • ind - expands to inductive declaration
  • struct - expands to structure declaration
  • cls - expands to class declaration

Configuration options

  • lean4CodeActions.registerRenameProvider - use this extension as a rename provider for .lean files
  • lean4CodeActions.updateImportsOnFileRename - update imports in other files when a file is renamed
  • lean4CodeActions.namespace.prefix - a prefix for top-level namespaces in generated code (added as ${prefix}.${body})
  • lean4CodeActions.createNewFile.imports - a list of Lean filenames to be imported.
  • lean4CodeActions.createNewFile.opens - a list of Lean namespaces to be opened.
  • lean4CodeActions.createNewFile.derivings - a list of Lean names to be derived.
  • lean4CodeActions.defaultLib - the default library to be used when creating a new file. If it's empty, the extension will ask you to choose the library interactively.

Related work

Create a new file

Before:

(Nothing)

After:

File: CodeActions/Test/CreateNewFile/User.lean

namespace CodeActions.Test.CreateNewFile

structure User where

deriving Repr, Inhabited

namespace User

Notes:

  • This command supports adding import, open and deriving instance commands via configuration.

Auto-import

Before:

def x : Rat := 1.0

After:

import Std.Data.Rat.Basic

def x : Rat := 1.0

Gotchas:

  • If you execute this command with an empty selection (just a cursor on the name), then only the part captured by getWordRangeAtPosition will be used. To import a hierarchical name, select it fully, then execute the command. Alternatively, you can enable detection of hierarchical names by installing a custom language configuration.

Update imports on rename

When you rename a file (or move it to another folder), it updates the imports in other files.

Before:

File 1: CodeActions/Test/UpdateImports/Child.lean

namespace CodeActions.Test.UpdateImports.Child

def x : Nat := 1

File 2: CodeActions/Test/UpdateImports/Parent.lean

import CodeActions.Test.UpdateImports.Child

namespace CodeActions.Test.UpdateImports.Parent

def y : Nat := 2 * Child.x

After:

File 1: CodeActions/Test/UpdateImports/Nested/RenamedChild.lean

namespace CodeActions.Test.UpdateImports.Child

def x : Nat := 1

File 2: CodeActions/Test/UpdateImports/Parent.lean

import CodeActions.Test.UpdateImports.Nested.RenamedChild

namespace CodeActions.Test.UpdateImports.Parent

def y : Nat := 2 * Child.x

Notes:

  • This is a listener, not a command - it is executed automatically upon a file rename. It works even if you rename a file via another extension (File Utils, File Bunny).
  • It doesn't update the namespaces (should be done manually).
  • It can be disabled by setting lean4CodeActions.updateImportsOnFileRename to false

Set argument style

Before:

(α : Type u)

After:

{α : Type u}

Notes:


Extract a definition to a separate file

Before:

File 1: CodeActions/Test/ExtractDefinition/Book.lean

namespace CodeActions.Test.ExtractDefinition

structure Author where
  name : String

structure Book where
  authors : List Author 

After:

File 1: CodeActions/Test/ExtractDefinition/Book.lean

import CodeActions.Test.ExtractDefinition.Author

namespace CodeActions.Test.ExtractDefinition

structure Book where
  authors : List Author 

File 2: CodeActions/Test/ExtractDefinition/Author.lean

namespace CodeActions.Test.ExtractDefinition

structure Author where
  name : String

namespace Author

How it works:

  • It extracts a definition into a separate file
  • It adds an import to the original file

Gotchas:

  • It doesn't add the open command yet

Find-replace the current word within a code block

Before:

def foo : IO String := do
  let text ← IO.FS.readFile "/tmp/secrets"
  return text

After:

def foo : IO String := do
  let secrets ← IO.FS.readFile "/tmp/secrets"
  return secrets

You can use it to rename a local binding (if the variable name is a unique string of characters across the code block).

Gotchas:

  • It's a simple find-replace: it doesn't distinguish between variables and text within strings, for example.
  • It's activated via "Rename Symbol" native command. If it causes problems, you can disable it by setting lean4CodeActions.registerRenameProvider to false in the extension configuration.
  • It relies on getWordRangeAtPosition to detect the word under cursor. You can improve the detection by installing a custom language configuration.

Notes:

  • A code block is defined as a continuous list of non-blank lines.

Convert a text block to a list of strings

Before:

foo
bar
xyz

After:

"foo",
"bar",
"xyz"

Each line becomes an element of the list.