Re: [isabelle] 2014-RC1 issues



On 30.07.2014 22:14, Makarius wrote:
> The invocation of error "" is the same as raise ERROR "", which makes
> the ML code fail and the Isar toplevel wrapper print the exeptions. 
> The error message is empty, which means it is vacous according to
> ancient Isabelle traditions, which hold until today.  The effect was
> not visible in the old TTY times, because that adds a prefix of "*** "
> by default. Note that there are other situations where ML failure
> might lead to no error output, notably involving Exn.Interrupt.
>
> Such non-printing exceptions should not show up under normal
> circumstances -- they indicate a programming mistake somewhere.
The following is probably not relevant to the 2014 release anymore, but
for the sake of completeness:

I encountered such a case yesterday (with 2014-RC2) with a tactic with
resulted in a non-productive result sequence, i.e. the equivalent of

ML <
  fun inf_seq () = Seq.cons 0 (inf_seq ())
  val nonprod_seq = Seq.filter (K false) (inf_seq ())
>

After some looking around, I found that I get a little hint in the Raw
Output panel -- if the panel is open while the failing code is executed.
I wonder whether the raw output panel could accumulate, say, the last 8k
worth of messages even if it is closed? Also, a "clear" button would be
nice (although closing/reopening works).

Interestingly, asking for an exception trace (via
[[ML_exception_trace]]) for this code sends polyml into a another
desperate quest for memory: It has been running on my machine a few
minutes with 4086M VIRT and 3956M RES -- so basically exhausting its
full address space -- before giving up:

    Welcome to Isabelle/HOL (Isabelle2014-RC2: August 2014)
    Warning - Unable to increase stack - interrupting thread

    Warning - Unable to increase stack - interrupting thread

    Warning - Unable to increase stack - interrupting thread

    Warning - Unable to increase stack - interrupting thread

    Run out of store - interrupting threads

    Run out of store - interrupting threads

    Failed to recover - exiting

    message_output terminated
    standard_output terminated
    standard_error terminated
    process terminated
    command_input terminated
    process_manager terminated
    Return code: 1


In these cases I could be useful to get at least at a partial trace
(which would probably already indicate which functions
went into a loop).



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