fix: init git only not inside git work tree (#5789)

Addresses part of #2758.

Author: haoxins

src/lake/Lake/CLI/Init.lean

@@ -278,8 +278,8 @@ def initPkg (dir : FilePath) (name : Name) (tmp : InitTemplate) (lang : ConfigLa
     IO.FS.writeFile readmeFile (readmeFileContents <| dotlessName name)
 
   -- initialize a `.git` repository if none already
-  unless (← FilePath.isDir <| dir / ".git") do
-    let repo := GitRepo.mk dir
+  let repo := GitRepo.mk dir
+  unless (← repo.insideWorkTree) do
     try
       repo.quietInit
       unless upstreamBranch = "master" do

src/lake/Lake/Util/Git.lean

@@ -63,6 +63,9 @@ def cwd : GitRepo := ⟨"."⟩
 @[inline] def quietInit (repo : GitRepo) : LogIO PUnit  :=
   repo.execGit #["init", "-q"]
 
+@[inline] def insideWorkTree (repo : GitRepo) : BaseIO Bool := do
+  repo.testGit #["rev-parse", "--is-inside-work-tree"]
+
 @[inline] def fetch (repo : GitRepo) (remote := Git.defaultRemote) : LogIO PUnit  :=
   repo.execGit #["fetch", "--tags", "--force", remote]
 

src/lake/tests/clone/test.sh

@@ -18,6 +18,7 @@ mkdir hello
 pushd hello
 $LAKE init hello
 $LAKE update
+git init
 git checkout -b master
 git config user.name test
 git config user.email test@example.com

src/lake/tests/depTree/test.sh

@@ -22,6 +22,7 @@ fi
 # a@1/init
 $LAKE new a lib.lean
 pushd a
+git init
 git checkout -b master
 git add .
 git config user.name test
@@ -33,6 +34,7 @@ popd
 # b@1: require a@master, manifest a@1
 $LAKE new b lib.lean
 pushd b
+git init
 git checkout -b master
 cat >>lakefile.lean <<EOF
 require a from git "../a" @ "master"
@@ -54,6 +56,7 @@ popd
 # c@1: require a@master, manifest a@2
 $LAKE new c lib.lean
 pushd c
+git init
 git checkout -b master
 cat >>lakefile.lean <<EOF
 require a from git "../a" @ "master"
@@ -69,6 +72,7 @@ popd
 # d@1: require b@master c@master => a, manifest a@1 b@1 c@1
 $LAKE new d lib.lean
 pushd d
+git init
 git checkout -b master
 cat >>lakefile.lean <<EOF
 require b from git "../b" @ "master"