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



Just for the record: I have also seen the second issue that Fabian describes several times but did not investigate yet, how to reproduce it reliably.

cheers

chris

On 07/15/2014 07:14 PM, Fabian Immler wrote:
Hi Isabelle,

I noticed two problems, it could be that they are related but i don't know. Note that (especially the first one) might be related to the ML process crashing in thread [1].

Here is how i can reproduce them -- it seems to be important to have a clean ISABELLE_HOME_USER.
I could reproduce them on my Mac (OS X 10.8.5) and on a Linux machine. The errors also occur with "current" isabelle bc957769b584.

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:

Welcome to Isabelle/HOL (Isabelle2014-RC0: July 2014)
message_output terminated
/Users/immler/Desktop/Isabelle2014-RC0.app/Contents/Resources/Isabelle2014-RC0/lib/scripts/run-polyml-5.5.2: line 84: 85096 Segmentation fault: 11  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" --error-exit < /dev/null

standard_error terminated
standard_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 139

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 "`⋀\^E\^Fxml_elem\^Fxml_name=typing\^E\^E\^Fxml_body\^E\^E\^Fxml_elem\^Fxml_name=sorting\^E\^E\^Fxml_body\^Etype\^E\^F\^E'a\^E\^F ...... l_elem\^Fxml_name=typing\^E\^E\^Fxml_body\^E\^E\^Fxml_elem\^Fxml_name=sorting\^E\^E\^Fxml_body\^Etype\^E\^F\^E'a\^E\^F\^E\^E\^F\^Exa\^E\^F\^E`" raised (line 261 of "General/table.ML")

Best regards,
Fabian

[1] http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/9091





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