summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authortv <tv@shackspace.de>2015-06-26 17:58:30 +0200
committertv <tv@shackspace.de>2015-06-26 17:58:30 +0200
commite34666bf320b70bff63f9e73bd03fdc94b2bcc05 (patch)
tree95fd85a25b2b41fc736ba3f03eaa7cd8c5382ea9
parent90772971a81d065028796fe2bf8a1d0ad78c06f7 (diff)
fetchgit: cache and share nixpkgs
-rwxr-xr-xbin/fetchgit71
1 files changed, 57 insertions, 14 deletions
diff --git a/bin/fetchgit b/bin/fetchgit
index b9fe90854..293cc31f3 100755
--- a/bin/fetchgit
+++ b/bin/fetchgit
@@ -1,25 +1,68 @@
#! /bin/sh
-# usage: fetchgit REVISION URL WORKTREE
+#
+# usage: fetchgit git_rev git_url out_link
+#
+# Clone the specified Git repository and make it available as out_link.
+#
set -euf
git_rev=$1
git_url=$2
-worktree=$3
+out_link=$3
-if [ ! -d "$worktree" ]; then
- mkdir -p "$worktree"
-fi
+# Put all bases in the same place as out_link.
+# Notice how out_link must not clash with cache_dir and work_dir.
+cache_base=$(dirname "$out_link")
+work_base=$(dirname "$out_link")
-cd "$worktree"
+# cache_dir points to a (maybe non-existent) directory, where a shared cache of
+# the repository should be maintained. The shared cache is used to create
+# multiple working trees of the repository.
+cache_dir=$cache_base/$(echo "$git_url" | urlencode)
-git init -q
+# work_dir points to a (maybe non-existent) directory, where a specific
+# revision of the repository is checked out.
+work_dir=$work_base/$(echo "$git_rev")
-if ! current_url=$(git config remote.src.url); then
- git remote add src "$git_url"
-elif [ "$current_url" != "$git_url" ]; then
- git remote set-url src "$git_url"
-fi
+cache_git() {
+ git --git-dir="$cache_dir" "$@"
+}
+
+work_git() {
+ git -C "$work_dir" "$@"
+}
-git fetch src
+is_up_to_date() {
+ test -d "$cache_dir" &&
+ test -d "$work_dir" &&
+ test "$(work_git rev-parse HEAD)" = "$git_rev"
+}
-git checkout "$git_rev"
+if ! is_up_to_date; then
+ if ! test -d "$cache_dir"; then
+ mkdir -p "$cache_dir"
+ cache_git init --bare
+ fi
+ if ! cache_git_url=$(cache_git config remote.origin.url); then
+ cache_git remote add origin "$git_url"
+ elif test "$cache_git_url" != "$git_url"; then
+ cache_git remote set-url origin "$git_url"
+ fi
+ cache_git fetch origin
+ if ! test -d "$work_dir"; then
+ git clone -n --shared "$cache_dir" "$work_dir"
+ fi
+ work_git checkout "$git_rev" -- "$(readlink -f "$work_dir")"
+ work_git checkout -b master "$git_rev"
+ work_git submodule init
+ work_git submodule update
+fi
+work_git clean -dxf
+
+# Relative links are nicer, and actually we know that work_dir and out_link are
+# the same. But, for robustness, check anyway.. :)
+if test "$(dirname "$work_dir")" = "$(dirname "$out_link")"; then
+ ln -snf "$(basename "$work_dir")" "$out_link"
+else
+ ln -snf "$work_dir" "$out_link"
+fi