Stream: Coq users

Topic: Triggering a warning during Compute


view this post on Zulip Pierre Roux (Aug 30 2021 at 13:03):

I guess the answer is no, but do we have a way to trigger a warning during Compute?

view this post on Zulip Pierre-Marie Pédrot (Aug 30 2021 at 13:05):

You mean, if something specific is evaluated?

view this post on Zulip Pierre-Marie Pédrot (Aug 30 2021 at 13:05):

or from ML code?

view this post on Zulip Pierre-Marie Pédrot (Aug 30 2021 at 13:05):

for the latter there is the reduction_effect_hook thingy

view this post on Zulip Pierre Roux (Aug 30 2021 at 13:26):

Yes, if something is evaluated.

view this post on Zulip Pierre-Marie Pédrot (Aug 30 2021 at 13:27):

If you have access to a ML plugin, I'd recommend registering the reduction_effet_hook somewhere.

view this post on Zulip Pierre-Marie Pédrot (Aug 30 2021 at 13:27):

What's the use case?

view this post on Zulip Pierre Roux (Aug 30 2021 at 13:28):

my goal would be to replace the OCaml implem of the primitive float parser with a vernacular one, while retaining the warning when parsing non exact floats (like 0.1)

view this post on Zulip Pierre-Marie Pédrot (Aug 30 2021 at 13:28):

Hmm, then for that I'd rather have a dedicated API from the Coq notation mechanism side.

view this post on Zulip Pierre-Marie Pédrot (Aug 30 2021 at 13:29):

It could return not only the parsed data, but also a list of messages.

view this post on Zulip Guillaume Melquiond (Aug 30 2021 at 13:29):

Why a dedicated API? Your initial suggestion of using reduction_effect seems just fine for this use case.

view this post on Zulip Pierre Roux (Aug 30 2021 at 13:29):

That was also my idea, thanks for the confirmation.

view this post on Zulip Pierre-Marie Pédrot (Aug 30 2021 at 13:30):

reduction_effect is a hack

view this post on Zulip Pierre Roux (Aug 30 2021 at 13:30):

It would also feel strange to have the parser/printer in vernacular while the warning is hardcoded in a plugin.

view this post on Zulip Pierre-Marie Pédrot (Aug 30 2021 at 13:30):

it would affect anyone using the actual constant for other purposes, and it's not really guaranteed to fire properly either


Last updated: Sep 23 2023 at 15:01 UTC