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.