Non-backwards compatibility of master/v2.0 with agda-2.6.3 via Reflection.TCM

[jamesmckinna]

PR #1972 introduces a dependency in Reflection.TCM on Builtin for agda-2.6.4 which is not backwards compatible with agda-2.6.3, which has, until now, been the stable version for most agda-stdlib development of v2.0 modules.

In time, this won't matter, but for the time being, is this desirable?

Easy remedy appears to be simply to comment out the offending imports (the last line) from Builtin in Reflection.TCM.

[MatthewDaggitt]

I mean there is no point to #1972 without those. So I think you're just suggesting the commit be reverted?

In my opinion, the library's goal in modules like these is to re-export the Agda primitives with an improved interface. I feel like we're breaking that contract if we don't provide the latest primitives.

[jamesmckinna]

I think that you are more across the significance of the PR (and its upstream agda origin... where there was even a discussion of putting off the change to 2.6.5...) than I am, and from the point of view of a library developer, rather than an end-user, I don't perceive/experience the benefits... yet. Perhaps it's also a cue to me to read label:upstream as also potentially entailing a system version change (which in my world view, counts as label:breaking as well).

It felt, to me at least, that this was another tricky step in walking the tightrope of compatibility... that even though we have broken the link between v.1.7.x and v2.y (for many good reasons), nevertheless it was worth considering maintaining the agda/stdlib version compatibility across that transition. Of course (?), lots of these phenomena arise because of how long we have spent getting v2.0 in shape to release relative to the main system development cycle, and in the future things won't/shouldn't involve quite so many breaking changes...

I raised the issue partly out of my own innate conservatism (towards 'what works stably'; I'm not a 'bleeding edge' kind of person) as regards upgrade policy... (but/and I can always patch my local copy of the library if I so wish during development ;-)), and partly because it represents a double breaking shift for end users, who will have to upgrade both their library and their system versions in order to profit from the last 2+years of effort on library development. But maybe that's not a big price to pay, beyond making me upgrade sooner than I would otherwise have wished ;-)

And partly... the still-reverberating echoes of #1939 ... as well as the recent, but thankfully amicable as well as speedy, resolution of the various issues around v1.7.3.

[MatthewDaggitt]

Perhaps it's also a cue to me to read label:upstream as also potentially entailing a system version change (which in my world view, counts as label:breaking as well).

So there is some truth in that, but it's not 100%. The interface in Agda.Primitive can change, and the standard library can mask that change to the users.

Of course (?), lots of these phenomena arise because of how long we have spent getting v2.0 in shape to release relative to the main system development cycle, and in the future things won't/shouldn't involve quite so many breaking changes...

I'm not sure this is true. This issue occurs almost every release of Agda. If you look at the list of standard library versions you linked to above, only once before in the history of the library have managed to support two versions of Agda the same time.

I raised the issue partly out of my own innate conservatism (towards 'what works stably'; I'm not a 'bleeding edge' kind of person) as regards upgrade policy...

I think there is a choice though. You can either be not bleeding edge and stay at both the previous version of Agda and the previous version of the library, or you can upgrade both. Yes they're coupled, but it is the standard Agda library after all. You'd expect it to make full use of the interface provided by Agda, and therefore be more affected than other libraries.

I think ultimately, the only way that I could be convinced that putting significant effort in maintaining backwards/forwards compatibility would be a good idea, is if and when we get CPP macros in Agda that actually let us inspect the Agda version in the code. Without those, we may be able to hack support in special cases, but in general it's an impossible task 😞