git/branch misunderstanding

Stream: new members

[Antoine Chambert-Loir]

Opening file#data.setoid.partition.lean in a supposedly clean master branch (I had just done git checkout master, leanproject up, I got an error message on line 248,
invalid field notation, 'sup_id_set_eq_sUnion' is not a valid "field" because environment does not contain 'finset.sup_id_set_eq_sUnion'

What did I do wrong ?

[Julian Berman]

git checkout master does not necessarily mean the file is clean -- what does/did git status say?

[Julian Berman]

Specifically If the file has uncommitted changes and you switch branches, git brings those changes along as you switch branches and doesn't throw them away (as doing so would lose data -- it will error if somehow your changes conflict with where you're switching to, but otherwise it just silently preserves the changes).

[Arthur Paulino]

:point_up: It's particularly useful when you're editing a file and then you suddenly realize you're working on the master branch before committing your changes. Then you can checkout to a new branch and your changes will go with you

[Antoine Chambert-Loir]

Now, git statusgives me a bunch of mathlib files which are supposedly modified (but I didn't modify them myself, probably leanproject did).

[Julian Berman]

If you're sure you want to discard the changes, you can run git restore . (don't forget the period, i.e. "the whole directory here")

[Julian Berman]

always safe to run git diff first just in case.

[Antoine Chambert-Loir]

I probably did a bunch of wrong stuff. It is probably simpler to create a new branch from scratch (there are only a few files of which I have a copy, so I won't lose anything…).