Re: [isabelle] Jinja-Threads build problem



On Fri, 18 Oct 2013, Peter Lammich wrote:

Finally, I broke down the problem to a strange behaviour of
Proof-General:

Take the following minimal example:
 theory A
 imports Main
 begin
   ML_val {*
     tracing "Looping ...";
     fun f a = f a;
     f 1
     *}
 end

 theory B imports A
 begin

 end

Then use PG to load theory B. It will happily do so, ignoring that the
ML_val command is still running. Actually, the ML_val command is
started, and still running when PG displays the theory as processed.

ML_val is a diagnostic command and these get forked by default, just like proofs. Non-termination and errors need to be exposed by a proper join in the right place by the system, but this was actually broken for TTY / Proof General, which is in some sense legacy for quite some time already.

In Isabelle2013-1-RC4 I've addressed this issue, such that it works like the standard batch build or the document model of Isabelle/Scala/jEdit.

Remaining users of Proof General should take a very close look at Isabelle2013-1-RC4. There has been significantly less testing of the old TTY mode, due to constantly decreasing numbers of every day users. I use myself Proof General mainly for "ispell", and only until I've found some time to activate spell-checking in jEdit properly.


However, when loading the theory A with PG, it gets stuck at the ML_val
command as expected.

Here you are on the bare TTY loop, and that does not fork diagnostic commands.


This raises another question about the semantics of ML_val:
 Is a theory correct, where some ML-val command diverges?

Formally yes, since there is no connection of the diagnostic command to the thm values derived from the LCF kernel.

Practically no, since all the forks of a theory body should be properly joined. This is an important computational aspect outside of the logic.


The diverging ML_val command was introduced by my changes, that
accidently produced a code equation of the form "f a b = f a b"

In Isabelle/jEdit you see non-terminating commands as dark-violet areas in the Theories panel, or the individual buffer overview (right column next to text area).

What is still missing is some kind of "Status panel" to make a summary of the whole session, similar to what isabelle build does in batch mode to wrap up in the very end.


	Makarius




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