Email Gateway (Aug 18 2022 at 14:46): Email Gateway (Aug 18 2022 at 14:46):From: Brian Huffman <brianh@cs.pdx.edu>
Sometimes the simplifier produces a warning message that looks like this:
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?)
Email Gateway (Aug 18 2022 at 14:46):From: Makarius <makarius@sketis.net>
This message indicates a situation where some Simplifier component
(simproc, looper, solver, or similar) does not observe the proof context.
When simplifying abstractions, fresh variables need to be invented -- the
"bounds" part of the simpset records already used auxiliary variables.
Sometimes this information is lost, because some tool restarts
simplification in an empty context (in ancient days tools could work from
the background theory alone). The Simplifier is smart enough to detect the
clash and tries to repair it, which appears to work in most situations.
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.
Makarius
Email Gateway (Aug 18 2022 at 14:46):From: Brian Huffman <brianh@cs.pdx.edu>
On Wed, Feb 17, 2010 at 12:20 PM, Makarius <makarius@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.
Email Gateway (Aug 18 2022 at 14:46):From: Makarius <makarius@sketis.net>
On Wed, 17 Feb 2010, Brian Huffman wrote:
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.
No, it indicates that the Simplifier has just repaired a problem
introduced in user space, notably one of these Simplifier plugins that can
be defined in the library. Since the main library in question is actually
main HOL, one could nonetheless argue that it is somehow relevant to
developers.
I would like Isabelle to refrain from printing warning messages unless
they provide meaningful information that users can act upon.
I am usually trying hard to keep messages relevant, and fight spam
wherever possible, although this often seems futile. As messages are
cleaned up here, new ones emerge there.
Concerning this particular message, I would not just switch it of because
it is an important reminder that certain things in HOL still need to be
sorted out. Maybe you can help looking through all the simprocs ...
Makarius
Last updated: Nov 21 2024 at 12:39 UTC