search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
575 stars 237 forks source link

remove everything deprecated from v1.3 (and before) #2338

Open JacquesCarette opened 6 months ago

JacquesCarette commented 6 months ago

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 commented 6 months ago

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 :cry:

JacquesCarette commented 6 months ago

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 commented 6 months ago

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 commented 6 months ago

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 commented 6 months ago

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 commented 6 months ago

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 commented 6 months ago

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

jamesmckinna commented 5 months ago

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

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

JacquesCarette commented 5 months ago

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."