No deprecation for Data.List.Categorical in v2.0?

[andreasabel]

It seems Data.List.Categorical simply vanishes when going from v1.7 to v2.0.
Will there be any deprecation module for backwards compatible? (I thought this was the general policy of the std-lib.)

[jamesmckinna]

See the v2.0 CHANGELOG... we put out an RFC here on the Zulip, and the mailing list, for issue #1636 / the associated PR #1735, which was sufficiently gross a global change that I pushed for it to be strongly breaking, without deprecation warnings...

[andreasabel]

@jamesmckinna
Ah, seems I have to pay the price now for unsubscribing from general notifications for this repo.

I just had the impression that the standard-library always had strong emphasis on backwards-compatibility and explicit deprecation, and this tradition seems discontinued now.
With Agda lacking CPP pragmas like #if MIN_VERSION_standard_library(2,0,0) (hello Haskell!), I see no way to support both standard-library 1.7 and 2.0 in my Agda development, other than having branches in my repo. I would prefer not having to maintain branches.
It would be nice if one could use both the latest release of the library and the current master. Say once 2.0 is out, I could address all the deprecations, drop 1.7, and then live with 2.0 and the new master.

In principle, if module A is renamed to module B, would it be hard to keep A as deprecated module that simply reexports all of B?

module Data.List.Categorical where
{-# WARNING_ON_IMPORT "Deprecated: Import Data.List.Effectful instead" #-}
open import Data.List.Effectful public

https://agda.readthedocs.io/en/v2.6.3/language/pragmas.html#warning-pragma

[jamesmckinna]

(Sorry not to have replied to this sooner, as the originator of PR #1735, but not the original issue #1636) I can see the argument for Data.*.Effectful being shadowed by deprecated Data.*.Categorical modules, but I think the price I/we did not wish to pay was that of maintaining an entire deprecated hierarchy below Category.* as well (which would have delayed the whole point of the change by at least one version bump).

UPDATED: Closed by PR #1946