Re: [isabelle] Isabelle2015-RC3: Spurious "Duplicate rewrite rule" warnings during Sledgehammer invocation.



On Fri, 8 May 2015, Lars Noschinski wrote:

These stray warnings had a nice little side-effect for me: They notified me that sledgehammer had found a proof. As I often switch to the output or query panels when sledgehammer is busy, this was often useful.

BTW: https://xkcd.com/1172/ ;)

This well-known cartoon proves that the words "bug" and "feature" are meaningless.

A problem with the current situation is that we still have too many "modes" of sledgehammer, some obsolete after the removal of TTY / Proof General.

Before the change bcd9a70342be, I did not know that the main entry point of sledgehammer has moved elsewhere. There are more details like treatment of "using" facts that are unified by it, not just disabling warnings.


Incremental results can be emitted indepently of that as official information messages. I don't know why this was not tried before, probably also because of too much "modes" confusion.

Presently on the release ramp, we should concentrate on the real problems, such as robust Windows support.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.