feat; customizable error message on build

[tydeu]

Adds a Lake configuration option (errorOnBuild) that, when set, will produced a custom error if ProofWidgets needs to be built (and the cache not merely reused). The plan is to use this option in Mathlib in order to advise users to run lake exe cache get instead to get an up-to-date ProofWidgets.

[Vtec234]

We could add this but I'm wondering, should this maybe be a Lake option, e.g. something you can customize when requireing a package? PW4 is the only mathlib dependency that needs cloud builds right now but I think putting such a requirement might be more generally useful, e.g. for ML packages that come with some prebuilt libraries that downstream should avoid building.

[kim-em]

I'd propose that we merge as is for now, to get this issue out of the way of Mathlib users (who I think still hit it frequently), and Mac decides when/if a more general fix goes into Lake.