Lean4 autocomplete

Stream: new members

[Vasily Ilin]

I get no autocomplete in Lean4 in VS Code. Has it just not been implemented yet? I relied on autocomplete in Lean3 to find relevant theorems.

[Patrick Massot]

Auto-complete does not work with imports yet but it definitely works with lemma names.

[Vasily Ilin]

lemma names from the current namespace?

[Damiano Testa]

This is a little hacky, but it does produce a form of "autocomplete":

import Std.Tactic.TryThis

namespace Mathlib.Tactic.imp

open Lean Elab Command FuzzyMatching

/--  A syntax that allows strings to be printed without surrounding them by guillemets `«...»`. -/
declare_syntax_cat write_me_output_stx

@[inherit_doc Parser.Category.write_me_output_stx]
syntax "import " ident : write_me_output_stx

/-- `imp <string>` tries to find a file matching `Mathlib.<string>`.
It prints a list of candidates, taking the names from `Mathlib.lean`.
If there is only one candidate, it suggests `import Mathlib.<uniqueCandidate>` as a `Try this`.

Using `imp! <string>` uses fuzzy-matching, rather than exact matching. -/
elab (name := commandImp!) tk:"imp" fz:("!")? na:(colGt ident) : command => do
  let inp := na.getId.toString
  let dat := (← IO.FS.lines "Mathlib.lean").map (String.drop · 15)
  let cands := dat.filter <| (if fz.isSome then fuzzyMatch else String.isPrefixOf) inp
  match cands.toList with
    | [] => throwErrorAt tk "no available imports"
    | [imp] =>
      let impS ← Lean.moduleNameOfFileName ("Mathlib/" ++ imp.replace "." "/" ++ ".lean") none
      let imp : TSyntax `write_me_output_stx ← `(write_me_output_stx| import $(mkIdent impS))
      let stx ← getRef
      liftTermElabM do
        Std.Tactic.TryThis.addSuggestion stx imp
    | cl => logInfoAt tk <| "\n".intercalate cl

@[inherit_doc commandImp!]
macro "imp!" na:(colGt ident) : command => `(command| imp ! $na)

end Mathlib.Tactic.imp

--  Here is how it works: typing
imp Data.ENat
-- produces
/-
Data.ENat.Basic
Data.ENat.Lattice
-/

-- typing
imp Data.ENat.L
--  produces
/-
Try this: import Mathlib.Data.ENat.Lattice
-/

imp! DtaENB
--  fuzzy matching!  produces
/-
Try this: import Mathlib.Data.ENat.Basic
-/

[Patrick Massot]

Damiano, you are not answering Vasily, are you?

[Damiano Testa]

Ah, I was answering your "Auto-complete does not work with imports yet"...

[Patrick Massot]

Yes, I understand.

[Patrick Massot]

This is nice, but we really need proper support from the Lean server.

[Damiano Testa]

Actually, I had this command a while ago, since I wanted it, so I thought of posting it here.

[Damiano Testa]

(In case others find it useful before proper support arrives!)

[Eric Wieser]

Is there a lean4 issue for this autocomplete? It so, it would maybe be a good place to keep Damiano's workaround.

[Damiano Testa]

I looked at the issues, but I could not find one about autocomplete imports. I remember the issue coming up a few times on Zulip, though.

[Marc Huisinga]

There's no issue in the Lean 4 repository for import auto-completion, but feel free to create one.

[Damiano Testa]

I just found out that there is a fuzzy-match algorithm in Lean, so I added fuzzy-matching capabilities to the auto-complete above! Now, if you type

imp! <string>

you will get real-time fuzzy-matching of <string> against all files in Mathlib and a Try this: import ... whenever there is a unique file fuzzy-matching your input.

[Utensil Song]

Users might expect imp? due to simp? etc.

[Utensil Song]

It seems that I have to change to IO.FS.lines "lake-packages/mathlib/Mathlib.lean" to use it, and why is Try this not clickable?

image.png

[Patrick Massot]

I don't think it's a good idea to invest more time in this workaround. I trust Marc to bring us the right solution in a not too distant future.

[Damiano Testa]

@Utensil Song, changing the ! to ? is no issue at all! Your other suggestion is easy to implement, but I only wrote this command thinking that it would help locate a single import and propose to import that one.

Anyway, as Patrick already mentioned, I had not intended this to be particularly robust or long-lived: it is a very short hack, while we wait for proper auto-complete support!

[Damiano Testa]

In fact, I would say that users should expect Ctrl-Space, rather than having to call a command!

[Utensil Song]

I fiddled with it a bit and got a clickable list:

Code

import Std.Tactic.TryThis

namespace Mathlib.Tactic.imp

open Lean Elab Command FuzzyMatching System

/-- Infer module name of source file name. -/
def moduleNameOfFileName (fname : FilePath) (rootDir : Option FilePath) : IO Name := do
  let fname ← IO.FS.realPath fname
  let rootDir ← match rootDir with
    | some rootDir => pure rootDir
    | none         => IO.currentDir
  let mut rootDir ← realPathNormalized rootDir
  if !rootDir.toString.endsWith System.FilePath.pathSeparator.toString then
    rootDir := ⟨rootDir.toString ++ System.FilePath.pathSeparator.toString⟩
  if !rootDir.toString.isPrefixOf fname.normalize.toString then
    throw $ IO.userError s!"input file '{fname}' must be contained in root directory ({rootDir})"
  -- NOTE: use `fname` instead of `fname.normalize` to preserve casing on all platforms
  let fnameSuffixComponents := fname.withExtension "" |>.components.drop (rootDir.components.length + 1)
  let modName    := fnameSuffixComponents.foldl Name.mkStr Name.anonymous
  pure modName

/--  A syntax that allows strings to be printed without surrounding them by guillemets `«...»`. -/
declare_syntax_cat write_me_output_stx

@[inherit_doc Parser.Category.write_me_output_stx]
syntax "import " ident : write_me_output_stx

/-- `imp <string>` tries to find a file matching `Mathlib.<string>`.
It prints a list of candidates, taking the names from `Mathlib.lean`.
If there is only one candidate, it suggests `import Mathlib.<uniqueCandidate>` as a `Try this`.

Using `imp! <string>` uses fuzzy-matching, rather than exact matching. -/
elab (name := commandImp!) tk:"imp" fz:("!")? na:(colGt ident) : command => do
  let inp := na.getId.toString
  let dat := (← IO.FS.lines "lake-packages/mathlib/Mathlib.lean").map (String.drop · 15)
  let cands := dat.filter <| (if fz.isSome then fuzzyMatch else String.isPrefixOf) inp

  liftTermElabM do
    cands.toList.forM fun imp => do
      let impS ← moduleNameOfFileName ("lake-packages/mathlib/Mathlib/" ++ imp.replace "." "/" ++ ".lean") none
      let imp : TSyntax `write_me_output_stx ← `(write_me_output_stx| import $(mkIdent impS))
      let stx ← getRef
      Std.Tactic.TryThis.addSuggestion stx imp


@[inherit_doc commandImp!]
macro "imp!" na:(colGt ident) : command => `(command| imp ! $na)

end Mathlib.Tactic.imp

imp! Ring

But I'm mostly struggled with the path prefix "lake-packages/mathlib" issue (I hacked my way through it but unsatisfied), do you have any idea why?

[Utensil Song]

Sure, better not to invest more time in this, but I was curious of the implementation so I fiddled with it a bit.

[Damiano Testa]

I understand: the reason I wrote this, was mostly to teach myself something about meta-programming, syntax and dealing with files in Lean.

[Utensil Song]

Now you have taught me (the interesting combination) :grinning:

[Damiano Testa]

On my computer, this line

  let dat := (← IO.FS.lines "lake-packages/mathlib/Mathlib.lean").map (String.drop · 15)

introduces lake-packages/mathlib/ which upsets the command. If I use

  let dat := (← IO.FS.lines "Mathlib.lean").map (String.drop · 15)

instead, then I get

imp! Ring
/-
Try this: import BigOperators.Ring
Try this: import BigOperators.RingEquiv
Try this: import Category.BoolRing
Try this: import Category.ModuleCat.ChangeOfRings
...
-/

[Damiano Testa]

(I removed both occurrences of lake-packages/mathlib/)

[Utensil Song]

On my Mac without them it just keeps complaining

no such file or directory (error code: 2)
  file: Mathlib.lean

So I need both of them to make it work:

image.png

[Damiano Testa]

Ok, I think that this is all the more reasons for preferring a more robust solution! Anyone should feel free to modify and use the code above, but I wouldn't even have guessed that what you reported could have been an issue...

[Damiano Testa]

By the way, Scott opened an issue for autocompletion of imports: Lean4 issue #2655.