Karl Palmskog (Jul 24 2020 at 08:22): 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?
Pierre-Marie Pédrot (Jul 24 2020 at 08:24):I think you should report a bug.
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.
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.
Is this something the fabled minimizer could be used for?
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: Jun 04 2023 at 19:30 UTC