Help understanding git checkout behavior

Help understanding git checkout behavior

[Cláudio Lourenço]

Hello,

We are master students at University of Minho in Portugal and we are
currently working on a project suggested by CSAIL (MIT), called
"Understanding Git with Alloy". The project consists in modeling git
using alloy and then check for some properties that git does (not)
guarantee.

The project was going pretty fine, till we start modeling the checkout
operation. We are with some problems finding useful information about
the properties that have to be satisfied when the "git checkout" is
performed. We have concluded that if everything that is on index is
commited then we have no problems making checkout.
The problem is when we have something on index that is not updated
with the last commit. We cannot find a general property that says when
checkout can be performed. We have even found some files that are
lost, like in this case:

smooke  teste $ git init
Initialized empty Git repository in /home/smooke/Dropbox/teste/.git/
smooke  teste $ touch f
smooke  teste $ echo a > f
smooke  teste $ git add f
smooke  teste $ git commit -m 'first commit'
[master (root-commit) dab04b9] first commit
 1 files changed, 1 insertions(+), 0 deletions(-)
 create mode 100644 f
smooke  teste $ git branch b
smooke  teste $ touch something
smooke  teste $ echo b > something
smooke  teste $ git add something
smooke  teste $ git commit -m 'something added'
[master 9f2b8ad] something added
 1 files changed, 1 insertions(+), 0 deletions(-)
 create mode 100644 something
smooke  teste $ git rm something
rm 'something'
smooke  teste $ mkdir something
smooke  teste $ cd something/
smooke  something $ touch f1
smooke  something $ echo c > f1
smooke  something $ cd ..
smooke  teste $ git add something/f1
smooke  teste $ git checkout b
Switched to branch 'b'
smooke  teste $ ls
f
smooke  teste $ git checkout master
Switched to branch 'master'
smooke  teste $ ls
f  something
smooke  teste $ cat something
b

We are not sure if this behavior has an explanation of if it is just a bug.

We are hoping that you could clarify us about this operation or
recommend us some place where we can find some useful information
about this...

Thank you in advance,
Best regards,

Cláudio and Renato

Re: Help understanding git checkout behavior

[Konstantin Khomoutov]

On Mon, 11 Jun 2012 17:52:26 +0100
Cláudio Lourenço <pt.smooke@gmail.com> wrote:

> We are master students at University of Minho in Portugal and we are
> currently working on a project suggested by CSAIL (MIT), called
> "Understanding Git with Alloy". The project consists in modeling git
> using alloy and then check for some properties that git does (not)
> guarantee.
I think providing a link to that "alloy" thing could be helpful.

[...]

Re: Help understanding git checkout behavior

[konglu]

Cláudio Lourenço <pt.smooke@gmail.com> a écrit :

> The project was going pretty fine, till we start modeling the checkout
> operation. We are with some problems finding useful information about
> the properties that have to be satisfied when the "git checkout" is
> performed. We have concluded that if everything that is on index is
> commited then we have no problems making checkout.
> The problem is when we have something on index that is not updated
> with the last commit. We cannot find a general property that says when
> checkout can be performed. We have even found some files that are
> lost, like in this case:
>
> smooke  teste $ git init
> Initialized empty Git repository in /home/smooke/Dropbox/teste/.git/
> smooke  teste $ touch f
> smooke  teste $ echo a > f
> smooke  teste $ git add f
> smooke  teste $ git commit -m 'first commit'
> [master (root-commit) dab04b9] first commit
>  1 files changed, 1 insertions(+), 0 deletions(-)
>  create mode 100644 f
> smooke  teste $ git branch b
> smooke  teste $ touch something
> smooke  teste $ echo b > something
> smooke  teste $ git add something
> smooke  teste $ git commit -m 'something added'
> [master 9f2b8ad] something added
>  1 files changed, 1 insertions(+), 0 deletions(-)
>  create mode 100644 something
> smooke  teste $ git rm something
> rm 'something'
> smooke  teste $ mkdir something
> smooke  teste $ cd something/
> smooke  something $ touch f1
> smooke  something $ echo c > f1
> smooke  something $ cd ..
> smooke  teste $ git add something/f1
> smooke  teste $ git checkout b
> Switched to branch 'b'
> smooke  teste $ ls
> f
> smooke  teste $ git checkout master
> Switched to branch 'master'
> smooke  teste $ ls
> f  something
> smooke  teste $ cat something
> b

What do you mean by "lost files" ? Are you talking about "something"
that doesn't appear on branch 'b' ?

Re: Help understanding git checkout behavior

[Leila]

When you create a branch, it will contain everything committed on the
branch you created it from at that given point. So if you commit more
things on the master branch like you have done (after creating b),
then switch to branch b, they won't appear. This is the correct
behavior. Does that answer your question?


On Mon, Jun 11, 2012 at 2:21 PM,  <konglu@minatec.inpg.fr> wrote:
>
> Cláudio Lourenço <pt.smooke@gmail.com> a écrit :
>
>
>> The project was going pretty fine, till we start modeling the checkout
>> operation. We are with some problems finding useful information about
>> the properties that have to be satisfied when the "git checkout" is
>> performed. We have concluded that if everything that is on index is
>> commited then we have no problems making checkout.
>> The problem is when we have something on index that is not updated
>> with the last commit. We cannot find a general property that says when
>> checkout can be performed. We have even found some files that are
>> lost, like in this case:
>>
>> smooke  teste $ git init
>> Initialized empty Git repository in /home/smooke/Dropbox/teste/.git/
>> smooke  teste $ touch f
>> smooke  teste $ echo a > f
>> smooke  teste $ git add f
>> smooke  teste $ git commit -m 'first commit'
>> [master (root-commit) dab04b9] first commit
>>  1 files changed, 1 insertions(+), 0 deletions(-)
>>  create mode 100644 f
>> smooke  teste $ git branch b
>> smooke  teste $ touch something
>> smooke  teste $ echo b > something
>> smooke  teste $ git add something
>> smooke  teste $ git commit -m 'something added'
>> [master 9f2b8ad] something added
>>  1 files changed, 1 insertions(+), 0 deletions(-)
>>  create mode 100644 something
>> smooke  teste $ git rm something
>> rm 'something'
>> smooke  teste $ mkdir something
>> smooke  teste $ cd something/
>> smooke  something $ touch f1
>> smooke  something $ echo c > f1
>> smooke  something $ cd ..
>> smooke  teste $ git add something/f1
>> smooke  teste $ git checkout b
>> Switched to branch 'b'
>> smooke  teste $ ls
>> f
>> smooke  teste $ git checkout master
>> Switched to branch 'master'
>> smooke  teste $ ls
>> f  something
>> smooke  teste $ cat something
>> b
>
>
> What do you mean by "lost files" ? Are you talking about "something"
> that doesn't appear on branch 'b' ?
>
>
>
> --
> To unsubscribe from this list: send the line "unsubscribe git" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at  http://vger.kernel.org/majordomo-info.html

Re: Help understanding git checkout behavior

[Jeff King]

On Mon, Jun 11, 2012 at 02:34:01PM -0400, Leila wrote:

> When you create a branch, it will contain everything committed on the
> branch you created it from at that given point. So if you commit more
> things on the master branch like you have done (after creating b),
> then switch to branch b, they won't appear. This is the correct
> behavior. Does that answer your question?

No, the problem is more subtle:

> >> smooke  teste $ git rm something
> >> rm 'something'
> >> smooke  teste $ mkdir something
> >> smooke  teste $ cd something/
> >> smooke  something $ touch f1
> >> smooke  something $ echo c > f1
> >> smooke  something $ cd ..
> >> smooke  teste $ git add something/f1
> >> smooke  teste $ git checkout b
> >> Switched to branch 'b'
> >> smooke  teste $ ls
> >> f

We have lost "something/f1" during the switch, which was not committed
anywhere. This is presumably an error because we see that "something"
used to be tracked, and now we are tracking something different there.

If we had put some new content into the file "something", git would
rightfully complain with:

  $ git checkout b
  error: Your local changes to the following files would be overwritten
  by checkout:
          something
  Please, commit your changes or stash them before you can switch branches.
  Aborting

But it misses the case when "something" switches from a file into a
directory, which is probably a bug.

-Peff

Re: Help understanding git checkout behavior

[Junio C Hamano]

Leila <muhtasib@gmail.com> writes:

> When you create a branch, it will contain everything committed on the
> branch you created it from at that given point. So if you commit more
> things on the master branch like you have done (after creating b),
> then switch to branch b, they won't appear. This is the correct
> behavior. Does that answer your question?

If there were "git commit" immediately before the "git checkout b"
to check out the branch "b", then something/f1 would be among the
data committed to the branch "master", and it is perfectly fine to
remove it in order to check out branch "b" that does not have the
directory "something" or file in it "something/f1".

But if there is "something/f1" that is not yet committed, the
command should have refused to check out the branch "b", which I
think is what Cláudio is talking about.  It looks like a bug to me.

>
>
> On Mon, Jun 11, 2012 at 2:21 PM,  <konglu@minatec.inpg.fr> wrote:
>>
>> Cláudio Lourenço <pt.smooke@gmail.com> a écrit :
>>
>>
>>> The project was going pretty fine, till we start modeling the checkout
>>> operation. We are with some problems finding useful information about
>>> the properties that have to be satisfied when the "git checkout" is
>>> performed. We have concluded that if everything that is on index is
>>> commited then we have no problems making checkout.
>>> The problem is when we have something on index that is not updated
>>> with the last commit. We cannot find a general property that says when
>>> checkout can be performed. We have even found some files that are
>>> lost, like in this case:
>>>
>>> smooke  teste $ git init
>>> Initialized empty Git repository in /home/smooke/Dropbox/teste/.git/
>>> smooke  teste $ touch f
>>> smooke  teste $ echo a > f
>>> smooke  teste $ git add f
>>> smooke  teste $ git commit -m 'first commit'
>>> [master (root-commit) dab04b9] first commit
>>>  1 files changed, 1 insertions(+), 0 deletions(-)
>>>  create mode 100644 f
>>> smooke  teste $ git branch b
>>> smooke  teste $ touch something
>>> smooke  teste $ echo b > something
>>> smooke  teste $ git add something
>>> smooke  teste $ git commit -m 'something added'
>>> [master 9f2b8ad] something added
>>>  1 files changed, 1 insertions(+), 0 deletions(-)
>>>  create mode 100644 something
>>> smooke  teste $ git rm something
>>> rm 'something'
>>> smooke  teste $ mkdir something
>>> smooke  teste $ cd something/
>>> smooke  something $ touch f1
>>> smooke  something $ echo c > f1
>>> smooke  something $ cd ..
>>> smooke  teste $ git add something/f1
>>> smooke  teste $ git checkout b
>>> Switched to branch 'b'
>>> smooke  teste $ ls
>>> f
>>> smooke  teste $ git checkout master
>>> Switched to branch 'master'
>>> smooke  teste $ ls
>>> f  something
>>> smooke  teste $ cat something
>>> b
>>
>>
>> What do you mean by "lost files" ? Are you talking about "something"
>> that doesn't appear on branch 'b' ?
>>
>>
>>
>> --
>> To unsubscribe from this list: send the line "unsubscribe git" in
>> the body of a message to majordomo@vger.kernel.org
>> More majordomo info at  http://vger.kernel.org/majordomo-info.html

Re: Help understanding git checkout behavior

[Cláudio Lourenço]

First of all, thank you all for your attention.
The link for alloy is http://alloy.mit.edu/alloy/  Feel free to take a
look, but this is not the point. We just want to understand what are
the pre-conditions that have to be satisfied to perform checkout.

We have done some tests and we concluded that it is possible to checkout if:

for each file that is on index, but not on the last commit, we have
two cases when it is possible to checkout (from master) to branch b

   first: the file is not on the commit pointed by branch b

   second: the file is on the commit pointed by branch b, and it has
the same content as the file on index, or, the file of both commits
(master and b) have the same content

The deleted files from index, are just ignored (we think the bug comes
from here).

Are our assumptions corrects? Is there any place were we can see such
specifications?



On Mon, Jun 11, 2012 at 7:56 PM, Junio C Hamano <gitster@pobox.com> wrote:
> Leila <muhtasib@gmail.com> writes:
>
>> When you create a branch, it will contain everything committed on the
>> branch you created it from at that given point. So if you commit more
>> things on the master branch like you have done (after creating b),
>> then switch to branch b, they won't appear. This is the correct
>> behavior. Does that answer your question?
>
> If there were "git commit" immediately before the "git checkout b"
> to check out the branch "b", then something/f1 would be among the
> data committed to the branch "master", and it is perfectly fine to
> remove it in order to check out branch "b" that does not have the
> directory "something" or file in it "something/f1".
>
> But if there is "something/f1" that is not yet committed, the
> command should have refused to check out the branch "b", which I
> think is what Cláudio is talking about.  It looks like a bug to me.
>
>>
>>
>> On Mon, Jun 11, 2012 at 2:21 PM,  <konglu@minatec.inpg.fr> wrote:
>>>
>>> Cláudio Lourenço <pt.smooke@gmail.com> a écrit :
>>>
>>>
>>>> The project was going pretty fine, till we start modeling the checkout
>>>> operation. We are with some problems finding useful information about
>>>> the properties that have to be satisfied when the "git checkout" is
>>>> performed. We have concluded that if everything that is on index is
>>>> commited then we have no problems making checkout.
>>>> The problem is when we have something on index that is not updated
>>>> with the last commit. We cannot find a general property that says when
>>>> checkout can be performed. We have even found some files that are
>>>> lost, like in this case:
>>>>
>>>> smooke  teste $ git init
>>>> Initialized empty Git repository in /home/smooke/Dropbox/teste/.git/
>>>> smooke  teste $ touch f
>>>> smooke  teste $ echo a > f
>>>> smooke  teste $ git add f
>>>> smooke  teste $ git commit -m 'first commit'
>>>> [master (root-commit) dab04b9] first commit
>>>>  1 files changed, 1 insertions(+), 0 deletions(-)
>>>>  create mode 100644 f
>>>> smooke  teste $ git branch b
>>>> smooke  teste $ touch something
>>>> smooke  teste $ echo b > something
>>>> smooke  teste $ git add something
>>>> smooke  teste $ git commit -m 'something added'
>>>> [master 9f2b8ad] something added
>>>>  1 files changed, 1 insertions(+), 0 deletions(-)
>>>>  create mode 100644 something
>>>> smooke  teste $ git rm something
>>>> rm 'something'
>>>> smooke  teste $ mkdir something
>>>> smooke  teste $ cd something/
>>>> smooke  something $ touch f1
>>>> smooke  something $ echo c > f1
>>>> smooke  something $ cd ..
>>>> smooke  teste $ git add something/f1
>>>> smooke  teste $ git checkout b
>>>> Switched to branch 'b'
>>>> smooke  teste $ ls
>>>> f
>>>> smooke  teste $ git checkout master
>>>> Switched to branch 'master'
>>>> smooke  teste $ ls
>>>> f  something
>>>> smooke  teste $ cat something
>>>> b
>>>
>>>
>>> What do you mean by "lost files" ? Are you talking about "something"
>>> that doesn't appear on branch 'b' ?
>>>
>>>
>>>
>>> --
>>> To unsubscribe from this list: send the line "unsubscribe git" in
>>> the body of a message to majordomo@vger.kernel.org
>>> More majordomo info at  http://vger.kernel.org/majordomo-info.html

Re: Help understanding git checkout behavior

[Junio C Hamano]

Cláudio Lourenço <pt.smooke@gmail.com> writes:

> The deleted files from index, are just ignored (we think the bug comes
> from here).

Not really.  In general, "git checkout b" (no path arguments,
checking out the branch "b") will try to keep the local changes you
made to the index and to the working tree for a path that are the
same between your current branch and the branch "b".  So it is
perfectly normal to see:

        $ git checkout master
        $ git ls-files file
        file
	... ok, the master branch has "file"
	$ git diff master side | grep file
        ... ok, the side branch also has it and it is the same
        $ git rm file
        $ git checkout side
	D	file
	Switched to branch 'side'

So it actually _actively_ pays attention to paths deleted or
modified in the index.

Another thing it does is when the local change to the index matches
that of the branch you are switching to, checkout is allowed even if
path is different between two branches.

When checking the differences between the two branches (the current
and the new), unpack-trees notices that the path "something" is not
present in "b" branch, and even though your current branch and the
index differs (the index does not have "something" as you have
removed it), it thinks it is OK for the result to not have it (which
is correct).  And when it does that, it forgets that a new path
"something/f1" still needs to be kept (which is not correct), which
is where the problem you are seeing comes from, methinks.

Re: Help understanding git checkout behavior

[Junio C Hamano]

Junio C Hamano <gitster@pobox.com> writes:

> When checking the differences between the two branches (the current
> and the new), unpack-trees notices that the path "something" is not
> present in "b" branch, and even though your current branch and the
> index differs (the index does not have "something" as you have
> removed it), it thinks it is OK for the result to not have it (which
> is correct).  And when it does that, it forgets that a new path
> "something/f1" still needs to be kept (which is not correct), which
> is where the problem you are seeing comes from, methinks.

So there are two paths involved in this two-way merge.

The master branch (HEAD) has "something", but not "something/f1".
The index does not have "something", but has "something/f1".
The "b" branch does not have either.

For path "something", the rule 2 in the "Two Tree Merge" section of
Documentation/git-read-tree.txt applies.  It does not exist in the
index, it does exist in HEAD, and it does not exist in the other
branch we are checking out.  The result should be to remove it.

For path "something/f1", the rule 4 ought to apply.  The index entry
for it is up to date with respect to the working tree file
(i.e. clean), the HEAD does not have it, and the other branch does
not have it either.  We should be keeping it intact across the
checkout.  For whatever reason, this is not happening and I suspect
that is because we have to remove "something" due to rule 2.

I just checked the history of unpack-trees code (which is the
underlying machinery of read-tree, which in turn is the machinery
used to check out another branch by "git checkout"), and I suspect
that this particular case has never worked.

Re: Help understanding git checkout behavior

[Jeff King]

On Mon, Jun 11, 2012 at 02:34:42PM -0700, Junio C Hamano wrote:

> So there are two paths involved in this two-way merge.
> 
> The master branch (HEAD) has "something", but not "something/f1".
> The index does not have "something", but has "something/f1".
> The "b" branch does not have either.
> 
> For path "something", the rule 2 in the "Two Tree Merge" section of
> Documentation/git-read-tree.txt applies.  It does not exist in the
> index, it does exist in HEAD, and it does not exist in the other
> branch we are checking out.  The result should be to remove it.
> 
> For path "something/f1", the rule 4 ought to apply.  The index entry
> for it is up to date with respect to the working tree file
> (i.e. clean), the HEAD does not have it, and the other branch does
> not have it either.  We should be keeping it intact across the
> checkout.  For whatever reason, this is not happening and I suspect
> that is because we have to remove "something" due to rule 2.

I think the problem is in verify_clean_subdirectory, which checks that
we do not have untracked files in the subdirectory, nor modifications
between the index and working tree. But I do not see it checking whether
we have modifications from the HEAD.

> I just checked the history of unpack-trees code (which is the
> underlying machinery of read-tree, which in turn is the machinery
> used to check out another branch by "git checkout"), and I suspect
> that this particular case has never worked.

Yeah, I verified it back to v1.6.x, but didn't bother going further
back.

-Peff

Re: Help understanding git checkout behavior

[Jeff King]

On Mon, Jun 11, 2012 at 05:47:05PM -0400, Jeff King wrote:

> > I just checked the history of unpack-trees code (which is the
> > underlying machinery of read-tree, which in turn is the machinery
> > used to check out another branch by "git checkout"), and I suspect
> > that this particular case has never worked.
> 
> Yeah, I verified it back to v1.6.x, but didn't bother going further
> back.

Actually, it was broken by c819353 (Fix switching to a branch with D/F
when current branch has file D., 2007-03-15).

However, before that the check was too tight, and says:

  fatal: Untracked working tree file 'something' would be removed by merge.

which is not really correct, either.

-Peff

Re: Help understanding git checkout behavior

[Junio C Hamano]

Jeff King <peff@peff.net> writes:

> I think the problem is in verify_clean_subdirectory, which checks that
> we do not have untracked files in the subdirectory, nor modifications
> between the index and working tree. But I do not see it checking whether
> we have modifications from the HEAD.

I actually think "comparison with HEAD" is a red herring.  As long
as the version in the index matches the version in the other branch
we are checking out, it does not matter if the version in the index
is different from the version in HEAD (case 4).  Also if the version
in the index is new and neither HEAD nor the other branch has it, we
should keep it (case 2).  And we should error out if these are not
possible.

I did a bit more digging on this; even though I am not going to
continue it further today, here is a snapshot of my current
thinking.

After replacing "something" with "something/f1" in the index,
attempting to "read-tree -m -u master b" (which is what checkout is
about) decides that the regular file "something" should not exist,
because it is in "master" but not in "b", so it calls

	deleted_entry(ce = master's version, old = NULL)

where "old" is the version of "something" in the index, i.e. "does
not exist".  This in turn calls verify_absent(ce) to make sure that
it is OK to remove regular file "something".  verify_absent() checks
the path "something" with lstat(), and it would be happy if there
weren't "something", as there won't be anything necessary to do in
that case.

But it finds a directory.  It calls check_ok_to_remove() on it.
This is where things go wrong.  This function is to see if it is ok
to nuke the entire directory "something", for the more common case
where we are about to create a different "something" there. It is an
appropriate check if we were trying to create a version of regular
file "something" from the branch we are trying to check out, but it
is a wrong thing to do when we are not interested in touching
"something" in any way.  We do not have regular file "something"
now, and after checking out the branch, we do not want to have
regular file "something" there, either ---so all we have to do is to
do nothing!

Instead, it says "Ah, something/f1 is clean", sets o->cache_bottom
to skip it, and the machinery loses sight of that path.

Probably we need to vet the caller of verify_absent() to see why
each caller wants to call it.  Some may be about to create a new
thing there, and really want to make sure there is nothing there
after they are done.  But this caller, when it _knows_ the path is
already removed (it can tell in check_ok_to_remove() after lstat()
says there is a directory "something" there---at that point we know
the regular file "something" cannot be there), should just be happy
and let the later callers to look at the remaining cache entries
without marking everything under something/* has been processed.

Or something like that.

Re: Help understanding git checkout behavior

[Vincent van Ravesteijn]

Op 11-6-2012 18:52, Cláudio Lourenço schreef:
> We are not sure if this behavior has an explanation of if it is just a bug.
>
> We are hoping that you could clarify us about this operation or
> recommend us some place where we can find some useful information
> about this...

I think it is a bug. The file "something/f1" should be retained when 
switching branches. So, checkout should fail because "something" would 
get overwritten by checkout, but it doesn't.

Vincent