test: lake: avoid git init in the checked-in test tree

[Kha]

This PR makes the Lake tests that require a Git repository operate on a copy in an untracked work/ directory instead of running git init inside the checked-in source tree. This prevents the tracked test files from being reported as removed when a nested Git repository is created under version control.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6de1d62f83565e01774358e8dce4a7aa3eebb482 --onto 2cd98639c40d2d2a026dd599093b70f55f55ffaf. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-28 16:53:26)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6de1d62f83565e01774358e8dce4a7aa3eebb482 --onto c47a0c7cf035381a2bcdd4cdf2442782eb4a5214. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-29 10:23:02)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 6de1d62f83565e01774358e8dce4a7aa3eebb482 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-28 16:53:28)

[tydeu]

LGTM!