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.
> fun some_conv ctxt = let
> val inner_conv = Simplifier.rewrite (ctxt addsimps ...)
> Conv.params_conv ~1 (K [...] inner_conv) ctxt
> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and