*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Changing unification depth*From*: John Munroe <munddr at gmail.com>*Date*: Fri, 26 Nov 2010 13:14:50 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <alpine.LNX.1.10.1011261354400.29140@atbroy100.informatik.tu-muenchen.de>*References*: <AANLkTi=fs2GJ_8VmufFukj24jvz-XPWEx9BSb=NrZuGn@mail.gmail.com> <alpine.LNX.1.10.1011261354400.29140@atbroy100.informatik.tu-muenchen.de>

Sorry, my mistake. Indeed I tried unify_search_bound = 5. I see that the configuration itself has changed, but the function hounifiers doesn't seem to see the update: If I do: declare [[unify_search_bound = 70]] ML {* Config.get_global @{theory} Unify.search_bound *} ML {* Config.get @{context} Unify.search_bound *} I do see 70 for both. But if I do ML {*!Unify.ref*} even after having run hounifiers, via, e.g., Unify.matchers, I see 60. Here's how ref is assigned: fun hounifiers (thy,env, tus : (term*term)list) : (Envir.env * (term*term)list)Seq.seq = let ... in (ref := search_bnd; add_unify 1 ((env, dps), Seq.empty)) end; So It seems hounifiers can't see the update. If I change it to something more extreme, like 5, the unifier itself doesn't behave as if it was 5 but as if it was 60. Thanks John On Fri, Nov 26, 2010 at 1:00 PM, Makarius <makarius at sketis.net> wrote: > On Fri, 26 Nov 2010, John Munroe wrote: > >> theory Test >> imports Complex_Main >> begin >> >> declare [[unification_search_bound = 70]] >> ... > >> It seems that Unify.search_bound is fixed to the value of >> Unify.search_bound_value, which is default to 60 due to > > Did you really try it as above? The configuration option is called > "unify_search_bound". Here is an example in Isabelle2009-2: > > declare [[unify_search_bound = 70]] > > ML {* Config.get_global @{theory} Unify.search_bound *} > ML {* Config.get @{context} Unify.search_bound *} > > For historical reasons there is a snag: unify options can only be modified > in a global context. E.g. consider: > > lemma A > using [[unify_search_bound = 42]] > > ### Ignoring local change of global option "unify_search_bound" > > As usual in Proof General, such warnings are easily overlooked. As usual, > it will be much more visible in the Isabelle/jEdit prover IDE, although I've > already had some complaints that warnings are too prominent there. > > > Makarius >

**Follow-Ups**:**Re: [isabelle] Changing unification depth***From:*munddr

**References**:**[isabelle] Changing unification depth***From:*John Munroe

**Re: [isabelle] Changing unification depth***From:*Makarius

- Previous by Date: Re: [isabelle] A beginner's questionu
- Next by Date: [isabelle] using Isabelle2005 on polyml5.0
- Previous by Thread: Re: [isabelle] Changing unification depth
- Next by Thread: Re: [isabelle] Changing unification depth
- Cl-isabelle-users November 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list