Why does `IO.currentFile` not exist?

Stream: lean4

[Michiel Huttener]

We have IO.currentDir which returns the name of the current directory, but there seems to be no (native) way to let Lean return the current file name.

[Julian Berman]

That'd be a slightly funny kind of "false friend" naming for such a thing to me, as the two concepts are not terribly related (one is a thing which is related to any process on a machine, the other is some programming-language-specific concept which isn't always well defined). I agree that I did expect to find such a function somewhere just now, all the languages I know of have one, but amusingly it seems Haskell seems maybe to not have one either unless you're using template haskell?

[Arthur Paulino]

Isn't it IO.appPath?

[Paul Lezeau]

If you have acceess to the CoreM monad you can access Lean.Core.Context.fileName

[Kyle Miller]

It makes senes for this to be in a "meta" monad rather than IO since the currently-processed file is a compile-time concern, not a runtime concern. (Assuming Paul's interpretation that "current file name" means the current Lean file is correct.)

[Michiel Huttener]

Aha I see! Thanks for the clarification.

For completeness, a MWE that shows the differences. (Fun to see in the web editor as well!)

import Lean

open Lean IO

 -- IO
#eval currentDir
#eval appDir
#eval appPath

-- very meta
#eval getFileName

[Michiel Huttener]

Oh wait, the getFileName above is Lean.MonadLog.getFileName and has nothing to do with Lean.Core.Context.fileName, and I don't see how one can get the context in CoreM.
Nevermind: there is an instance

[Eric Wieser]

Arthur Paulino said:

Isn't it IO.appPath?

Arguably it's argv[0], but Lean only passes argv[1:] to def main (lean4#5819)

[Markus Himmel]

If you want argv[0] and have a recent Lean you can use docs#Std.Internal.IO.Process.getExecutablePath (it will move out of Internal later this year). I don't know whether this ever returns something different from docs#IO.appPath.

[Eric Wieser]

I guess the test is what exec -a secret_name ./lake/build/bin/foo does, which appPath didn't previous respect