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



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.