lake clean should remove lakefile.olean in the root directory and under lake-packages

[semorrison]

(And possibly its location outside of build should be reconsidered.)

[digama0]

The technical reason given for not putting lakefile.olean in build (there was also a philosophical reason but I didn't really understand it) is that the location of the build directory is configurable from the lakefile using the buildDir option in package, so we wouldn't know where to look for the olean until we'd already parsed the lakefile.

My opinion is that the location of the build directory is a user option, not a package option, and should be configured (if configuration for this is even necessary) using a separate configuration mechanism: a global configuration file, a project-local configuration file (not the lakefile, and customarily not checked in), an environment variable, or a CLI flag.

[semorrison]

I see. No configuration is the best configuration! :-) I'm currently failing to think of a use case of configuring the location of build directory. Configuring the location of lake-packages is obviously important, because lecturers may want to be able to share this to support student accounts with limited space.

In any case, this question is incidental to the actual topic of the issue, which can certainly be resolved without worrying about the location question.

[tydeu]

@semorrison

I'm currently failing to think of a use case of configuring the location of build directory.

If it helps,, two of use cases were I currently customize the build directory:

• Splitting it by platform architecture when that is relevant. This allows me to have one build directory for Windows and one for WSL without having to rebuild or manually switch them in and out.
• Building Lean with Lake (which I do locally for a more interactive VSCode). The build directory needs to be in build/<config>/stage<n> (with the subdirectories for libs, IR, etc also customized).