Re: [isabelle] Isabelle2014-RC0 available for testing



I found some problems.

The following can be solved by isabelle 2013-2 but not by Isabelle 2014-RC0:
lemma "finite X ⟹ finite {(x1, x2) ∈ X. P x1 x2}" by simp
In Isabelle 2014-RC0, also try0 and sledgehammer fail.
I suppose it is because of the tuple notation?

When a proof fails, the output buffer displays: "...  method⌂: ...".
Notice the triangle-like symbol. The same strange symbol is displayed
for an ML error.

Finally, when I try to sledgehammer something in one of my thys, the
prover crashes.
"Welcome to Isabelle/HOL (Isabelle2014-RC0: July 2014)
Malformed message:
bad chunk (unexpected EOF after 0 of 7314 bytes)
message_output terminated
/home/diekmann/Downloads/Isabelle2014-RC0/lib/scripts/run-polyml-5.5.2:
line 84: 15324 Segmentation fault      (core dumped) "$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"
I will try to reproduce this in a minimal example

Cheers
  Cornelius




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