Re: [isabelle] 2014-RC1 issues
On 30.07.2014 21:53, Makarius wrote:
> What do you mean by "warnings are omnipresent in Isabelle"? The
> prover IDE shows them more prominently than in the TTY past, but that
> could be taken as motivation to remove the reasons for warnings. Not
> all such spots are bad, but an avarage theory normally has only few
Often, the "Ignoring duplicate rewrite rule/intro/..." warnings get
annoying, as they are not always meaningful (for example, overwriting
intro by intro! triggers a warning). In particular, in certain
locale-heavy theories (HOL-Algebra comes to mind), interpreting (or
opening) a locale gives you a number of these warning and there is not
always a (nice) way around them (I'd even claim that these warnings are
mostly vacuous for theory interpretations, but this is another topic).
I had some theories where these warnings were common enough to obscure
the real ones.
> Nothing new about this observation. It belongs to general mismatch of
> TTY/PG mechanics wrt. the document-oriented model. Note that you can
> also use the Query panel to print proof states on demand and only on
On the topic of the query panel: Some time in the future, I'd like to
see the equivalent of the jEdit action bar (or, to phrase it
differently, a "general" query panel) for Isabelle, where I enter an
arbitrary (diagnostic) command and get the output in the panel.
BTW: I just discovered that symbol completion works now in the
text-boxes in the panels, very nice!
This archive was generated by a fusion of
Pipermail (Mailman edition) and