Release version v0.5 while changing the release process

[felixwellen]

I think we should take some current state (e.g. the current master, whenever we will do what this issue says) and declare it to be release v0.5 of the cubical library (which works with agda 2.6.3). And then we should just go back to more or less track agda master. With that I mean, we should move forward, whenever there is a new agda feature we want to use and keep track of the agda version the library builds with. This shouldn't happen too often, but it might mean library developers have a bit more work to keep up with agda. One instance of a new agda feature we can use, is described in #1010.

What do you think about doing that @mortberg , @ecavallo ?

[felixwellen]

I also thought the new release process should then be that we release a matching version for whenever there is an agda release. Note that at the last agda release, we released a version of cubical for the old agda version, since we say that the current master build with the current stable release. The standard library does what I propose as the new release process and it seems to be what people expect.

[felixwellen]

Talked with @mortberg and decided: We make a release now, v0.5, and add a new row to the table in README, which says: "current main | SOME_FIXED_COMMIT_OF_AGDA ".

[felixwellen]

This means, we have to update the CI, to use the SOME_FIXED_COMMIT_OF_AGDA.

[jpoiret]

Latest master chokes on

cubical/Cubical/Homotopy/HopfInvariant/Homomorphism.agda:698,7-11
(fst f x) != (fst g x) of type (Susp (S₊ (suc n)))
when checking that the expression cool has type _x_5616 ≡ _y_5617

I don't know anything about these files so I didn't dig further.

[mortberg]

Latest master chokes on

cubical/Cubical/Homotopy/HopfInvariant/Homomorphism.agda:698,7-11
(fst f x) != (fst g x) of type (Susp (S₊ (suc n)))
when checking that the expression cool has type _x_5616 ≡ _y_5617

I don't know anything about these files so I didn't dig further.

@aljungstrom Can you look into this?

[felixwellen]

This is very good to know. I'll do the release anyway, since it is independent of this problem - the fixed agda commit will be the v2.6.3 tag at first.

[felixwellen]

Done up to post-release tasks.

[felixwellen]

There were no post-release tasks. The library seems to check with current Agda master, so we can move forward if there is need to do so.

[jpoiret]

Setting up CI now would help noticing breaking changes faster instead of having to look at a whole release's changelog. It will eat up more CI time the way it is currently set up though as the job will also rebuild Agda itself. I wonder if/how we could re-use the main agda repo's artifacts.

[felixwellen]

I'm not sure I get what you want to achieve - if it is about detecting breaking chances in agda, shouldn't it be more something for the agda ci?

[felixwellen]

Moving this discussion to a new issue, closing this one.

[felixwellen]

Hope I got it right, what your comment was about.