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