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



Hi,

after a few hours of guessing and trying to figure out what happens, I
have tracked down the issue to the following dangerous pattern that
violates context discipline, but which, unfortunately, I used a lot.
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).

The obvious 'fix' would be to modify the simpset before invoking the
conversion, which, however, easily leads to modularity problems, as in:

fun complicated_inner_conv_reused_from_multiple_places ctxt = let
  val ctxt = ctxt addsimps ...
  [...]
in
  Simplifier.rewrite ctxt
end

I cannot come up with a robust solution here, in particular if more
than one inner_conv is involved. 

--
  Peter




On Sun, 2021-11-14 at 01:38 +0100, Peter Lammich wrote:
> Hello,
> 
> I'm getting an exception
> 
> exception Fail raised (line 673 of "variable.ML"): Bad context: clash
> of fresh free for bound: :001 vs. xb
> 
> from "Sepref_Frame.prepare_fi_conv"
> in afp/thys/Refine_Imperative_HOL/Sepref_Frame.thy
> 
> I assume that this is due to not sticking to some ominous 'context
> discipline'. I tried an analogous fix to what has been done in 
> Refine_Util.f_tac_conv in
> thys/Automatic_Refinement/Lib/Refine_Util.thy, i.e.,
> Variable.declare_term just before Goal.prove_internal, and using the
> resulting goal_context in the proof tactic, however, the exception
> persists.
> 
> I'm lost! Can someone please explain what might go wrong here, and
> how
> to debug and track down such errors, or point me to (ideally concise
> and understandable) documentation about what 'context discipline'
> exactly means.
> 
> --
>   Peter
> 
> ps
>   given the fact that this regression seems to not occur in the AFP
> (such that the affected code has not been changed), I'm deeply
> worried
> about this stricter context discipline enforcement, as such errors
> may
> slip through, silently degrading add-on tools for which not enough
> use-
> cases are in the AFP. At least, it needs some concise documentation
> (WITH A POINTER TO WHERE IT IS IN THE NEWS FILE), such that poor
> users
> like me at least get an understanding of what they are doing, rather
> than blindly trying to copy code, and having to give up if that does
> not work.
> 
> pps
> 
> Fix I tried:
> 	...
> 
>         val new_t = mk_entails (P', Q')
>         val goal_t = Logic.mk_equals (t,new_t)
> 
>         val goal_ctxt = Variable.declare_term goal_t ctxt
>   
>         val msg_tac = dbg_msg_tac (Sepref_Debugging.msg_allgoals
> "Solving frame permutation") goal_ctxt 1
>         val tac = msg_tac THEN ALLGOALS (resolve_tac goal_ctxt @{thms
> reorder_enttI}) THEN star_permute_tac goal_ctxt
>         
>         val thm = Goal.prove_internal ctxt [] (Thm.cterm_of ctxt
> goal_t) (fn _ => tac)
> 
> 
> 
> On Fri, 2021-11-12 at 21:26 +0100, Makarius wrote:
> > Dear Isabelle users,
> > 
> > please see https://isabelle.sketis.net/website-Isabelle2021-1-RC3
> > and
> > https://isabelle-dev.sketis.net/phame/post/view/53/release_candidates_for_isabelle2021-1
> > for further progress on the release process.
> > 
> > There is now a proper download for Linux (ARM), and the "isabelle
> > build_docker" tools works for it (relevant on Apple M1 hardware).
> > 
> > This is also the fork-point of the isabelle-dev repository, which
> > continues
> > for the time after this release:
> > https://isabelle.sketis.net/repos/isabelle/rev/4f1c1c7eb95f
> > 
> > 
> > Reminder: Any feedback about release candidates should be posted
> > with
> > a meaningful
> > Subject (not just a clone of the announcement).
> > 
> > We have approx. 4 weeks left until final lift-off: afterwards there
> > will be no
> > more changes on this line.
> > 
> > 
> > 	Makarius
> > 
> 
> 





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