Re: [PATCH] push: Alias pushurl from push rewrites

On Wed, Mar 27, 2013 at 04:09:43PM -0700, Josh Triplett wrote:

On Wed, Mar 27, 2013 at 05:48:45PM -0500, Rob Hoelz wrote:

quoted

On Wed, 27 Mar 2013 15:07:18 -0700
Junio C Hamano [off-list ref] wrote:

quoted

Jonathan Nieder [off-list ref] writes:

quoted

Sorry, typo.  The configuration in the example above should have
been

	[url "git://anongit.myserver.example.com/"]
		insteadOf = myserver.example.com:
	[url "myserver.example.com:"]
		pushInsteadOf = myserver.example.com:

In other words, suppose I set url.*.insteadof to point to a faster
address for fetching alongside url.*.pushinsteadof requesting that
the original address should still be used for pushing.

I didn't know we were even shooting for supporting the identity
mapping:

	url.X.pushinsteadof=X

but that would certainly be nice.

By the way, it seems that the original commit 1c2eafb89bca (Add
url.<base>.pushInsteadOf: URL rewriting for push only, 2009-09-07)
wanted to explicitly avoid use of pushInsteadOf aliasing for a
pushURL and it is also documented in config.txt from day one.

I think the intent is "You have a normal URL, and a way to override
it explicitly with pushURL, or a way to rewrite it via the aliasing
the normal URL with pushInsteadOf. Either one or the other, but not
both, as having many levels of indirection would be confusing."

Which I can understand and sympathise.

In anay case, the change proposed in this thread seems to change
that, so the documentation would need to be updated.  Also the tests
the original commit adds explicitly checks that pushInsteadOf is
ignored, which may have to be updated (unless that test is already
broken).

My use case is that I use Github for my personal development.  I have a
prefix for my personal repos (hoelzro: -> git://github.com/hoelzro for
fetch, git@github.com:hoelzro/ for push) and one for all other Git repos
(github: -> git://github.com/)  I have a few projects where I work in a
fork, but I want to fetch updates from the original project.  So my url
for the origin remote is github:org/project, but my pushurl is
hoelzro:project.  This behavior in Git currently doesn't allow me to
work that way.  I used to work with two remotes; origin for my repo and
base for the official one, but I've found that I prefer this other way.

The test that checked that pushInsteadOf + pushurl shouldn't work as I
expect was actually broken; I have removed it, updated the
documentation, and sent a new patch to the list.

There's an argument for either behavior as valid.  My original patch
specifically documented and tested for the opposite behavior, namely
that pushurl overrides any pushInsteadOf, because I intended
pushInsteadOf as a fallback if you don't have an explicit pushurl set.
For instance, you could use pushInsteadOf to rewrite a family of
anonymous git URLs to corresponding pushable repositories, but then use
an explicit pushurl to override that for a specific repository.  This
change would break the ability to use pushurl for its original intended
purpose, namely having a local repository where fetch comes from one
remote repo and push goes to another.

One use case of mine: I have a .gitconfig in my git-managed home
directory which sets pushInsteadOf so that I can clone via git:// and
immediately have working push.  I work with a number of systems that
don't have inbound access to each other but do have outbound access to
the network; on some of these "satellite" boxes, I can't push changes
directly to the server pushInsteadOf points to, so I can explicitly set
pushurl in .git/config for that repository, which overrides the
pushInsteadOf.  This change would break that configuration.

Clarifying this use case a bit: note that it's been a while since I had
many such boxes, so I don't actually have any systems currently using
that pushurl configuration.  Still a regression in defined behavior,
though.

Why not just use insteadOf for your personal github prefix hoelzro:, and
both insteadOf and pushInsteadOf for github: in general?  Then, a
repository cloned via github: would work for pull and push (if you have
push access), and you can change pushurl to your personal github alias
if needed.

Though, as Junio said, the modern push-updates-remote-heads behavior of
git means that both of our configurations arguably seem wrong, and we
should both just use separate remotes for separate repos.

- Josh Triplett