ltac2: operations to manipulate transparent states

[MathisBD]

Adds low-level operations to manipulate transparent states in Ltac2.

1. I wrote small wrappers around TransparentState in the file ltac2/tac2stdlib.ml. I'm not sure this is the right place for this code.
2. The API exposed in TransparentState.v is quite redundant because many functions are mirrored for constants, projections, and variables. Would it be cleaner to create a small Ltac2 type like:

Ltac2 Type entry := [
| Variable (ident)
| Constant (constant)
| Projection (projection)
].

And have the functions in TransparentState.v take as input an entry instead?

[ppedrot]

Would it be cleaner to create a small Ltac2 type like

No, this would expose too much internal details and not be future-proof whenever we want to add data there. ADTs should only be in the FFI whenever we want to expose a view type, not when we take arguments across distinct domains. (IMO some of the Ltac2 APIs are already too fragile in this regard, but that doesn't prevent from trying to make the situation worse.)

[ppedrot]

(The more reasonable alternative to an ADT is an opaque type with injection functions.)

[MathisBD]

@coqbot run full ci

[thomas-lamiaux]

@SkySkimmer looks good to me, should the milestones be 9.2 for @andres-erbsen ?

[ppedrot]

should the milestones be 9.2

What's not clear about the concept of a release here?

[thomas-lamiaux]

Was the freeze done now ? I don't get it

[ppedrot]

We've branched a while ago, yes.

[thomas-lamiaux]

This was not merged #21541 so we can still put 9.2+rc1 right ?

[ppedrot]

we can still put 9.2+rc1 right ?

The RM (@tabareau) is sovereign, but the very concept of the branch is to put a hold on the 9.2 development. Only fix PRs should be backported (when reasonable) and in theory we collectively agree for some feature PRs on the verge of being ready to be backported before the branch. This is a feature PR that was written after the branch, ergo it's not backportable.

[thomas-lamiaux]

This is a feature PR that was written after the branch, ergo it's not backportable.

In the case of pure extensions like this one, that do not create overlays, I personally disagree since we have only a release every 6 months, and consequently it gets the feature to most people which do not work with master with 6 months delay. But it is up to the developers doing the releases to choose.

[tabareau]

The PR #21541 is just a "working PR" to test the CI before backporting and is not supposed to be merged.

That said, the problem of providing an untested extension just before the release is that it prevents from modifying it in few weeks if you realize it should be done differently.

So 9.3.

[SkySkimmer]

I'm not sure if we should expose these operations. In #19117 there is some discussion about changing Hint Constants Opaque to set a default but not change constants which were explicitly set transparent, I'm not sure how well that would work with combining transparent states.

[thomas-lamiaux]

This low-level API are useful to a small minority of users that want a very fine control.
I would imagine, they would be interested in recovering the transparency state for some hint databases, and take the union or sth like that ? @andres-erbsen would you have such a need ?

[ppedrot]

@SkySkimmer this would typically be done at the HintDB API level, not the transparent state one AFAIU. I'm envisioning a system where we keep two different TS for each hintdb and switch one with the other with a flag. So I don't think exposing this kind of operations is problematic.

[SkySkimmer]

needs changelog

[Janno]

2. The API exposed in TransparentState.v is quite redundant because many functions are mirrored for constants, projections, and variables. Would it be cleaner to create a small Ltac2 type like:

Ltac2 Type entry := [
| Variable (ident)
| Constant (constant)
| Projection (projection)
].

A different way to go would be to (abstractly) expose the structure of OCaml's TransparentState.t. We could then use the tag infrastructure in FSet.v to provide operations on the individual parts. We do need a new Pred.v file with an FSet-like interface that accounts for the difference between Set and Predicate. But at least that we only have to write once and it might even come in handy in other places.

It's a bit more work up-front but it does make the interface to TransparentState.t a whole lot nicer. It would look like this, I think:

Module TransparentState.
Ltac2 Type t.
Ltac2 @ external empty : t := .. (* unchanged *)
Ltac2 @ external full : t := .. (* unchanged *)
Ltac2 @ external get_constants : constant_tag Pred.t := .. (* same for variables, projections *)
Ltac2 @ set_constants : constant_tag Pred.t -> t -> t := .. (* same for variables, projections *)

[ppedrot]

@Janno This is adding more coupling with the implementation, I think this is a bad idea. We should be as abstract as possible, especially when it comes to collections as it could be very inefficient to convert back and from different representations.

[SkySkimmer]

@coqbot run full ci

[SkySkimmer]

@coqbot merge now