search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
96 stars 21 forks source link

Deprecating structures/mixins/factories #436

Open pi8027 opened 2 months ago

pi8027 commented 2 months ago

Although HB comes with the idea of preserving backward compatibility (e.g., by turning a mixin into a factory), we sometimes want to rename (or even remove?) existing structures, mixins, and factories.

For example, we recently renamed a factory of complemented lattices in order.v: https://github.com/math-comp/math-comp/blob/6634f9a81d2882d40b87db3ccb99f79cc14c2b5b/mathcomp/ssreflect/order.v#L4953-L4970 and renamed the HB classes of some archimedean structures: https://github.com/math-comp/math-comp/blob/df3d86612e26e595b9b9c16bd561233f2da33e63/mathcomp/algebra/archimedean.v#L742-L775

As you can see, we have to declare several deprecation notations to deprecate a structure because a structure consists of several Coq declarations. It would be convenient if HB had a command that generates deprecation code like these.

pi8027 commented 2 months ago

IMO, we unlikely want to remove a structure, but we may want to remove a factory in favor of another factory or mixin when we find the former useless.

pi8027 commented 2 months ago

If Coq had a feature to deprecate a module, we wouldn't need this feature in HB:

#[deprecated(since="mathcomp 2.3.0")]
Module hasRelativeComplement := BDistrLattice_hasSectionalComplement.