Stream: Coq devs & plugin devs

Topic: Ignoring "Nothing to inject" warnings


view this post on Zulip Karl Palmskog (Jul 24 2020 at 08:22):

Many of the MathComp-using projects I maintain have a bunch of Warning: Nothing to inject. However, there is no warning code associated with this message, so I can't suppress it. This seems inconsistent with nearly any other warning I've encountered - is it by design, or should report an issue?

view this post on Zulip Pierre-Marie P├ędrot (Jul 24 2020 at 08:24):

I think you should report a bug.

view this post on Zulip Enrico Tassi (Jul 24 2020 at 08:29):

Indeed this "warning" predates the warning system, and the merge of ssr into Coq came after the new warning system was introduced and all warnings ported to the new system. What a stroke of luck. Please open an issue about porting this warning to the current warning system.

view this post on Zulip Karl Palmskog (Jul 24 2020 at 08:40):

done: https://github.com/coq/coq/issues/12746

However, providing a minimal example that triggers this requires more cycles than I currently have. Best I can offer is

File "./Core/DepMaps.v", line 52, characters 0-47:
Warning: Nothing to inject.

for https://github.com/DistributedComponents/disel/blob/25a437666b4772f49264b24dc91005bcccc70f7d/Core/DepMaps.v#L52

Is this something the fabled minimizer could be used for?

view this post on Zulip Enrico Tassi (Jul 24 2020 at 08:44):

I guess Goal forall b : bool, b -> False. move=> b [h]. reises the warning as well. As some point injection started to fail rather than doing nothing on equations that could not be "injected", while used to fail only on non-equations. The problem is that forgetting an extra [.] in ssr is easy and 99% of our formulas are equations (hidden . = true). So we had to turn the error into something else, because we had gazillions of instances. If we port the warning to the current system one can easily switch between warning, error or nothing, and that could help getting rid of these little mistakes.


Last updated: Oct 16 2021 at 07:02 UTC