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:

changeset:   45486:600682331b79
user:        wenzelm
date:        Mon Nov 14 16:16:49 2011 +0100
files:       src/Pure/Isar/runtime.ML
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 trace.

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 MHonArc.