Re: [isabelle] Changing unification depth



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;



Just a follow-up question: If unify_search_bound is updated, I should expect to see ref to be updated there, right?

Thanks
John


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. Eg 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

>






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