Release v2.1.1

[JacquesCarette]

Now that it is finally released, we should make sure we're compatible with it (both to see if v2.1 is, and current development/v2.2 is). If memory serves me correctly, neither are - but we should make sure all appropriate wikis are clear about that!

[JacquesCarette]

(I was looking at what labels to add to this, and didn't see anything that fit all that well?)

[jamesmckinna]

Now that it is finally released, we should make sure we're compatible with it (both to see if v2.1 is, and current development/v2.2 is). If memory serves me correctly, neither are - but we should make sure all appropriate wikis are clear about that!

Oh no!

At least as far as v2.1 is concerned, it should simply be badged as compatible with v2.6.4.3... but that does put pressure on us to make v2.2 release (!) to be 'eventually compatible' with 2.7? Can we fix this up at release time, or will the CI for new commits on existing PRs expect, in particular --exact-split? This may very well be a major source of breaking... sigh ;-)

But as for my current v2.2 developments, I'm not quite ready to make the 'great leap forward'... yet!

[andreasabel]

Could you release 2.1.1 instead with just the minimal fixes over 2.1 for Agda 2.7.0? (Some fixes are on the experimental branch.)

[JacquesCarette]

That was implicitly my goal with this issue, i.e. get a 2.1.1 release out if it's needed (and then folding that into 2.2), and indeed experimental is already (partway?) there.

[iblech]

I just checked: Just two commits from the experimental branch need to be cherry-picked to tag v2.1 in order to establish compatibility with Agda 2.7.0: 586f56a and c7d65e0

[MatthewDaggitt]

Yup, I will try get it sorted tomorrow

…

On Mon, 19 Aug 2024, 21:46 Ingo Blechschmidt, ***@***.***> wrote: I just checked: Just two commits from the experimental branch need to be cherry-picked to tag v2.1 in order to establish compatibility with Agda 2.7.0: 586f56a <586f56a> and c7d65e0 <c7d65e0> — Reply to this email directly, view it on GitHub <#2461 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAP26EUQZPQ752JXVTN6IT3ZSHZL3AVCNFSM6AAAAABMUAHTISVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDEOJWGYZDAOBXHE> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[MatthewDaggitt]

Created the first release candidate.

[MatthewDaggitt]

Second release candidate created

[mechvel]

I try testing lib-2.1.1-rc2 on my large application.
I type-checks everything.
But I also test compilation examples to executable.
And this produces internal error due to a bug in Agda 2.7.0 (see news in the Agda bug tracker).
Therefore I cannot reliably test lib-2.1.1-rc2 before this bug in Agda is fixed.

[mechvel]

More precisely, it is compiled by a certain sequence of type-check-compile commands and produces "internal error" for another sequence.
Most probably this effect does depend on the standard library version.

[andreasabel]

@mechvel wrote:

And this produces internal error due to a bug in Agda 2.7.0

This refers to

• Code only reachable from display forms not serialised in Agda 2.7.0  agda#7436

One would speculate that it is a regression in the .agdai creation. I do not think it is related to the standard library.

[jamesmckinna]

Milestone is v2.2.1? Rather than v2.1.1?

[JacquesCarette]

I think that's just a typo, I'll see if I can fix it.

[MatthewDaggitt]

I've made the release. @gallais any chance you could generate and upload the website docs? I still can't get it running on my computer 😢

[jamesmckinna]

@MatthewDaggitt @gallais I've just tried following the release-guide.txt instructions, and had several/many problems, so suggest raising a separate continuous-integration/admin issue?
In short order, working with the supplied instructions:

• cabal run GenerateEverything.hs should be superseded by make setup, since we moved the Everything* files to doc (also, for my version of cabal, it objects, suggesting instead cabal run GenerateEverything, which does work, but is out of step with the new destination for the generated files...)
• git checkout gh-pages falls over, because of clashes between that branch and, AFAICT, on all the files added/updated since the v2.1 release... did we fail to update the gh-pages branch after the v2.1 release? or is something else broken?

At that point, I bailed...

[gallais]

It should have landed now: https://agda.github.io/agda-stdlib/

[jamesmckinna]

Out of interest, @gallais , were you able to diagnose how/why Matthew and I were having problems as above?

[gallais]

I had similar issues with cabal but I do not dare to suggest a solution as everyone seems
to have a different version using a different mechanism to run scripts.

I don't know why the location of the EverythingX.agda files would matter given the command
line to generate the html includes all of -i. -idoc -isrc. It could be you had stray files left in the
doc/ directory?

I don't know why anything would fall over when you checkout gh-pages.

[jamesmckinna]

Thanks @gallais I may try a fresh clone after merging #2473 ...

[jamesmckinna]

I got myself confused as to whether this issue is closed by #2473 or not...

[MatthewDaggitt]

It was closed by @gallais uploading the release branch 😄 Rebasing master so that it includes the changes from v2.1.1 is not per se part of the release process I think...

[MatthewDaggitt]

Thanks everyone for their work!