Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP



Hi Fabian, Makarius,

Fabian wrote:

> 1.) When I start Isabelle loading the following theory,
> 
> theory Scratch
> imports Main
> begin
> 
> notepad
> begin
>  fix P and x::'a
>  {
>    fix x::'a
>    have "P x ⟹ P x"
>      by simp
>  } hence True
>    sledgehammer
> 
> sledgehammer finds a proof and appears to have terminated, but the poly-Process keeps running with 100% CPU until I get the following error message (via Isabelle Syslog) indicating a segfault:

I can reproduce the problem with the following (array-free!) theory:

    theory Scratch
    imports Main
    begin

    ML {*
    fun launch_thread timeout task =
      let
        val birth_time = Time.now ()
        val death_time = Time.+ (birth_time, timeout)
        val desc = ("", "")
      in
        Async_Manager.thread "" birth_time death_time desc task
      end
    *}

    ML {*
    launch_thread (seconds 10.0) (fn _ => error "FOO")
    *}

    end

In short: Any uncaught exception raised from an old-style "Async_Manager" worker thread eventually leads to a segfault.

> 2.) When I load the following theory (again with a clean ISABELLE_HOME_USER)
> 
> theory Scratch
> imports Main
> begin
> 
> lemma True
> sledgehammer learn_isar
> ..
> (* sufficiently many blank lines to have the sledgehammer invocation below outside of the visible part of the text area *)
> notepad
> begin
>  fix P and x::'a
>  {
>    fix x::'a
>    have "P x ⟹ P x"
>      by simp
>  } hence True
>    sledgehammer
> 
> while making sure that "sledgehammer" is not started before "sledgehammer learn_isar" ends, sledgehammer fails with
> 
> exception DUP "`⋀

I have yet to investigate this closer, but the exception that was thrown in (1) was "DUP", so the bug appears to be a... duplicate. ;)

Thanks again for taking the time to produce such a useful bug report!

Jasmin





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