Re: [isabelle] Jinja-Threads build problem
- To: Peter Lammich <lammich at in.tum.de>
- Subject: Re: [isabelle] Jinja-Threads build problem
- From: Makarius <makarius at sketis.net>
- Date: Thu, 7 Nov 2013 21:18:57 +0100 (CET)
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <1382085196.12729.7.camel@lapbroy33>
- References: <1382009159.4722.73.camel@lapbroy33> <1382085196.12729.7.camel@lapbroy33>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Fri, 18 Oct 2013, Peter Lammich wrote:
Finally, I broke down the problem to a strange behaviour of
Take the following minimal example:
tracing "Looping ...";
fun f a = f a;
theory B imports A
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and