[fix] issue 1865 for all the raw bundles added in #1755 [coda to Issue1858/ PR 1861]

[jamesmckinna]

No description provided.

[MatthewDaggitt]

While you're here any chance you could do the same thing for the bundles moved in 578e7a6 as well? Then we could close the issue 😄

[jamesmckinna]

Yes! not tonight I think (SPLS all day, plus I'm driving there and back...) ;-)
UPDATED: done? (please check... ;-))

[jamesmckinna]

cf. discussion in PR #1852: I'll do the re-imports, and then rename/deprecate the names. On second thoughts, I won't do the second, and leave the inconsistency to mop up later. But my obsessive compulsion towards consistency is strong...
UPDATED: it got the better of me

[jamesmckinna]

How do I achieve strikethrough in the name of the PR? to reflect that it is now more general?
Ah, I see... nothing escapes github's gaze...

[MatthewDaggitt]

I'm afraid something has gone wrong in your merging here, and you've picked up a load of extraneous commits to Relation.Nullary that make it very difficult to review. Any chance you could try to clean it up?

[jamesmckinna]

Aaargh... apologies. I'll try to do this (more) slowly and carefully.
I shouldn't have sat down to do it in a burst of wild energy after an already long day including 100-mile round trip drive.
Let me know how I'm getting on.

[jamesmckinna]

@MatthewDaggitt I've gone through each of the 13 commits on my branch issue1858 associated with this PR, and they all seem good, so I've commented to that effect on the individual commits there.

That leaves commits 167fc7f and fd37e5d and I think I don't understand how they came to be part of this PR. And the PR itself records 16 commits, not 15 as I might have expected (my 13 plus 2 spurious).

Commit c2302f4 appears in the PR, but not on my branch, it would seem, so I'm now thoroughly confused.
Ah, I see it was part of #1844/#1862 which was successfully merged in a while back. Sorry!

Each of the commits on the branch seem OK, and of the others, obviously yours and Nathan's are the rogue elements.

What I don't understand is how to remove 167fc7f and fd37e5d from this PR (or, alternatively, given that GH says that the branch can successfully be merged, how to shield your reviewing eyes from them... :-(). Advice welcome! Hopefully the above detective work is a start, at least.

Can you review the branch commits?

[MatthewDaggitt]

So the easiest way is to run git rebase -i HEAD~16 and then remove the lines containing the commits that you don't want. Then run git push -f.

In general this is not encouraged as it changes the history, so if other people were working on this branch then you would royally screw things up for them. But in this case I think its fine!

[jamesmckinna]

Hmmm. I tried this, and expected to see 16 commits, of which 3 could be removed. But in fact the 16 I saw went way further back in the history than I might have expected, and the merge commits which caused all the trouble seem not to appear in the list for potential rebasing... so now I have gone somewhat passed my horizon of clear understanding of what's going on.

UPDATED Have tried again on another copy (issue1858-BAD now deleted) of the branch (going back to HEAD~9 which seems to actually be where the trouble started, but then the rebase failed as it could not replay one of the commits.

UPDATED How do I make a fresh branch (and from what starting point, and only include the commits actually on the issue1858 branch? I can see that this is perhaps the intention behind the rebase, but it didn't seem to work...). Have now tried this (see below), cherry-picking the old commits one-by-one from a backup copy (issue1858-BAK )of this branch, and re-committting them to this one. Hopefully that works!

[jamesmckinna]

OK, don't know what went wrong this time around: I tried cherry-picking the commits from the backup branch (but there seemed to be only 12 of them this time, not 13), but now have two merge conflicts arising from (what?).
What's the remedy? pull the changes from agda/master, resolve merge conflicts and then push?

[jamesmckinna]

OK, perhaps that has now restored the missing commits in Data.Integer.Base (did I somehow fail to cherry-pick one of them?) and resolved the conflicts in CHANGELOG (which seemed to have a spurious entry for parity coming from #1852...???
UPDATED aaaargh that PR had already been merged, but maybe that's OK on this branch still).

[jamesmckinna]

(n+1)th time is the charm? Sigh.

[MatthewDaggitt]

Otherwise looks great now! Thanks for fixing the commits. Hope it wasn't too difficult in the end!

[MatthewDaggitt]

Thanks for sticking with this one!