Re: [isabelle] Changing unification depth



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
>





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