Moving to .lake/build/

Stream: lean4

[Thomas Murrills]

I saved ~3.75 GB by remembering to delete mathlib4/build in favor of mathlib4/.lake/build. (I only realized I still had it after using a program that displays your computer's files by size.)

Would it be easy to prompt people to delete their old-style build folder (or simply delete it for them)? (Or did I simply miss the notification somehow?) I wouldn't want people to lose hard drive space unnecessarily. :)

[Shreyas Srinivas]

To keep the projects running, especially ones on older toolchains, after deleting the build folder, might involve unnecessary invocations to the lake update deity who currently appears to be rather annoyed about some manifest (destiny?).

[Mario Carneiro]

I'm not sure about having lake automatically remove the build folder (lest a certain version of lake that shall not be named mistake the project folder for the build folder), but it might prompt about it. As a user I don't see any reason not to remove it after upgrading. @Shreyas Srinivas: downgrading is not supported, but you might end up switching to an old version of lake by switching branches. In this case lake update is not the appropriate response, this kind of comment is not helpful. Just lake build or lake exe cache get; lake build should suffice

[Shreyas Srinivas]

I changed my mathlib dependency to stable on a recent project. Lake update downgraded my toolchain to 4.3 from 4.4.0-rc1.

[Shreyas Srinivas]

So lake does seem to handle downgrades upto some point.

[Shreyas Srinivas]

The question in this case is, isn't the change in lake's folder structure tied to toolchains?

[Mario Carneiro]

Lake will of course do its best with both upgrades and downgrades, but it's not guaranteed to work (and indeed it has a poor track record overall)

[Mario Carneiro]

when you check out a branch or change the dependency version there usually aren't issues with this as long as all deps are using the same version of lake

[Mario Carneiro]

Shreyas Srinivas said:

The question in this case is, isn't the change in lake's folder structure tied to toolchains?

Yes? What's your point

[Shreyas Srinivas]

Suppose this new folder structure was introduced in toolchain X, won't lake on projects with toolchains older than X try to search in the older folder structure and otherwise cache and build within the build folder when lake cache + build is called?

[Shreyas Srinivas]

So lake update would be needed to bring them up to a sufficiently new toolchain. And this causes issues reported on other threads

[Mario Carneiro]

lake update is not how you upgrade your toolchain

[Mario Carneiro]

it is how you upgrade your dependencies

[Shreyas Srinivas]

At the project level

[Shreyas Srinivas]

(sorry dependencies toolchain)

[Thomas Murrills]

@Shreyas Srinivas, just to clarify, are you talking specifically about a situation in which the current project's toolchain uses project/.lake/build, but its dependencies may rely on an older toolchain which uses project/build?

[Shreyas Srinivas]

Yeah

[Mario Carneiro]

that cannot happen

[Mario Carneiro]

your dependencies are compiled with the same lake that compiles your project

[Mario Carneiro]

whether or not they request a different one in their lean-toolchain file

[Shreyas Srinivas]

Yeah but so far the project toolchain is identical to mathlib's toolchain for successfully building math projects

[Mario Carneiro]

yes, because mathlib specifically pins your toolchain to be the same as mathlib's

[Mario Carneiro]

(although this doesn't really work, as the recent lake update revealed - if syntax changes on the new version then lake can't even run the lake script which says to copy the toolchain)

[Shreyas Srinivas]

To make sure I understand this correctly, what you are saying is that I should be able to update (to get the new folder structure) and cache + build a project from, say July/August, using the old folder structure, without a hitch, after discarding my local build folder (ignoring mathlib and Std changes from consideration for the moment)

[Shreyas Srinivas]

Okay I think I see what was meant. @Thomas Murrills : I guess you are suggesting that users delete the build folder after the lake update has already made it redundant. I previously thought you meant that older projects could save space by updating first and then deleting the build folder. my concern was the update not going through properly for older projects

[Shreyas Srinivas]

Apologies from my side

[Thomas Murrills]

No problem! I originally was suggesting that either lake deletes it automatically when it’s using .lake/build or that there’s a prompt/pop-up to delete it—Mario explained why the first option could be a little, er, dangerous :P

Since lake apparently makes this decision based only on the top-level project’s toolchain, if you did (manually) update your project first and got everything building successfully, my understanding is that nothing would go wrong if you then deleted the original non-.lake build folder. I’m not concerned here with bumps in that update process itself, though, which is the only place lake update should come up in all this.