Re: [isabelle] Simplifier divergence in Isabelle 2014 release candidates.
On Tue, 12 Aug 2014, Thomas Sewell wrote:
In hindsight this all makes sense, and is entirely my problem. I hope
noone else has to deal with anything this awful as a result of this
Thanks to everyone for listening to me talk to myself about simplifier
This thread seems to be resolved for now. I just want to make sure that
there is nothing left to reconsider for the Isabelle2014 release, which
will be shipped next week.
Some months ago there was a similar surprise about simplifier depth limit
concerning simprocs. See the subject line "Product_Type.split_beta fails"
in October 2013 with the conclusion here:
The changeset mentioned there is:
date: Mon Feb 10 13:04:08 2014 +0100
more elementary put_simpset: exchange the simplifier configuration
outright, which is particularly relevant concerning cumulative depth, e.g.
for Product_Type.split_beta in the subsequent example:
lemma "P (\<lambda>s. (case s of (x, y) \<Rightarrow> c))"
using [[simp_depth_limit = 1]]
It falls in the interval between the last release Isabelle2013-2 and the
emerging one Isabelle2014. Thus it might be relevant concerning potential
regressions of Simplifier behaviour due to a change that was meant to
improve the situation.
This archive was generated by a fusion of
Pipermail (Mailman edition) and