Agda-stdlib: Concurrent development of agda-stdlib and agda-categories

[JacquesCarette]

This is basically a 'protocol' question: there are a few things currently in agda-categories that are CT independent, and really belong in agda-stdlib. [A couple have been moved already.] I'd like to move a few more.

The protocol part comes in synchronizing. I don't want users of agda-categories, perhaps even users of the development branch of it, to have to use the development version of agda-stdlib. But I'd like to make sure that future agda-categories works cleanly with current dev agda-stdlib.

The obvious thing to do is to borrow the strategy of agda-stdlib, once removed:

1. master branch is compatible with current released version
2. experimental branch is compatible with current master version (of agda-stdlib)
3. alpha branch is compatible with experimental of agda-stdlib and master of agda.

I think the above "makes sense", but if somehow my reasoning is flawed, I'd like to catch that before I enshrined any of the above in Travis scripts!

I'm putting this question here, as we can accommodate lots of different things on our side, it's making sure I've got the agda-stdlib side of the protocol correct that I'm most concerned with.

I should probably ping @HuStmpHrrr and @sstucki too.

[gallais]

That seems sensible to me.

Note that you can ask for a specific version number in the .agda-lib file
for agda-categories to ensure that Agda will pick up the right version of the
stdlib if users have multiple ones installed.

[sstucki]

SGTM too.

Maybe alpha doesn't have to be a permanent branch, but more like a collection of wip branches that get deleted after releases. Then again, branches are cheap, so 🤷‍♂️

[JacquesCarette]

Using a version number is likely a good idea, at least for master and likely experimental.

I think it makes sense for alpha to be a branch, as it represents a commitment that "eventually" those features will appear in a release -- unlike wip- branches, which may never be finished.

[HuStmpHrrr]

sounds cool. having a version specified is a good idea too.

[MatthewDaggitt]

Note that you can ask for a specific version number in the .agda-lib file
for agda-categories to ensure that Agda will pick up the right version of the
stdlib if users have multiple ones installed.

Does that mean we need to start prepending the version number to the name of the standard library?

Maybe alpha doesn't have to be a permanent branch, but more like a collection of wip branches that get deleted after releases.

@sstucki I suspect you should have a single permanent branch for alpha, otherwise you run the risk of ending up with a _lot_ of merge conflicts.

[sstucki]

@sstucki I suspect you should have a single permanent branch for alpha, otherwise you run the risk of ending up with a _lot_ of merge conflicts.

fair enough.

[MatthewDaggitt]

@JacquesCarette I'm going to close this as I think it's been resolved to everyone's satisfaction. Feel free to reopen if not!