determine imports of current file

Stream: general

[Scott Morrison]

Is there an API to determine the imports of the current file? It seems you could almost, but not quite, determine this information from judicious use of environment.decl_olean.

[Scott Morrison]

It would be lovely to have a linter that reduced unnecessary imports.

[Patrick Massot]

Last time I asked this wasn't possible.

[Patrick Massot]

But that was Lean3.4.2 time.

[Scott Morrison]

I think there might be a crazy hack, that would rely on adding a few extra lines at the end of every file (i.e. so might be usable in a script)

[Scott Morrison]

But if we can expose it directly, even better.

[Johan Commelin]

Simon had tools for this with olean-rs, right?

[Johan Commelin]

At some point this was even part of CI, I think

[Gabriel Ebner]

We already have functions that allow you to import modules into an environment, but apparently none that tells you the dependencies.