[isabelle-dev] error in cook book ?

[Makarius]

On Wed, 8 Sep 2010, Nils Jähnig wrote:

> yes, i found this trace buffer, but it is not really convenient to work 
> with, as it does not auto clear (i found now C-x C-w and try to use it) 
> and informations there (especially in the cook book) are meant to be 
> together with the other output. and i have an Isabelle-buffer, where all 
> information is displayed (i think this one is read by PGEclipse).

I think Christian even had a strong inclination towards tracing output in 
some versions of the Cookbook, because it produced a certain wanted 
behaviour on a certain version of Proof General / Emacs.


> but using "by simp" displays the informations written with pwriteln 
> (Pretty.writeln) in the response buffer together. is this something "by" 
> does?

The regular way to output things is via writeln.  In some situations, 
end-of-proof (e.g. via 'by') prints a result using writeln as well.  In an 
open proof state, some extra workarounds are required, because most Proof 
General configurations tend to put the state output in front.  You should 
be able to switch back to *response* nonetheless, or use "3 window mode" 
or something.

If you look at print_tac in the sources, it uses tracing explicitly, 
hoping to escape these traps.  There are other variations on the theme, 
like using warning, or even the special Output.priority protocol message. 
The latter is generally a bit dangerous, because it suppresses error 
output in certain situations, causing great confusion.

All of this is very fragile, and will only become better with the next 
generation of user interfaces.  As a general rule of thumb, one should 
keep the ML part as plain and simple as possible, and use writeln most of 
the time.


> The PGEclipse is kind of working, but not enough, to work with it. it 
> has problems with "undo previous proof command", especially if you have 
> ML-code in the same file. So at the moment all it does is looking much 
> more user friendly than emacs, and displaying the output as i want it, 
> but i have to restart often, so it is not yet an option.

I did not know that it can actually be run -- when I tried some years ago 
I failed miserably.  In my frustation I asked the Google oracle what to do 
about "Eclipse sucks", and it pointed me to a blog spot saying "Do not use 
Eclipse, but jEdit."  Some years later, I have an almost working version 
of Isabelle/jEdit.  The one distributed with Isabelle2009-2 is merely a 
sneak preview -- if you look closely you can imagine its full potential.

Even that partial version is already quite good to get acuainted with 
Isabelle/ML programming, though.  Some months ago we sucessfully ran a 2 
day workshop on Isabelle tool development using this mini-IDE with great 
success.  E.g. hovering over ML embedded in the theory source will give 
you tooltips about inferred types, or CTRL-hover-click gives you 
hyperlinks to navigate the the sources.  The "Output" window also shows
results from the prover without too much smartness getting in between.

See Isabelle2009-2/src/Tools/jEdit/README for further details.  Assuming 
you have an original (!) JVM 1.6 from Sun/Oracle, you merely need to say 
"isabelle jedit" to get you out of the old PG/Emacs world order. (It is 
not usable for serious proof development right now.)


 	Makarius