Stream: MetaCoq

Topic: Options in `tm_util`


view this post on Zulip 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:

Cc @Matthieu Sozeau

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Maxime Dénès (Mar 29 2023 at 07:40):

And which would be loaded by both independent ones.

view this post on Zulip Matthieu Sozeau (Mar 30 2023 at 06:00):

Right, indeed

view this post on Zulip Matthieu Sozeau (Mar 30 2023 at 06:00):

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

view this post on Zulip 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).

view this post on Zulip Matthieu Sozeau (Mar 30 2023 at 08:15):

Good enough !


Last updated: Jul 23 2024 at 20:01 UTC