Add coercion hook

[proux01]

This adds a hook in pretyping/coercion.ml to enable programming more elaborate coercions in an external metalanguage (Ltac, Ltac2, Elpi,...). This was developped during CUDW 2023 along with a coq-elpi interface: https://github.com/proux01/coq-elpi/tree/coercion_hook

Fixes / closes #????

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

• Opened overlay pull requests.

[ejgallego]

Needs to be made safe wrt backtracking

[gares]

Needs to be made safe wrt backtracking

I don't think so. This pr is a twin of

#16654

[ejgallego]

Needs to be made safe wrt backtracking

I don't think so. This pr is a twin of

#16654

I understood that that PR was only for "experimentation", but see my review.

I think that both that PR and this PR need amending as they are breaking a critical use case, breaking unrelated files / backtrack of the plugin require. Both of the approaches hinted above should work (indirection or ~local:true)

[gares]

I think you want to error if the same hook is declared twice.

[proux01]

@ejgallego your request should now be fullfilled, could you please update your review if you agree this is indeed the case?

[ejgallego]

@ejgallego your request should now be fullfilled, could you please update your review if you agree this is indeed the case?

Thanks @proux01 , I'm happy with any mechanism that works with the current VernacState approach, so loading a plugin in a document doesn't leak to other unrelated documents. If @SkySkimmer and/or @ppedrot are OK with the approach here please feel free to dismiss my review.

[I would prefer if we had an API that was actually always safe instead of placing the burden in the plugin writer, but as long as things work properly on backtrack I don't mind so much here. But indeed, if we are gonna start making these parts of Coq extensible IMHO we need a principled approach]

[gares]

This PR seems to validate that property.

[ejgallego]

This PR seems to validate that property.

Yes you are correct I somehow misread it. I think we have some similar code already in the system so at some point it could be nice to refactor this pattern into something that could be shared.

[gares]

@coqbot run full ci

[proux01]

I think we have some similar code already in the system

Any idea where? I thought the same but couldn't find any example.

[ejgallego]

I think we have some similar code already in the system

Any idea where? I thought the same but couldn't find any example.

We don't need to solve this now, but I think a couple of places where we do something similar is in the primitive notations and grammar extension code, but @SkySkimmer @herbelin know better.

[SkySkimmer]

Those have a similar principle of indirection through strings, but they're different enough that it's not clearly factorizable IMO

[ejgallego]

Those have a similar principle of indirection through strings, but they're different enough that it's not clearly factorizable IMO

Too bad :( For #17807 we want to copy this code but I'm unsure if that's enought as to make this "Summary-friendly" Hook API available in as Summary.Hook.Make(F)

[gares]

@coqbot merge now