I guess the answer is no, but do we have a way to trigger a warning during
You mean, if something specific is evaluated?
or from ML code?
for the latter there is the reduction_effect_hook thingy
Yes, if something is evaluated.
If you have access to a ML plugin, I'd recommend registering the reduction_effet_hook somewhere.
What's the use case?
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)
Hmm, then for that I'd rather have a dedicated API from the Coq notation mechanism side.
It could return not only the parsed data, but also a list of messages.
Why a dedicated API? Your initial suggestion of using
reduction_effect seems just fine for this use case.
That was also my idea, thanks for the confirmation.
reduction_effect is a hack
It would also feel strange to have the parser/printer in vernacular while the warning is hardcoded in a plugin.
it would affect anyone using the actual constant for other purposes, and it's not really guaranteed to fire properly either
Last updated: Feb 01 2023 at 13:03 UTC