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
> warnings.
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
> demand.
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!

  -- Lars

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