*To*: Fabian Immler <immler at in.tum.de>, Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP*From*: Jasmin Christian Blanchette <jasmin.blanchette at gmail.com>*Date*: Thu, 24 Jul 2014 16:22:12 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Cezary Kaliszyk <cezary.kaliszyk at uibk.ac.at>*In-reply-to*: <FB87B696-CFF3-4CF8-A556-BC0BEDDB8E1E@in.tum.de>*References*: <FB87B696-CFF3-4CF8-A556-BC0BEDDB8E1E@in.tum.de>

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

**Follow-Ups**:

**References**:**[isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP***From:*Fabian Immler

- Previous by Date: Re: [isabelle] returning to the original document in Isabelle/jedit
- Next by Date: Re: [isabelle] returning to the original document in Isabelle/jedit
- Previous by Thread: Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
- Next by Thread: Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
- Cl-isabelle-users July 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list