Stream: Mirror: Isabelle Users Mailing List

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


view this post on Zulip Email Gateway (Nov 14 2021 at 13:49):

From: Makarius <makarius@sketis.net>
On 14/11/2021 01:38, Peter Lammich wrote:

I'm getting an exception

exception Fail raised (line 673 of "variable.ML"): Bad context: clash
of fresh free for bound: :001 vs. xb

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.

Here is the announcement of the NEWS item on isabelle-dev some weeks ago:
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2021-October/017512.html

I had spent several days looking carefully at old (and some new) tools that
where violating the plain block structure that the Proof.context discipline
formalizes.

In the end it did work reasonably well: So an ancient warning could become a
proper error.

val thm = Goal.prove_internal ctxt [] (Thm.cterm_of ctxt
goal_t) (fn _ => tac)

Do you see a chance to work with proper Goal.prove, instead of the internal
side-entry Goal.prove_internal?

Makarius

view this post on Zulip Email Gateway (Nov 14 2021 at 13:52):

From: Makarius <makarius@sketis.net>
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


Last updated: Jul 15 2022 at 23:21 UTC