Stream: Ltac2

Topic: robust compatible Constr.Unsafe

Gaëtan Gilbert (Nov 13 2023 at 15:51):

@Pierre-Marie Pédrot has this plan to reduce backwards incompatible changes when dealing with the unsafe constr API

instead of the current

Ltac2 Type kind := [ ... | Proj (projection, constr) | ... ]. (* version before relevance was added *)
Ltac2 @ external kind : constr -> kind.
Ltac2 @ external make : kind -> constr.

we would have

Ltac2 Type proj_kind.
Ltac2 Type kind := [ ... | Proj (proj_kind) | ... ].
Ltac2 @ external kind : constr -> kind.
Ltac2 @ external make : kind -> constr.

Ltac2 @ external proj_kind_projection : proj_kind -> projection.
(* same for constr *)

Ltac2 Type proj_kind_builder := { proj_kind_projection : projection option; proj_kind_constr : constr option }.
Ltac2 default_proj_kind_builder := { proj_kind_projection := None; proj_kind_constr := None }.
Ltac2 @ external build_proj_kind : proj_kind_builder -> proj_kind.
(* when a field is None, pick something backwards compatible if possible otherwise throw some error *)

then the change to add the relevance would be

• add proj_kind_relevance : proj_kind -> relevance
• add a field proj_kind_relevance : relevance option to proj_kind_builder, add proj_kind_relevance := None to the default value, build_proj_kind uses Relevant when passed None

Accesses are enforced to be forward compatible, and building can be made forward compatible by always using { default_proj_kind_builder with ...} (we would need to turn the "all fields are listed" error into a warning)

Does this approach seem reasonable to everyone? RFC

Michael Soegtrop (Nov 13 2023 at 16:17):

I have only very few functions which are affected by this, so fine with me.

I expect that very few people use the unsafe API directly and instead use it in some wrappers of their own, so I would expect that changes in the unsafe API typically don't lead to large porting effort. Also (afair) it is documented that one should expect porting efforts when using the unsafe API, so IMHO this is perfectly fine.

Ike Mulder (Nov 14 2023 at 10:40):

For context: do I understand correctly that the arguments to the Proj constructor are changing in a new Coq version?
This seems reasonable. I assume any possible future changes to other constructors would get the same treatment?

Last updated: Oct 12 2024 at 11:01 UTC