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 change.

Thanks to everyone for listening to me talk to myself about simplifier mysteries.

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: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-February/msg00056.html

The changeset mentioned there is:

changeset:   55375:d79c057c68f0
user:        wenzelm
date:        Mon Feb 10 13:04:08 2014 +0100
files:       src/Pure/raw_simplifier.ML
description:
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]]
    apply simp
    oops


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.


	Makarius




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