RFC: `_lake` vs `.lake`

Stream: lean4

[Mac Malone]

Lake-related output files will be stored in a dedicated Lake directory in the near future (lean4#2749) and one design decision that is unclear is what is the best name for the directory. I have discussed this with a few people and the there has not been a clear answer on which of _lake or .lake is the better. .lake would make it a hidden directory on Unix operating systems while _lake would not be, and it is not clear whether or not this is desirable. What does the Lean community at large think? Vote below.

[Mac Malone]

/poll What is the best name for the Lake directory?
_lake
.lake

[Eric Wieser]

(one data point against . is that python uses __pycache__ not .pycache)

[Johan Commelin]

Does python explain why they made that choice?

[Mario Carneiro]

they just really like dunder

[Sebastian Ullrich]

I don't think that .lake is desirable or a good look for programming. bin/ is the main output of interest for these users of Lean so it really shoudn't be put in a hidden directory. I consider this more important than the very slight inconvenience of listing one more directory item for other uses (but recall that it will be two fewer items than today!). /cc @Joe Hendrix

[Mario Carneiro]

I mentioned this to Mac and he said that where lake decides to put binaries is an implementation detail and it should have some lake install thing for moving those binaries somewhere else or calling them if necessary

[Mario Carneiro]

A survey of what the top programming languages / package managers do here I think would be helpful

[Eric Wieser]

This is an implementation detail that Cache needs to be in on, right?

[Eric Wieser]

We don't just take things out of the build directory, but put artifacts in there

[Mario Carneiro]

yes, cache has a knack for depending on lake implementation details

[Julian Berman]

To me a small relevant bit is that having potentially giant directories be hidden is a bit "impolite". I.e. I prefer tools use hidden directories on my machine when they drop junk in places, especially in cwd, but not if that directory can be 4GB and I end up with 30 of them and wonder wherefore my hard drive weeps

[Julian Berman]

Sphinx (in the Python ecosystem) uses _foo for its directories, I wonder if they elaborate there on why they chose that.

[Patrick Massot]

Julian, we are already doing that to your harddrive.

[Patrick Massot]

You probably have a giant .mathlib folder in your home.

[Julian Berman]

Right, but I know to clean that! And central directories are way easier to manage

[Patrick Massot]

and a giant .cache/mathlib

[Julian Berman]

That's why I put that directory in $XDG_CACHE_HOME alongside other things I can blow away.

[Patrick Massot]

But indeed they are centralized.

[Julian Berman]

Here the difference is it's going to sit in the repo directory itself.

[Schrodinger ZHU Yifan]

I voted _Lake because hidden dirs are sometimes filtered from pattern ./*

[Joe Hendrix]

How about _lake_ so it's visually a bit like its on a lake?

[Julian Berman]

(This is likely way OT, but even nicer would be if lake's build directories weren't in CWD but rather were more like what pnpm does -- centrally located and symlinked into CWD)

[Arthur Paulino]

If cleanup is the concern, lake clean could learn how to do that

[Eric Wieser]

It would be great to have a option to point lake at an external build directory that didn't require modifying the lake files