Re: [isabelle] Simplifier: renamed bound variable ":000" to ":000a"



On Wed, Feb 17, 2010 at 12:20 PM, Makarius <makarius at sketis.net> wrote:
> On Wed, 17 Feb 2010, Brian Huffman wrote:
>
>> Sometimes the simplifier produces a warning message that looks like this:
>>
>> ### Simplifier: renamed bound variable ":000" to ":000a"
>>
>> Should I care?
>>
>> If it is important, what does this message mean---does it indicate a
>> problem?
>>
>> If it is *not* important, why is this message printed at all? (Or at
>> least, why is it printed even when the debugging flag is not turned on?)
>
> This message indicates a situation where some Simplifier component (simproc,
> looper, solver, or similar) does not observe the proof context.
...
> At some point I would like to see these remaining holes in existing proof
> tools being filled.  Although there is no immediate problem, this is a bit
> strange -- just like plugging the power cord to switch off a computer
> instead of a clean shutdown.

If I understand you correctly, the "renamed bound variable" message
indicates a problem in the *implementation* of some part of the
simplifier. So the message is only potentially useful to developers,
and not ordinary users.

With this in mind, I ask again: Why is the message printed when the
debugging flag is not set?

Maybe this is better phrased as a feature request: I would like
Isabelle to refrain from printing warning messages unless they provide
meaningful information that users can act upon. Either the "renamed
bound variable" warning should be suppressed, or else it should tell
users where to send a bug report. Otherwise, it is just noise.

- Brian





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