[isabelle-dev] error in cook book ?

[Nils Jähnig]

jEdit looks very good! i will i try it the next days, but from what
what i experienced during five minutes, i think i will keep it.
thanks for your answer
/Nils


2010/9/8 Makarius <makarius at sketis.net>:
> 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
>