Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)
On Fri, 14 Sep 2012, David Greenaway wrote:
On 14/09/12 08:58, Rafal Kolanski wrote:
I really wish that there was some way to get exception traces again when
working interactively in Isabelle.
I too had previously thought that the exception traces in Isabelle had
disappeared somewhere around the Isabelle2011-1 time-frame,
Both of you seem to have taken software decay for granted, and did not
tell anybody here or on isabelle-dev. Isabelle has traditionally very
high ethical standards for software quality, so things are usually put
into shape again quickly, once the problem is known.
I have come across the issue myself last fall just after the
Isabelle2011-1 release, so in Isabelle2012 it works again. See the
typical changelog prose of mine that explains everything in one line,
quoting even the relevant Poly/ML change:
date: Mon Nov 14 16:16:49 2011 +0100
more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);
(Interestingly, there are actually two traces printed: the first is
the one listed above, the second seems less useful.)
That is the "more detailed" aspect above. By filtering out some less
relevant exceptions, the full trace was lost by accident. So it is now
redundant, but informative again.
So I am not sure if/when the stack traces disappeared, or if/when they
came back, but happily they seem to be working now. The key points are
to enable "Toplevel.debug", disable inlining for the code you are trying
to debug, and make sure you look in "*isabelle*" trace window for the
In Isabelle/jEdit this is the raw output panel, to show physical stdout
messages that are produced by the Poly/ML runtime system for the exception
trace. This is unmanaged output, and the window needs to be active when
it happens, otherwise it is lost.
On a marginally related note, PolyML also has stepping/tracing
facilities, as described in:
which you can theoretically use by typing commands in the "*isabelle*"
window. I have personally found that the combination of Isabelle and
ProofGeneral and PolyML debugging tends to be a little unstable, so
I don't ever use these. I would be curious to know if others have had
more success, however.
In Isabelle/jEdit the support for Isabelle/ML support (including tracing
and debugging) is already better in Isabelle/jEdit of Isabelle2012 than
ever before in the history of Isabelle Proof General.
There is also clear separation of physical stdin from the protocol
channel. So in principle one could negotiate with the raw Poly/ML
toplevel loop (and its debugger) while Isabelle is running at full speed.
There is no console window for that in the Prover IDE, though.
In practice, I usually use plain writeln and PolyML.print to see what is
happening in some ML code (after recompiling), not the debugger.
This archive was generated by a fusion of
Pipermail (Mailman edition) and