New branch `agda-master` working with the master version of Agda

[andreasabel]

Following #3012 (comment), I added a branch agda-master forked from master and cherry-picked the commits that make it build with the master version of Agda

• Fixes for agda/agda#8533: eta equality is no longer inferred #2986
• Make irrelevant-recompute unsafe #3012

In comparison with experimental, @jamesmckinna 's commit 2f84dcc is missing that did not pick cleanly and is also not required to make the std-lib work with Agda's master.
Also, since agda-master is not tracked by CI I did not pick CI-related commits from experimental (meaning 008f12c which is anyway outdated now).

The branch agda-master could replace experimental.
I did not want to do this now because experimental contains @jamesmckinna work 2f84dcc whose status I do not know.
If someone picks it onto the agda-master branch, I think we could go ahead to replace experimental without losses.

If #3012 lands on master, the agda-master branch should be rebased on master with the #3012-specific commit removed. (I'd certainly volunteer to do this.)

[jamesmckinna]

@andreasabel thanks for doing this, and in principle it seems a good idea to have a 'clean' branch for upstream evolution of Agda, given that we seem to have got stuck with suitably bringing the experimental branch up-to-date with the new master branch of stdlib (I confess I've always been shaky about the what, the when, and the why, especially as to when we should try to keep it up-to-date other than at stdlib release moments).

You draw attention to two commits for which I'm notionally responsible, together with PR #3012 as something 'experimental' which nevertheless might instead more cleanly be merged into master.

Tackling the two commits which concern the final deprecation of Reveal/inspect, indeed my understanding had always been that they depend on changes to with... in ... eq syntax which have not been released under the planned Agda v2.9.0. On that basis, I'd be happy for them to wait for that release (and remain status:blocked), but am I correct in understanding that the current Agda master branch would support that final deprecation, in which case is there an objection in principle to making those commits to the stdlib agda-master branch? I don't think there's huge urgency either way, other than our desire to have this change for Agda-stdlib-v3.0, which I guess now is intended eventually to be released after Agda-v2.9.0.

As to #3012, again I think there may be misunderstandings on my part about the way forward:

• one argument for merging it into master is that it itself is intended as a 'provisional' fix, marking as unsafe something which may eventually be made safe again with @jespercockx 's various PRs in this area?
• and as such, one which we would rather have merged sooner rather than later, so that agda-stdlib/master be 'as safe/consistent as possible' now
• and, that if experimental is now to be 'abandoned' as a branch in favour of agda-master (and perhaps with a different responsibility for maintaining such a branch as each of agda/master and agda-stdlib/master evolve?), that subsequent repairs to irrelevance, and their consequences for Data.Irrelevant, be merged into agda-master?

I realise even as I write this that my words betray what are perhaps deep misunderstandings on my part about your intentions for the agda-master branch (and its relationship to experimental?), but none of the above issues strike me as critical to resolve, on the time axis at least. I don't think there's pressure from the stdlib maintenance team to have a 'bleeding-edge' stdlib developed hand-in-hand with the bleeding edge of Agda itself, but you seem to be saying that that is in fact something desirable from the main Agda development side?

[MatthewDaggitt]

The scheme is pretty easy: the experimental branch can be brought up-to-date whenever. It is usually brought up to date when some breaking change happens on the dev branch of Agda. So yes, happy for it to be renamed to agda-master if that would make the intention clearer and easier.

[shhyou]

Agda HEAD's std-lib submodule currently points to the unmerged commit 9a543dc in #3012. Should it switch to agda-master?

[jespercockx]

Agda HEAD's std-lib submodule currently points to the unmerged commit 9a543dc in #3012. Should it switch to agda-master?

Yes, this was just a temporary measure until the discussion around the experimental/agda-master branch was finished. If the situation is clear now, we should update the commit to point to agda-master instead.