Re: [isabelle] Isabelle2021-1-RC3: HELP! Bad context exception



On 14/11/2021 13:07, Peter Lammich wrote:
> I'm still trying to figure out a way how to systematically catch them
> all, and how to fix it in some cases without potentially introducing
> performance regressions.
> 
> Pattern:
> 
> fun some_conv ctxt = let
>   val inner_conv = Simplifier.rewrite (ctxt addsimps ...)
> in
>   Conv.params_conv ~1 (K [...] inner_conv) ctxt
> end
> 
> I probably thought it was a good idea, b/c it keeps the (maybe
> expensive?) operations on the context, like adding a lot of simp-
> lemmas, out of the conversion (in particular, if [...] applies the
> conversion multiple times).

You can use get_simpset / put_simpset to produce an augmented simpset before
going into the context. Here is an example where I did have a performance leak
beforehand:
https://isabelle-dev.sketis.net/rISABELLE71bafd70acb


	Makarius




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