Zulip Chat Archive

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

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

@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....

Kevin Buzzard (Nov 14 2018 at 08:19):

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: Dec 20 2023 at 11:08 UTC