Re: [isabelle] 2014-RC1 issues

> 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.

I mean that there are many warnings in my theories, usually from the
simplifier/classical reasoner that inform me that I have added rules
that were already present in the simpset/claset (including the spurious
warning when using intro! for an [intro] - rule). 

Thus, in my case, it is difficult to write theories without warnings, or
to manually check every single warning whether it is bad (garbage in the
theory) or not (just some spurious simplifier warning). 

The surprise will probably come in batch-build mode, as this will be the
time when the garbage will make problems. 

I'm already looking forward to the tutorials of the semantics-lecture,
where students will definitely hand in lots of unfinished lemmas, many
of them convinced they actually have proven it ...
In PG, or even in older isabelle/jedits, I could just give them the rule
of thumb: Your theory must not contain errors, sorrys, or oops. 

Also, I will have hard times checking the submissions, as I have to
manually check every warning to see wether the proof is actually
closed ...

> > * In the output buffer, the standard Ctrl-Ins for "copy" does not work,
> > while it works in the main text area. Can these shortcuts be configured
> > separately? Or do I have to live with Ctrl-C?
> I did not know about Ctrl-Ins yet.  What you observe here is merely the 
> known and documented difference of the main jEdit text area with its 
> actions and shortscuts vs. regular Java Swing GUI components.  The latter 
> only have basic Ctrl-C, and it actually works routinely, which is a big 
> step forwards to the historic perspective.
> If Ctrl-C does *not* work somewhere, it is actually an issue that needs to 
> be addressed.

Looks like I have to lower my expectations to modern user interfaces.
One of these expectations is full configurability, not forcing the user
to some fixed shortcuts that, depending on typing habits, may or may not
be convenient. Btw: the "old-fashioned" "ancient" emacs is fully
configurably in the above sense!

> > * Odd behaviour when focus lays in output buffer or any other panel:

> This belongs to normal jEdit policies.  In Isabelle/jEdit for the coming 
> release I added the faint cursor to emphasize that -- normally it would be 
> just absent.

Ok, maybe its a jEdit feature. Personally, I find it very odd and I have
hard times getting used to it: Whenever I used a query/sledgehammer
panel, I regularly forget to click into the text-area before typing ...

> >
> >  In PG, there was a nice auto-indentation feature that worked reliable 
> > for (almost) all cases.
> That is indeed a notable omission.  In 1998, I added indentation to PG 2.x 
> quite early, and earned the name "The indentation Man" in the inner circle 
> of PG developers.  

It was a very useful feature, and I'm really missing it. As code-folding
also does not work, there is currently no feature that assists in
keeping track of the structure of big developments.

> > * When developing proofs:
> >  The output window displays the current position
> >  by default ... if you are typing a new command, it usually displays
> >  "Syntax error".
> >  However, while typing your next method/isar step, you usually want to
> >  see the current goal state, not a the completely useless information
> >  "syntax error".
> >
> >  In PG, the output was not updated before you explicitely processed
> >  the command. Maybe, this can be simulated by turning auto-update off
> >  and bind update to a convenient shortcut.
> 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.

Let's hope I can bind these thing to some shortcuts ...


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