feat: a way to build a project inside lake check's sandbox without checking it #15282

lake check builds the project inside a bubblewrap sandbox before exporting it and replaying the result through the kernel. For anyone whose project is untrusted input, the sandbox is the valuable part, but it is only reachable by also paying for the export and the kernel replay.

It would be useful to run just the build, under the same sandbox and with the same guarantees: for CI that wants to compile a possibly-malicious project without giving it the runner, where kernel checking either happens later or is not wanted at all.

The alternative today is to reconstruct Lake's sandbox by hand with bwrap, which duplicates the mount and namespace setup in Lake.CLI.Check and breaks whenever that changes.

Context, where lean-action gained a lake check input and the question of what to build where came up:

leanprover/lean-action#190 — feat: add lake-check input for sandboxed independent kernel checks