Email Gateway (Aug 22 2022 at 09:46): Email Gateway (Aug 22 2022 at 09:46):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Overwriting congruence rule for “HOL.If”
Should these really be warning messages or should we classify them as “trace” or something similar?
Warnings light up fairly prominently in jedit these days, and such messages distract for warnings that you want to do something about.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:46):From: Christian Sternagel <c.sternagel@gmail.com>
I agree with Gerwin that this is too much "noise".
On a related note: (At least for me) also warnings like
Rule already declared as introduction (intro)
for when you add an existing intro rule as safe intro, e.g.,
apply (auto intro!: exI)
are distracting, since I always have the feeling that something is not
quite right with my theory file as long as there are warnings.
cheers
chris
Email Gateway (Aug 22 2022 at 09:46):From: Larry Paulson <lp15@cam.ac.uk>
I agree. That is not something to warn about.
Larry
Email Gateway (Aug 22 2022 at 09:46):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Yes, I sometimes have a similar urge to remove warnings from my theories ;-)
The warning for duplicates is useful (with simp, intro, elim, etc), but we shouldn’t warn about a duplicate when it’s added under a different category (i.e. “intro!" instead of "intro").
It’s possible that this is motivated by implementation details somewhere, but I haven’t looked at it yet.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:47):From: Tobias Nipkow <nipkow@in.tum.de>
I am tempted to remove these altogether. I had done so alread with warnings
about overwriting split rules.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 09:47):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
I now realise what they were useful for originally: when you declare [cong] globally, to set up a library for instance, you want to be warned if a constant already has a cong rule. If you use them locally, you don’t want to know about it.
Probably the same for intro!/intro
Would probably mean passing another parameter into the implementation to distinguish the global from the local use (unless you can already tell by something else).
Gerwin
Email Gateway (Aug 22 2022 at 09:47):From: Lars Noschinski <noschinl@in.tum.de>
The problem is that the warnings are emitted at the wrong level: Deep
inside the implementation (in addsimps et al), instead at the top in the
user-facing operation. When the warning is emitted e.g. by a method
parser, we can also do more elaborate things (like emitting warnings per
lemma connection instead of per lemma).
There is also the thing that "cong del" lies about its (moral)
signature: it deletes not the specified congruence rule, but the
congruence rule for the given constant (which is determined from the
congruence rule).
Email Gateway (Aug 22 2022 at 09:47):From: Larry Paulson <lp15@cam.ac.uk>
This behaviour is inherited from the way things were 20 years ago, when what is now deeply buried was itself the user-facing operation.
Larry
Email Gateway (Aug 22 2022 at 09:48):From: Makarius <makarius@sketis.net>
Indeed, that was a rather different era, in the depths of time of Isabelle
history. It vaguely reminds me of the "real mode" of x86 CPUs:
http://en.wikipedia.org/wiki/Real_mode
Today it is a bit challenging to emit warnings (or other markup) in a way
that makes proper sense to the user. Context_Position.is_visible is
already well-established as a guard for most messages. Last year I also
introduced Context_Position.is_really_visible for Simplifier declarations,
to reduce spurious yellow in the PIDE markup. Such things are always
dangerous: there is more and more complication, and problems ultimately
don't get solved.
Right now, I have no particular opinion in which direction to move. If
certain warnings can be removed altogether, they cannot cause further
problems.
Makarius
Email Gateway (Aug 22 2022 at 09:48):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Overall, I think I’d be happy removing these specific warnings completely.
The cases where they are useful are rare compared to normal usage.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:48):From: Tobias Nipkow <nipkow@in.tum.de>
It is gone now.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 09:49):From: Makarius <makarius@sketis.net>
This is indeed a bit odd. I will take another look after the Isabelle2015
release to see how it can be renovated.
Makarius
Email Gateway (Aug 22 2022 at 10:13):From: Makarius <makarius@sketis.net>
That is an important observation: rules are both indexed and identified
by the head constant here.
Normally the index is just a data structure to help retrieval, while the
identity of rules works via Thm.eq_thm_prop. This would allow multiple
rules to be declared, and the latest addition for a particular constant is
used, the are others ignored. After deletion of some rules, ignored ones
might come back in front.
I've put this on the list of things to be reformed for a future release,
unless someone points out why this odd historical behaviour has to remain
like that.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC