Accessing argv[0]

Stream: lean4

[Eric Wieser]

Is it possible to access argv[0] in lean? As I read it, src#Lean.IR.EmitC.emitMainFn only propagates argv[1] onwards to the arguments to def main.

[Eric Wieser]

(As for the behavior of lean --run, this could set argv[0] to the path to the lean source file, like python -m does)

[Eric Wieser]

If it's too late to change the signature of main (which would be very unfortunate, since it currently diverges from Python, C, and Rust), then I suppose this could be exposed by IO.progName : IO String?

[Sebastian Ullrich]

Yes, that may be the most reasonable addition at this point. Do you have a use case where appPath (sp?) is not sufficient?

[Eric Wieser]

Yes, in my use case the generated binary is symlinked from multiple locations, and I need to know which symlink my binary was invoked from

[Eric Wieser]

(I think appPath fully resolved the symlink when I tried it)

[Henrik Böving]

Eric Wieser said:

Yes, in my use case the generated binary is symlinked from multiple locations, and I need to know which symlink my binary was invoked from

Note that this is a very general use case, for example busybox "single binary all UNIX utils" trick works like this. So from a PL perspective we definitely want this feature in some way.

[Eric Wieser]

It looks like Haskell's design is close to lean; getArgs does not include argv[0], which is instead in getProgName

[Eric Wieser]

So I retract any implication that Lean has made a wrong turn here; this is a missing feature not a design flaw :)

[Eric Wieser]

Perhaps another solution is to allow def main (progName : String) (args : List String) : IO _

[Eric Wieser]

Though making progName available globally monadically like it is in Haskell would be convenient for me

[Eric Wieser]

Filed as lean4#5819

[Eric Wieser]

And a working patch at lean4#5820