> Thanks.  A few comments.
>
> At the design level.  Where does this $sha1 come from in the first
> place?
>
actually, sha1=$(git rev-parse "$ref"^0)
(please remember that I'm discovering git internals while figuring out
how to make git filter-branch work in my use case)

in my use case, $ref is "refs/tags/4.0" which is an annotated tag

$ git rev-parse "refs/tags/4.0"
e941b1999906c17b59320f776d58b71fc2fcdb72

$ git cat-file -t e941b1999906c17b59320f776d58b71fc2fcdb72
tag

$ git rev-parse e941b1999906c17b59320f776d58b71fc2fcdb72^0
dcd7cdc18240dd9a54b30d757dd2347f52040490

$ git cat-file -t dcd7cdc18240dd9a54b30d757dd2347f52040490
commit

so $sha1 is dcd7cdc18240dd9a54b30d757dd2347f52040490

and then git-filter-branch calls git update-ref -m "filter-branch:
delete" -d "refs/tags/4.0" dcd7cdc18240dd9a54b30d757dd2347f52040490
which makes git update-index complains
e941b1999906c17b59320f776d58b71fc2fcdb72 !=
dcd7cdc18240dd9a54b30d757dd2347f52040490

so hmm, adding test $(git rev-parse --verify "$ref^{commit}") = $sha1
as I did in my patch is always true since sha1=$(git rev-parse
"$ref"^0)

>  If a ref that named the annotated tag was deleted, shouldn't
> we arrange things so this part of the code receives the $sha1 of the
> tag that corresponds to the $ref
>
I'm not sure what you mean by "a ref that named the annotated tag was deleted"
What's happening in my situation is that the commit the tag points to
gets rewritten to nothing as the result of my filtering:
"refs/tags/4.0" points to e941b1999906c17b59320f776d58b71fc2fcdb72
(tag) which points to dcd7cdc18240dd9a54b30d757dd2347f52040490
(commit) which gets rewritten to nothing so the tag must be deleted.

> so that "update-ref -d" can check
> that nobody tampered with the repository while the script was
> working?
>
I'm not quite sure what could possibly go well if somebody tampers
with the repository while it's being filtered with git filter-branch
anyways???

If we want to address "did somebody tamper with the repository while
the script was working?", then test $(git rev-parse --verify
"$ref^{commit}") = $sha1 verifies somebody didn't tamper with $ref
since we got $sha1 from it.
But that doesn't ensure tampering didn't take place in between
  test $(git rev-parse --verify "$ref^{commit}") = $sha1
and
  git update-ref -m "filter-branch: delete" -d "$ref".

How defensive should git filter-branch really be?

> At the implementation level.  When the ref being deleted pointed at
> a tree or a blob, the original would have correctly removed it, but
> will the updated one?
>
Yes.

Now that you made me think about it even more, the title of that
thread isn't "git filter-branch doesn't dereference annotated tags".
It in fact does as per sha1=$(git rev-parse "$ref"^0).

Maybe the suggested fix should be: in case the tag points to a commit
that has been rewritten to nothing, get $sha1 again without
dereferencing recursively with sha1=$(git rev-parse "$ref") then use
the 3 arguments versions of git update-ref as before.

Thanks for reading
Gregory

>From 59f86c9c07715734d59009c15816220f996b75be Mon Sep 17 00:00:00 2001
From: Gregory Pakosz <gpakosz@visionobjects.com>
Date: Mon, 31 Dec 2012 15:30:36 +0100
Subject: [PATCH] git-filter-branch: support annotated tags deletion

git-filter-branch let git-update-ref -d verify that the value for $ref matches
$sha1. $sha1 is obtained form dereferencing $ref recursively. In case $sha1 gets
rewritten to nothing as per result of the filtering, the tag should be deleted.
However, in case of an annotated tag, git-update-ref -d fails because $ref
doesn't directly point to $sha1.

To make git-filter-branch properly delete an annotated tag, obtain $sha1 again
withouth dereferencing the tag before asking git-update-ref to verify $ref and
$sha1 match.

Signed-off-by: Gregory Pakosz <gpakosz@visionobjects.com>
---
 git-filter-branch.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/git-filter-branch.sh b/git-filter-branch.sh
index 5314249..7ae9912 100755
--- a/git-filter-branch.sh
+++ b/git-filter-branch.sh
@@ -383,6 +383,7 @@ do
 	case "$rewritten" in
 	'')
 		echo "Ref '$ref' was deleted"
+		test $(git cat-file -t "$ref") = 'tag' && sha1=$(git rev-parse "$ref")
 		git update-ref -m "filter-branch: delete" -d "$ref" $sha1 ||
 			die "Could not delete $ref"
 	;;
-- 
1.8.0.1