auto imports

Stream: lean4

[Maxime Riché]

I am new to Lean... I am working with LLM in generating Lean4 code. I am using datasets containing theorems but the imports are not provided.

Is there an existing solution to automatically add the necessary imports?

[Matthew Ballard]

You could try import Mathlib at the top.

[Edward van de Meent]

and end with #min_imports to minimise the required imports

[Kyle Miller]

It would be pretty neat to have some autoimport mechanism, where "unknown identifier" could trigger reading all the oleans and reporting modules that might provide a relevant declaration. I don't know if this is practical, but it would be a nice UX improvement.

[Shreyas Srinivas]

Haskell and rust do this already. So I have to ask why it wouldn't be feasible?

[Arthur Paulino]

I'm pretty sure it's feasible and just a matter of prioritization

[Henrik Böving]

Kyle Miller said:

It would be pretty neat to have some autoimport mechanism, where "unknown identifier" could trigger reading all the oleans and reporting modules that might provide a relevant declaration. I don't know if this is practical, but it would be a nice UX improvement.

You don't actually have to read all the oleans. The ilean files should contain all of this information already and they should be loaded by the LSP I think? At least I don't know how the LSP would provide symbol search for stuff that you haven't yet imported otherwise. So the key component that is left here is integrating it with the autocompletion mechanism.

[Henrik Böving]

Arthur Paulino said:

I'm pretty sure it's feasible and just a matter of prioritization

Yes, there is lots of other things to be worked on the LSP and VSCode plugin as well.

[Kyle Miller]

These are the questions that come to mind:

• How does an open Lean project know everything that could potentially be imported?
• Can you load the declaration names quickly enough that it wouldn't create unacceptable UI delay?
• Is having just declaration names sufficient? Do we need to worry about missing opens or unprocessed export commands? What about dot notation?
• Can this be done from within a lazy message, so that all this processing only happens when a user actually looks at it? Perhaps there are macro tactics out there that depend on name resolution failing fast?

[Henrik Böving]

Question 1 and 2 is already answered by the fact that you can do symbol search from a plain project that doesn't import Lean within the Lean namespace. The answer to number 1 in particular is most likely that you can just look up all ilean files that are available on the SEARCH_PATH and that should be everything you can ever import.

The rest do get more interesting yes.

[Shreyas Srinivas]

The answer to 3 is to either use fully qualified names which are truncated upto the current namespace

[Shreyas Srinivas]

Or add more complex code to open namespaces

[Kyle Miller]

That's a possible answer, but it would take some work to validate it. Plus, it's likely that there needs to be some additional support (if it doesn't already exist for ileans) to be able to find exported names.

[Shreyas Srinivas]

You can always cache them as a symbol table with an index that is updated when a new dependency is added or there is an update

[Maxime Riché]

Thanks a lot @Matthew Ballard and @Edward van de Meent ! I will try your solution