Feature request - button to replace with minimized imports

Stream: lean4

[Seewoo Lee]

Would it be possible to add a small button in VSCode extension for #min_imports, where clicking it automatically replaces all the imports with minimized imports? (I always copy-paste manually.)

[Damiano Testa]

It might be possible to make it produce a Try this suggestion.

[Seewoo Lee]

I left this as an issue in vscode-lean4.

[Henrik Böving]

That's not really an issue for vscode-lean4, #min_imports is mathlib code.

[Seewoo Lee]

Oops sorry, then where should I ask this? Issue in actual mathlib? I don't know much about how other Try this suggestions works in vscode extension.

[Damiano Testa]

Here is a possible implementation: I called it #min_imports' simply to distinguish it from the other.

import ImportGraph.Meta
import Lean.Meta.Tactic.TryThis

open Lean Elab Command Parser Meta.Tactic.TryThis in
elab "#min_imports'" : command => do
  let imports := (← getEnv).minimalRequiredModules.qsort (·.toString < ·.toString)
    |>.toList.map (s!"import {·}")
  let newImports := "\n".intercalate imports
  let fm ← getFileMap
  let (imps, _) ← parseHeader {inputString := fm.source, fileName := ← getFileName, fileMap := fm}
  liftTermElabM do addSuggestion (origSpan? := imps) (← getRef) newImports

#min_imports'

[Damiano Testa]

Note that if the imports are interspersed with comments, those will get erased by the Try this suggestion.

[Damiano Testa]

Leading/trailing comments are preserved, though.

[Damiano Testa]

-- survives `Try this`
import Lean -- this comment gets erased
import Mathlib -- this comment also survives

[Kim Morrison]

The new shake will do a much better job than #min_imports, which is essentially obsolete now. Once we're actually shipping the new shake we will probably add a VSCode extension menu item for it.