## Stream: PR reviews

### Topic: rebasing

#### Scott Morrison (Nov 13 2018 at 22:49):

Hi @Reid Barton, @Johan Commelin. I'm about to rebase limits-others-new. This is going to leave adjunctions and sheaf in a strange position.

#### Scott Morrison (Nov 13 2018 at 22:49):

Would it be okay if I rebased either of both of those onto the new limits branch?

#### Scott Morrison (Nov 13 2018 at 23:02):

It would mean doing a force push to community/adjunctions and/or to community/sheaf, so I'd need to get the okay that you're not actively working on that branch.

#### Reid Barton (Nov 14 2018 at 00:01):

Yes, feel free, or I am also happy to take care of the rebase myself.

#### Scott Morrison (Nov 14 2018 at 00:22):

Maybe it's best if you do it, so I don't mess up authorship information.

#### Scott Morrison (Nov 14 2018 at 00:24):

oh, worked it out :-)

#### Johan Commelin (Nov 14 2018 at 06:35):

@Scott Morrison Please go ahead with rebasing sheaf. I have no idea how to do that...

#### Scott Morrison (Nov 14 2018 at 07:22):

Done! Your old history is now on the sheaf-old branch, but if everything looks okay we can delete that.

#### Johan Commelin (Nov 14 2018 at 07:28):

Thanks, I'll take a look!

#### Johan Commelin (Nov 14 2018 at 07:30):

@Scott Morrison Hmm, that's easier said than done.

#### Johan Commelin (Nov 14 2018 at 07:30):

How do I take a look?

#### Johan Commelin (Nov 14 2018 at 07:30):

git pull origin sheaf gives me an aweful lot of merge conflicts in files that are not sheaf.lean

#### Keeley Hoek (Nov 14 2018 at 07:43):

Hi Johan, Try

git merge --abort
git checkout sheaf
git branch -m sheaf-old
git branch sheaf-old -u origin/sheaf-old
git fetch
git checkout -b sheaf origin/sheaf


@Johan Commelin

#### Keeley Hoek (Nov 14 2018 at 07:44):

The new sheafs will be sheaf, the old sheafs will be sheaf-old

#### Johan Commelin (Nov 14 2018 at 07:48):

Thanks @Keeley Hoek, that seems to have worked git-wise. Now checking if Lean is happy by recompiling.

#### Johan Commelin (Nov 14 2018 at 08:18):

Oh boy, lots of red squiggles....

how christmassy

#### Scott Morrison (Nov 14 2018 at 08:20):

Thanks Keeley for the instructions!

#### Scott Morrison (Nov 14 2018 at 08:20):

Are things working, Johan?

#### Johan Commelin (Nov 14 2018 at 08:20):

Nope, not really...

#### Johan Commelin (Nov 14 2018 at 08:21):

I feel like I should start taking a more structured approach. Because this file has been growing like a kludge of hacks.

#### Scott Morrison (Nov 14 2018 at 08:21):

Sorry, let me try compiling here. :-)

#### Scott Morrison (Nov 14 2018 at 09:10):

@Johan Commelin, all but one error fixed, which is just an unfinished proof at the bottom.

#### Scott Morrison (Nov 14 2018 at 09:11):

There was a universe issue, a missing simp lemma, and the syntax of yoneda had changed.

#### Johan Commelin (Nov 14 2018 at 11:17):

@Scott Morrison Thanks a lot! (Sorry, I had seminars and then lunch...)

Last updated: May 09 2021 at 14:10 UTC