Zulip Chat Archive

Stream: new members

Topic: Lean4 autocomplete

Vasily Ilin (Oct 09 2023 at 19:50):

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 (Oct 09 2023 at 19:51):

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

Vasily Ilin (Oct 09 2023 at 19:54):

lemma names from the current namespace?

Damiano Testa (Oct 09 2023 at 20:42):

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

-- 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 (Oct 09 2023 at 20:44):

Damiano, you are not answering Vasily, are you?

Damiano Testa (Oct 09 2023 at 20:44):

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

Patrick Massot (Oct 09 2023 at 20:45):

Yes, I understand.

Patrick Massot (Oct 09 2023 at 20:45):

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

Damiano Testa (Oct 09 2023 at 20:45):

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

Damiano Testa (Oct 09 2023 at 20:46):

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

Eric Wieser (Oct 09 2023 at 20:52):

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

Damiano Testa (Oct 09 2023 at 21:06):

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 (Oct 10 2023 at 07:34):

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

Damiano Testa (Oct 10 2023 at 19:41):

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 (Oct 11 2023 at 14:02):

Users might expect imp? due to simp? etc.

Utensil Song (Oct 11 2023 at 14:13):

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?


Patrick Massot (Oct 11 2023 at 14:40):

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 (Oct 11 2023 at 15:50):

@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 (Oct 11 2023 at 15:51):

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

Utensil Song (Oct 11 2023 at 15:55):

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


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 (Oct 11 2023 at 15:57):

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 (Oct 11 2023 at 15:58):

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 (Oct 11 2023 at 15:58):

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

Damiano Testa (Oct 11 2023 at 16:03):

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 (Oct 11 2023 at 16:04):

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

Utensil Song (Oct 11 2023 at 16:06):

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:


Damiano Testa (Oct 11 2023 at 16:13):

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 (Oct 11 2023 at 20:37):

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

Last updated: Dec 20 2023 at 11:08 UTC