best practice for running `lake` in a subdirectory.

Stream: lean4

[Scott Morrison]

I'm currently doing some benchmarking, where it feels natural to work deep in some subdirectory, but to be able to run lean files there.

Currently I have to jump back out to the main project directory, then run lake env lean path/to/my/file.lean.

Is there a way to stay in that directory, but either point lake to the right project root, or have it automatically walk up the directory hierarchy until it finds one? ( :ping_pong: @Mac Malone)

[Mario Carneiro]

does either lake env lean path/to/my/file.lean or lake env lean file.lean work when the cwd is path/to/my/?

[Mario Carneiro]

also lake -d=../../.. env lean file.lean

[Scott Morrison]

That last one works, thanks!

[Scott Morrison]

(The first two don't.)

[Scott Morrison]

Automatically walking up would be lovely, if it doesn't cause problems.

[Mario Carneiro]

I agree that it should walk up by default (according to the "what would rust do" principle)

[Mac Malone]

@Scott Morrison Feel to post walking up as a feature request issue. Seems like a nice to have.