move ZModulo to test suite

[andres-erbsen]

#16914

• Added / updated test-suite.
• Added changelog.

[andres-erbsen]

@coqbot run full ci

[andres-erbsen]

elpi failure is also on master 8e03144

[proux01]

@andres-erbsen note that the usual policy before removing something is that potential users should have been able to see a deprecation warning for at least two versions. So I'm afraid we cannot remove that now.

[andres-erbsen]

Are you sure this is the policy even for changes with backwards-compatible fixups? The most relevant written record I can find says

it should always be possible for a project written in Coq to be compatible with two successive major versions, features must be deprecated in one major version before they can be removed in the next, Coq developers must have a good estimate of the effort it takes to fix a project with respect to a given change, and finally and most importantly, breaking changes must be clearly documented with clear recommendations explaining how to fix a project.

(from the dissertation of @Zimmi48, https://hal.inria.fr/tel-02451322v1 page 44)

Removals based on similar reasoning have been approved and merged as well, e.g. #15268.

[Alizter]

The fact that we cannot deprecate entire modules is a missing feature that would be very useful here.

[proux01]

@andres-erbsen indeed I was wrong with the requirement for deprecation in two releases, one can be enough under some circumstances.
I still think that we should offer users a deprecation warning in at least one release.

[Alizter]

Here is an issue about deprecating libraries #8032

[andres-erbsen]

The deprecation was announced in the previous release here. For a library that was actually used or understood to be useful, I can see that aiming for a higher level of communication (some solution to #8032, perhaps manual) would have value, but AFAIK this file has only caused confusion so far so I don't think it is worth holding back with its removal any longer.

[Alizter]

@andres-erbsen As it has been deprecated previously, I support you removing this.

[Zimmi48]

Given that CI reveals no issues, I also support this removal (but it should be documented in a changelog).

[ppedrot]

AFAICT this is ready and needs an assignee. @proux01 maybe?

[proux01]

Maybe I should clarify my position here: I still think this deserves proper deprecation warnings and I won't merge without them (I would otheriwse) but I will not oppose if anyone else think it's fine without warnings.

[ppedrot]

Either we merge this quickly, or we do deprecate the relevant definitions before the 8.18 branch. Since there is not much momentum for the first option, maybe the second should be considered?

[JasonGross]

Now that 8.18 has branched, this can be merged into master, right?

[andres-erbsen]

Gentle ping @coq/number-maintainers

[Alizter]

@coqbot run full ci

[andres-erbsen]

Full CI failures look unrelated, refman failure is fixed in latest version.

[Alizter]

@coqbot merge now

[coqbot-app]

@Alizter: You cannot merge this PR because:

• There is still a needs: full CI label.

[Alizter]

@coqbot merge now