Ability to return values from Ltac2 to Ltac1 is not documented

[RalfJung]

Description of the problem

Currently, ltac2:(...) quotations only accept terms that return (). Any time data needs to be passed from ltac2 to ltac1, one has to write things in continuation-passing style, which can require major refactoring of existing code and makes gradual migration a lot harder.

It would be great if there was a way to directly return values of type Ltac1.t from ltac2 to ltac1.

Cc @robbertkrebbers

Coq Version

8.18.0

[SkySkimmer]

8.18 should have ltac2val:() #17575

[robbertkrebbers]

What's the reason we need a special ltac2val: for that. Why cannot ltac2: be generalized to also support value-returning tactics?

[RalfJung]

Ah, I seemed to remember that there was some improvement here but https://coq.inria.fr/refman/proof-engine/ltac2.html?highlight=ltac2#compatibility-layer-with-ltac1 doesn't mention ltac2val so I didn't find it.

What's the reason we need a special ltac2val: for that. Why cannot ltac2: be generalized to also support value-returning tactics?

I guess it is similar to the "tactic must either have side-effects or return a value but not both" restriction? Though that can be worked-around with match goal so it's not really water-tight, and I never understood where this limitation comes from either.

[SkySkimmer]

What's the reason we need a special ltac2val: for that. Why cannot ltac2: be generalized to also support value-returning tactics?

@ppedrot didn't want it #17575 (comment)

[RalfJung]

Would it make sense to keep this open to track the lack of documentation of ltac2val?

[SkySkimmer]

What lack of documentation? It's in there https://coq.inria.fr/doc/master/refman/proof-engine/ltac2.html#ltac2-from-ltac1

[RalfJung]

I could have sworn I did Ctrl-f ltac2val and didn't find anything... maybe that was an outdated page? Or I'm unable to type.

Sorry for the noise.