[isabelle-dev] Metis: Unused Theorem Reduces Run-Time?

[Jasmin Christian Blanchette]

Hi Tjark,

Am 20.01.2013 um 22:21 schrieb Tjark Weber:

> On Fri, 2013-01-18 at 19:29 +0100, Jasmin Christian Blanchette wrote:
>> What's your concrete suggestion here?
> 
> It's more of a curiosity than an issue, of course. Otherwise, I would
> suggest to: First, make sure that the behavior is not due to a bug or
> silly inefficiency in the metis code. Second, offer a way to suppress
> the warning.

"First" is quite a bit of work, if you want to bring it into a format that Joe Hurd can understand, assuming he even has the time to look into it.

To suppress the warning, one trick is to ensure that the theorem has no name hint, e.g.

    mythm[THEN asm_rl]

or (if it's not polymorphic) pipe it in with "using mythm apply -". The first trick could be made cleaner through a new attribute, e.g. "silent" or "nameless".

I'd rather not add any feature directly to "metis" because it's unlikely to be discovered by the few users who will run into the issue, and care -- but I encourage you to experiment with this, and if your idiom spreads so that it has more than one user we could consider it for inclusion in Isabelle [*].

Cheers,

Jasmin

[*] A rule of thumb I remember from industry was to wait until we had the same feature request at least three times before implementing anything. That of course made more sense w.r.t. a large user base (~ 10 000 to 100 000) than for the Isabelle community.