Pierre Roux (Aug 30 2021 at 13:03): 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?
Pierre-Marie Pédrot (Aug 30 2021 at 13:05):You mean, if something specific is evaluated?
Pierre-Marie Pédrot (Aug 30 2021 at 13:05):or from ML code?
Pierre-Marie Pédrot (Aug 30 2021 at 13:05):for the latter there is the reduction_effect_hook thingy
Pierre Roux (Aug 30 2021 at 13:26):Yes, if something is evaluated.
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.
Pierre-Marie Pédrot (Aug 30 2021 at 13:27):What's the use case?
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)
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.
Pierre-Marie Pédrot (Aug 30 2021 at 13:29):It could return not only the parsed data, but also a list of messages.
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.
Pierre Roux (Aug 30 2021 at 13:29):That was also my idea, thanks for the confirmation.
Pierre-Marie Pédrot (Aug 30 2021 at 13:30):reduction_effect is a hack
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.
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: Oct 13 2024 at 01:02 UTC