fix: init git only not inside git work tree

[haoxins]

trafficstars

Addresses part of #2758.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-10-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-10-21 10:19:03)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4ee44ceb1d77f16b9b81bc655bc8b318cd6e8c4d --onto 9847923f9be5de968f10ed7c7493e3ca0072abce. (2024-10-29 04:03:50)

[tydeu]

LGTM! This does not address every feature covered by #2758, so I do not think this should close that issue. Regardless, this seems like a strict improvement, so am merging it.

[tydeu]

Ah, here is the problem. Lake tests make use of the lake new/init to generate packages with Git repositories. That fails with this change because it is within the work tree of Lean itself. The tests could be fixed by running git init in the packages separately from Lake.

[haoxins]

Ah, here is the problem. Lake tests make use of the lake new/init to generate packages with Git repositories. That fails with this change because it is within the work tree of Lean itself. The tests could be fixed by running git init in the packages separately from Lake.

thanks, it works now.