Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Jinja-Threads build problem

Email Gateway (Aug 19 2022 at 12:08):

From: Peter Lammich <lammich@in.tum.de>
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.

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

What has happened here? Is this a problem of PG, or of some
Isabelle-stuff used elsewhere (As PG does not do loading of required
theories itself, I suspect the problem lies somewhere in Isabelle)

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

Email Gateway (Aug 19 2022 at 12:48):

From: Makarius <makarius@sketis.net>
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

Last updated: Apr 25 2024 at 16:19 UTC