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
From: Konstantin Khomoutov <hidden> Date: 2016-06-15 22:54:02
On Mon, 11 Jun 2012 17:52:26 +0100
Cláudio Lourenço [off-list ref] 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.
[...]
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' ?
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, [off-list ref] wrote:
Cláudio Lourenço [off-list ref] a écrit :
quoted
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
From: Vincent van Ravesteijn <hidden> Date: 2016-06-15 22:54:02
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
From: Jeff King <hidden> Date: 2016-06-15 22:54:02
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:
quoted
quoted
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