Re: [isabelle] Suppressing warnings



On Mon, Dec 6, 2010 at 5:27 PM, Tobias Nipkow <nipkow at in.tum.de> wrote:

> declare [[unify_trace_bound = 100]]
>
> or some value > 60. By default, unification starts tracing when the
> search depth reaches 50, and stops searching at 60. If you get many such
> warnings, it may be an indication that some proof method (eg auto) is
> not getting anywhere and is not appropriate.
>
>
Sure. But I think the display of the warning is determined by
unify_search_bound instead. According to unify.ML

    if tdepth > search_bnd then
        (warning "Unification bound exceeded"; (Seq.pull reseq))

I can't change the search bound to something large because I want to keep
the unification shallow, but suppress the warning messages.

Thanks
Steve

Tobias
>
> Steve W schrieb:
> > Hi,
> >
> > Does anyone know how to turn off warnings in Proof General? Warnings like
> > "Unification bound exceeded" sometimes flood my response window.
> >
> > Cheers,
> > Steve
>




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