Agda-stdlib: Release of 0.15

[MatthewDaggitt]

Given that quite a lot of stuff has stacked up since the last release, I'd like to release 0.15 relatively soon, before the next wave of additions arrives.

The problem is that several commits have been made to master that depend on the upcoming release of Agda 2.5.4. and so we can't release the library as is. In future I'd like to create a branch for such commits so that we can keep them separate from master and therefore avoid this problem later on.

One solution is just to wait for 2.5.4 (agda/agda#2875) to release. Alternatively does someone more conversant with Git know of someway of extracting the problem commits from master into a separate branch so the release can go ahead sooner?

[gallais]

What needs to be removed?

• [ ] Word Builtin
• [ ] Sigma Builtin
• [ ] Size Builtin
• [ ] Support for older GHCs

[MatthewDaggitt]

The size builtins need changing as well. Do we need to remove the removal of support for GHC versions (e.g. 2033814d1f118401a37484390fdb5b75b83e6bb4)?

[gallais]

Do we need to remove the removal of support for GHC versions (e.g. 2033814)?

That sounds reasonable.

[fredrikNordvallForsberg]

• [ ] Renaming of Agda.Builtin.Size.ω (751f8f56a9d28637b5b86a9758c39871ce30eab6)

Edit: Sorry, that's what @MatthewDaggitt meant by "The size builtins need changing as well" of course.

[gallais]

So many rebase conflicts in the CHANGELOG...

[gallais]

What should we do with this one?

https://github.com/agda/agda-stdlib/commit/e9055a78b2514d316bc06827d24d492422826886

[MatthewDaggitt]

Ah sorry. That's undoubtedly my fault...

[MatthewDaggitt]

What should we do with this one? e9055a7

I don't think it matters right? The corresponding file for the main installation of Agda 2.5.3 should ensure the right requirements are met? You can remove it if you want though.

[gallais]

I've pushed https://github.com/agda/agda-stdlib/tree/master-rewritten
and I'm currently checking that shaving the 5 last commits off makes the stdlib agda-2.5.3 compatible

[gallais]

Ok, https://github.com/agda/agda-stdlib/tree/release-0.15 works with agda-2.5.3.
What I suggest is to adopt the rewritten history as the new master and release that new master minus the 5 latest patches as 0.15

[andreasabel]

One solution is just to wait for 2.5.4 (agda/agda#2875) to release.

Ah, yes, don't wait for that to happen very soon... ;-)

[asr]

+1 for detaching the release of the standard library from the release of Agda.

Do we need to remove the removal of support for GHC versions (e.g. 2033814)?

Yes. Agda 2.5.3 supports GHC 7.8.4.

What should we do with this one? e9055a7

I don't think it matters right? The corresponding file for the main installation of Agda 2.5.3 should ensure the right requirements are met?

Right.

[MatthewDaggitt]

Thanks so much @gallais!

Ok, https://github.com/agda/agda-stdlib/tree/release-0.15 works with agda-2.5.3.
What I suggest is to adopt the rewritten history as the new master and release that new master minus the 5 latest patches as 0.15

Yes so I think the best thing to do is as follows:

• Move the current contents of branch master to a new branch agda-future (or some similarly meaningful name)
• Make the branch 0.15 the new master.

Anytime the core language changes, we update agda-future. When a new version of Agda releases we can then cherrypick the commits we need from agda-future to merge into master.

[MatthewDaggitt]

Sorry, I think I'm speaking gibberish with my proposed moves. Please ignore them! What would be ideal is to have at the end:

• master contains everything minus the 5 latest patches
• agda-future contains everything including the 5 latest patches.

[gallais]

Sounds good to me. Should someone able to bypass the fact that master is locked
push-force the content of release-0.15 on master?

As for agda-future (or experimental or whathever we call it), I'd argue that we should
try to always have the extra patches floated all the way to the top of the history. This way
when a new version of Agda is released we can simply move these on top of master and
release. No need to rebase a big chunk of changes, and no rewritten history for the user.

[MatthewDaggitt]

Sounds good to me. Should someone able to bypass the fact that master is locked
push-force the content of release-0.15 on master?

That sounds good. Who can do that? Presumably @andreasabel ?

As for agda-future (or experimental or whathever we call it), I'd argue that we should
try to always have the extra patches floated all the way to the top of the history. This way
when a new version of Agda is released we can simply move these on top of master and
release. No need to rebase a big chunk of changes, and no rewritten history for the user.

That sounds like a good idea, although how would you do that? Presumably from time-to-time we'd want to merge master into experimental to keep it up-to-date. Maybe we only perform the merge after a release...

[gallais]

Presumably from time-to-time we'd want to merge master into experimental to keep it up-to-date.

Oh yeah, most definitely. But if you rebase instead of merging then you
can commute the commits to make sure you always float the additional
ones to the top.

It should be a lot easier to do continuously rather than trying to rewrite
the history after 60 commits have passed by like we just did.

[MatthewDaggitt]

Ah okay, that makes sense. I'll spend some time reading up on rebase :smile:

[asr]

Should someone able to bypass the fact that master is locked push-force the content of release-0.15 on master?

I guess I can bypass the lock (I know I can remove it). Why do you need to push-force release-0.15 into master (I haven't followed the discussion closely).

[MatthewDaggitt]

I guess I can bypass the lock (I know I can remove it). Why do you need to push-force release-0.15 into master (I haven't followed the discussion closely).

Currently master contains commits that use new features in Agda 2.5.4. We want to perform a release of the library, without having to wait for 2.5.4.

To that end @gallais has done a heroic job separating out the offending commits. Currently release-0.15 contains everything except the offending commits, while master-rewritten contains everything including the offending commits.

[asr]

If we push-force release-0.15 into master how are you planning to update the subproject commit in the Agda repo? I guess release-0.15 doesn't type check with the current Agda stable-2.5 and master branches.

[gallais]

The Agda repo should point to the experimental branch. It's currently called
master-rewritten but we should adopt a better name for it.

[MatthewDaggitt]

I'm happy with experimental as a name.

[asr]

@MatthewDaggitt, I included you in the Owners team, so you can make the push-force.

[asr]

I'm happy with experimental as a name.

And if Agda stable and master diverge, we could use the experimental-stable and experimental-master names.

[MatthewDaggitt]

@MatthewDaggitt, I included you in the Owners team, so you can make the push-force.

Eek, not sure that's a good idea :worried:

Looking at the second answer here, should I instead be running the following?

git checkout master
git revert -n HEAD~67..HEAD                   # Revert all commits since 0.14 release
git commit -m "reverting to release 0.14"
git merge release-0.15
git push

This should get us to where we want, without doing a push --force that'll screw over anyone who has a cloned copy of the repository right?

[asr]

doing a push --force that'll screw over anyone who has a cloned copy of the repository right?

Right. (I should have mentioned that the push-force isn't a good idea).

[MatthewDaggitt]

Right. (I should have mentioned that the push-force isn't a good idea).

That's okay. You implied it strongly!

[MatthewDaggitt]

Took a while, but I've finally got it to go through this morning. master is now in the state that we want it (i.e. the results of all commits not compatible with 2.5.4 removed). Doesn't even screw up the history, only a single commit :smile: If you look here you can see a list of all the things removed.

I'll try and fix-up #191 and then release either this afternoon or early next week.

[gallais]

Thanks! I'll try to rebase master-rewritten so that it is current master + extras (and I'll rename it to experimental at the same time).

Edit: I think we're good! https://github.com/agda/agda-stdlib/tree/experimental
Edit2: Hmmm. Looks like I can't cleanly git pull --rebase . master on experimental after having added something. Crap.
Edit3: Don't know why I get stupid CHANGELOG conflicts in that rebase....
Edit4: the trick seems to be to cherry-pick these extra commits instead of trying to rebase.

Now we can do:

git checkout master
touch test
git add test
git commit -m "test"
git checkout experimental
git pull --rebase . master

and the commit introducing the new test file will be sitting on top of the big revert, under the changes which are 2.5.4-specific

[MatthewDaggitt]

Okay, I've done everything for the release except update the main Agda repository and send out the email.

Can I just get confirmation from someone in the know, of which branch to push the updated standard lib submodule to in Agda, master or stable-2.5?

[asr]

Can I just get confirmation from someone in the know, of which branch to push the updated standard lib submodule to in Agda, master or stable-2.5?

1. push to stable-2.5
2. merge stable-2.5 into master

[gallais]

Do remember however that only the experimental branch is compatible
with the dev version of Agda.

[MatthewDaggitt]

Do remember however that only the experimental branch is compatible
with the dev version of Agda.

Hmm that is a good point. What do you think the best solution is?

[asr]

Do remember however that only the experimental branch is compatible
with the dev version of Agda.

Right. I was talking about Agda branches, that is,

1. push experimental to Agda stable-2.5
2. merge Agda stable-2.5 into Agda master

[MatthewDaggitt]

Great, thanks for the help both of you.

I've also added a file notes/updating-experimental on how to update the new experimental branch so I don't forget.

[MatthewDaggitt]

There was also a small backwards compatibility issue in Relation.Binary.Sum picked up when running the benchmark test suite, which is why the commit history isn't quite so clean as it could be. I've got it squished now though, and I've retagged v0.15.

[asr]

Thank you for the release.

I've got it squished now though, and I've retagged v0.15.

FWIW. I pulled the library after you created the tag but before you retagged it, so I needed to delete the local tag.

[MatthewDaggitt]

@asr apologies. I had hoped that no-one would have been so quick of the mark to get the old tag in the couple of hours it was around. In the end I thought it was better to have a small possibility of a tagging issue than to ship the library with the backwards compatibility bug.

I hope it wasn't too painful.