Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: current file name


Eric Wieser (Jul 06 2022 at 09:52):

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

Bart Michels (Jul 06 2022 at 11:56):

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

Eric Wieser (Jul 06 2022 at 12:21):

Ah sorry, I'm asking about Lean 3

Alex J. Best (Jul 06 2022 at 14:38):

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 (Jul 06 2022 at 14:46):

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

Eric Wieser (Jul 06 2022 at 14:47):

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

Damiano Testa (Jul 06 2022 at 14:55):

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 (Jul 06 2022 at 15:06):

Yeah, that was the closest thing I found

Eric Wieser (Jul 06 2022 at 15:07):

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

Damiano Testa (Jul 06 2022 at 18:10):

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?


Last updated: Dec 20 2023 at 11:08 UTC