Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)




Hi Raf,

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, but when
I tried to reproduce the problem this morning in Isabelle2012 I was
pleasantly surprised to find that the problem had gone away and I could
actually get them again.

In particular, with the following code:

    ML {*
        exception FOO;
        fun x1 (a : int) = raise FOO;
        fun x2 (a : int) = x1 a * x1 a;
        fun x3 (a : int) = x2 a * x2 a;
        (* ... *)
        fun x14 (a : int) = x13 a * x13 a;
        fun x15 (a : int) = x14 a * x14 a;
    *}
    ML {* x15 0 *}

in Isabelle2012 using ProofGeneral 4.0 with "Toplevel.debug" set to
true, I get in the "*isabelle*" response window a partial stack trace:

    x9(1)
    x13(1)
    <top level>
    CODETREE().genCode(2)(1)
    COMPILER_BODY().baseCompiler(4)executeCode(1)

(Interestingly, there are actually two traces printed: the first is
the one listed above, the second seems less useful.)

If I set "PolyML.Compiler.maxInlineSize" to 0 and recompile the above
code, I get a more complete exception trace, with every function (other
than "x1", where the exception is raised) listed:

    x2(1)
    x3(1)
    x4(1)
    [...]
    x14(1)
    x15(1)
    <top level>
    CODETREE().genCode(2)(1)
    COMPILER_BODY().baseCompiler(4)executeCode(1)

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.

On a marginally related note, PolyML also has stepping/tracing
facilities, as described in:

    http://www.polyml.org/docs/Debugging.html

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.

Cheers,
David

--




The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.





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