lake: improve functionality in read-only container

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Lake does not work in read-only file system when the absolute path has changed, even if it should not need to do anything (for example when lake build --no-build is supposed to succeed).

Context

This would allow the web editor at live.lean-lang.org to use the leanOptions defined in the lakefile.

The web editor wants to build the project completely outside any container and then run lake serve -- inside a read-only container for any user accessing it.

Steps to Reproduce

0. Ensure you have bubblewrap installed
1. create any lake project with at least one dependency. For simplicity that could be lake new Bubblewrap math but does not need to be mathlib.
2. cd Bubblewrap
3. Create the sample bubblewrap-script to simulate read-only environment:

   touch bubblewrap.sh
   chmod a+x bubblewrap.sh
   nano bubblewrap.sh
   

   and fill it with the following content

   #!/bin/bash
   LEAN_ROOT="$(lean --print-prefix)"
   LEAN_PATH="$(lake env printenv LEAN_PATH)"
   (exec bwrap\
     --ro-bind "." "/project" \
     --ro-bind "$LEAN_ROOT" /lean \
     --ro-bind /usr /usr \
     --dev /dev \
     --tmpfs /tmp \
     --proc /proc \
     --symlink usr/lib /lib\
     --symlink usr/lib64 /lib64\
     --symlink usr/bin /bin\
     --symlink usr/sbin /sbin\
     --clearenv \
     --setenv PATH "/lean/bin" \
     --setenv LAKE "/no" `# tries to invoke git otherwise` \
     --setenv LEAN_PATH "$LEAN_PATH" \
     --unshare-user \
     --unshare-pid  \
     --unshare-net  \
     --unshare-uts  \
     --unshare-cgroup \
     --die-with-parent \
     --chdir "/project/" \
     lake build --no-build
   )
   

4. Build the project normally: lake build
5. Ensure it's built if you want: lake build --no-build
6. Try ./bubblewrap.sh and observe the error message

Expected behavior: I'd expect now that ./bubblewrap.sh would succeed because everything has been built already and there is nothing to change.

Actual behavior: However, lake throws an error about updating the URL of the dependency:

info: mathlib: URL has changed; deleting '././.lake/packages/mathlib' and cloning again
error: read-only file system (error code: 30)
  file: ././.lake/packages/mathlib/Counterexamples.lean

This is confusing because I don't think lake should need to update any revs or URLs of packages at this stage.

Versions

leanprover/lean4:v4.19.0-rc2
Linux (Ubuntu)

Additional Information

bubblewrap can usually be installed with sudo apt-get install bubblewrap

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the provided bubblewrap.sh reproduction and compare lake build with and without --no-build after the project is built normally. Trace Lake's dependency URL update path for the read-only invocation, using the reported mathlib package error as the failure point. Done means lake build --no-build succeeds in the read-only container without attempting to modify the dependency checkout.