remove everything deprecated from v1.3 (and before)

[JacquesCarette]

Since v1.2 (and before) were removed from v2.0, I'm removing v1.3 from v2.1.

We probably could add in v1.4 as well, as there were very few things deprecated for that release. v1.5 was a different matter.

[MatthewDaggitt]

Unfortunately this is a breaking change and so cannot be done before v3.0. It's the reason I tried to clean out a lot of stuff before v2.0 😢

[JacquesCarette]

It is a 'tiny' breaking change that shouldn't affect many people as long as they look at warnings. Do we really have to wait until v3.0 for this?

[MatthewDaggitt]

Well the contract is that deprecation warnings aren't fatal, and we certainly don't enforce (only advice) that people should immediately follow the warnings. I've definitely in my own (non-Agda) code suppressed warnings as I have no plans to upgrade a package, and you can do the same in Agda.

Under those circumstances this is a large, not a tiny, breaking change. The idea is that all Agda code, with whatever flags, should not be broken by a minor version bump of the library.

[JacquesCarette]

I'll whine that the Agda devs break things in this way all the time in releases (2.6.3 and 2.6.5 are not compatible because Reflection changed), so holding the moral high ground on stdlib seems kind of pointless?

But I'll accept that this is unlikely to sway anyone, and that this is likely not going to be accepted until v3.0. I'm just now extra-eager for it!

If this is going to be v3.0, maybe I should go ahead and remove all stuff deprecate until say v1.5 (inclusive) ?

[MatthewDaggitt]

I'll whine that the Agda devs break things in this way all the time in releases (2.6.3 and 2.6.5 are not compatible because Reflection changed), so holding the moral high ground on stdlib seems kind of pointless?

While I agree Agda frequently breaks things, that doesn't mean there's no point to maintaining backwards compatibility in the standard library. It will still make migrating versions much easier for users, compared to if both Agda and the standard library were making separate breaking changes at the same time.

If this is going to be v3.0, maybe I should go ahead and remove all stuff deprecate until say v1.5 (inclusive) ?

In v3.0 I'd advocate removing everything deprecated in versions v1.X.

[JacquesCarette]

In v3.0 I'd advocate removing everything deprecated in versions v1.X.

So I could go ahead and do that as part of this PR?

[MatthewDaggitt]

Yes, under the proviso that it will sit around for a long time and it may bit rot somewhat in that time...

[jamesmckinna]

My sympathies are with @JacquesCarette , but over the last three (four?) years I have come to appreciate @MatthewDaggitt 's insistence on a more conservative/conservationist approach ... not least because having to adhere to it has taught me a lot about 'infrastructure' (the Zero/Initial&Terminal refactoring of Algebra.Construct was especially instructive in that regard, IIRC...), as well as discovering that many of my 'first thought, best thought' PRs tend not to have survived scrutiny, in favour of smaller, better/better-focused ones.

Deprecation is tricky, not least for the knock-on viscosity it implies/entails. I take this PR in part as a desire to reduce this as an ambient quality of stdlib as a software artefact... but I've come to see that as an inevitable aspect of 'community' software. The Lean developers have given themselves great latitude to take the opposite path, seemingly without cost, but different economies of scale seem to be in place there.

That said, I'm hoping that

• we try for a v2.1 release soon
• we actively engage (in whatever form) with candidate designs/issues for v3.0
• we leave existing v3.0-badged issues/PRs open, but maybe not add new v3.0 PRs for the time being; issues are fine, though!

'Just' my opinions though, writing in a personal capacity...

[JacquesCarette]

To me the trickiest part is that we don't have good access to 'the community', i.e. those people who use stdlib, especially the ones who try to use it as much as possible. [We don't care about Agda users who work on their own libraries and don't use stdlib.] If we knew which way they skewed (conservative or move-fast-and-break-things like Lean), it would be a lot easier to "go with what the community wants."

[jamesmckinna]

The main thing missing from this PR is to go through and check which of the many warning-suppression pragmas

{-# OPTIONS --warn=noUserWarning #-}

that we have added over the years are still needed?

Apologies in advance if you have already done such smoke testing!