current file name

Stream: metaprogramming / tactics

[Eric Wieser]

Is there any way to get the name / path of the current file?

[Bart Michels]

Maybe this line or a similar @[extern] declaration? https://github.com/leanprover/lean4/blob/fc7c1d105390dbc47e2ff36d4d2dd3b60defe48e/src/Init/System/IO.lean#L293

[Eric Wieser]

Ah sorry, I'm asking about Lean 3

[Alex J. Best]

No such thing exists in general, lean works perfectly fine in an unsaved buffer on vscode for example, what do you need it for?

[Eric Wieser]

I want to ask "is this file part of my current leanpkg project"

[Eric Wieser]

Or more precisely "does this filename string I have come from the same leanpkg project as the metaprogram asking the questions"

[Damiano Testa]

Maybe you already know about this, but there is docs#environment.in_current_file (and docs#declaration.in_current_file), that returns none if the declaration is not in an imported file. If you know that your declaration is either imported or in the current file, having none means that it is in the current file.

If I understand correctly, the commands read the olean files to determine the answer.

[Eric Wieser]

Yeah, that was the closest thing I found

[Eric Wieser]

But as an example, what if I want to exclude all declarations in a directory and not just in a particular file?

[Damiano Testa]

Is the issue that you want to exclude all declarations in the same folder as the one in a given file? This would be easy if you knew the path beforehand, right? E.g. if you were working in an "import all" file?