Stream: MetaCoq

Topic: Options in `tm_util`

Maxime Dénès (Mar 29 2023 at 05:49):

Hi there,

I'm trying to understand the following piece of code : https://github.com/MetaCoq/metacoq/blob/coq-8.16/template-coq/src/tm_util.ml#L14

It gets in the way of parsing/execution separation, because it tries to read all table options values at linking time. I'm missing a bit of context to try to fix it:

• what is "the extractable plugin" ?
• what does it mean to load the extractable and template plugins "at the same time"? There surely is one linked before the other, right? Why not declare the option in that one using the normal API?

Cc @Matthieu Sozeau

Matthieu Sozeau (Mar 29 2023 at 06:10):

The problem is that the two plugins are independent, they could be loaded in any order. If there was a way for declare_bool_option_and_ref to just return an existing option's read method instead of failing on redefinition then this could be solved

Maxime Dénès (Mar 29 2023 at 07:40):

I see. The way of doing it with the current API and no hacks would be to have a common parent plugin which declares the option, I guess, right?

Maxime Dénès (Mar 29 2023 at 07:40):

And which would be loaded by both independent ones.

Matthieu Sozeau (Mar 30 2023 at 06:00):

Right, indeed

Matthieu Sozeau (Mar 30 2023 at 06:00):

I’ve no time to implement that at this time though ;)

Maxime Dénès (Mar 30 2023 at 07:23):

I added a small get_option_value API meanwhile, to make things a little cleaner, and not query all options when you just need one (which was incidentally breaking the phase separation).

Matthieu Sozeau (Mar 30 2023 at 08:15):

Good enough !

Last updated: Oct 13 2024 at 01:02 UTC