fix: properly update git packages specified by branch

closes #84

Author: tydeu

Diff for: Lake/Config/Resolve.lean

@@ -19,10 +19,17 @@ namespace Lake
 def updateGitPkg (name : String)
 (repo : GitRepo) (rev? : Option String) : LogIO PUnit := do
   if let some rev := rev? then
-    if (← repo.headRevision) == rev then return
-    logInfo s!"{name}: updating {repo} to revision {rev}"
-    unless ← repo.revisionExists rev do repo.fetch
-    repo.checkoutDetach rev
+    if (← repo.branchExists rev) then
+      repo.fetch
+      let rev ← repo.parseOriginRevision rev
+      if (← repo.headRevision) == rev then return
+      logInfo s!"{name}: updating {repo} to revision {rev}"
+      repo.checkoutDetach rev
+    else
+      if (← repo.headRevision) == rev then return
+      logInfo s!"{name}: updating {repo} to revision {rev}"
+      unless ← repo.revisionExists rev do repo.fetch
+      repo.checkoutDetach rev
   else
     logInfo s!"{name}: updating {repo}"
     repo.pull

Diff for: Lake/Util/Git.lean

@@ -33,7 +33,10 @@ def exec (args : Array String) (wd : Option FilePath := none) : LogIO PUnit := d
 
 def test (args : Array String) (wd : Option FilePath := none) : LogT BaseIO Bool :=
   let act : IO _ := do
-    let child ← IO.Process.spawn {cmd := "git", args, cwd := wd}
+    let child ← IO.Process.spawn {
+      cmd := "git", args, cwd := wd,
+      stdout := IO.Process.Stdio.null, stderr := IO.Process.Stdio.null
+    }
     return (← child.wait) == 0
   act.catchExceptions fun _ => pure false
 

Diff for: Makefile

@@ -12,7 +12,7 @@ test: check-lake test-ci test-bootstrap test-bootstrapped
 
 test-ci: test-tests test-examples
 
-test-tests: test-49 test-50 test-62 test-75
+test-tests: test-49 test-50 test-62 test-75 test-84
 
 test-examples: test-init test-hello test-io test-deps\
 	test-git test-ffi test-targets test-precompile test-scripts
@@ -21,7 +21,7 @@ test-bootstrapped: test-boostrapped-hello
 
 clean: clean-build clean-tests clean-examples
 
-clean-tests: clean-62
+clean-tests: clean-62 clean-84
 
 clean-examples: clean-init clean-hello clean-io clean-deps\
 	clean-git clean-ffi clean-targets clean-precompile clean-bootstrap
@@ -137,3 +137,9 @@ clean-62:
 
 test-75:
 	cd test/75 && ./test.sh
+
+clean-84:
+	cd test/84 && ./clean.sh
+
+test-84:
+	cd test/84 && ./test.sh

Diff for: test/84/.gitignore

@@ -0,0 +1,2 @@
+/a
+/b

Diff for: test/84/clean.sh

@@ -0,0 +1,2 @@
+rm -rf a
+rm -rf b

Diff for: test/84/test.sh

@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+set -exo pipefail
+
+LAKE=${LAKE:-../../build/bin/lake}
+
+./clean.sh
+
+$LAKE new a
+pushd a
+git add .
+git commit -am 'first commit in a'
+popd
+
+$LAKE new b
+pushd b
+cat >>lakefile.lean <<EOF
+require a from git "../a" @ "master"
+EOF
+../$LAKE update
+git add .
+git commit -am 'first commit in b'
+popd
+
+pushd a
+echo def hello2 := 42 >>A.lean
+git commit -am 'second commit in a'
+popd
+
+pushd b
+../$LAKE update
+git diff | grep -m1 manifest
+popd