Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Suppressing warnings

Email Gateway (Aug 18 2022 at 16:37):

From: Steve W <s.wong.731@gmail.com>
Hi,

Does anyone know how to turn off warnings in Proof General? Warnings like
"Unification bound exceeded" sometimes flood my response window.

Cheers,
Steve

Email Gateway (Aug 18 2022 at 16:37):

From: Tobias Nipkow <nipkow@in.tum.de>
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.

Tobias

Steve W schrieb:

Email Gateway (Aug 18 2022 at 16:37):

From: Steve W <s.wong.731@gmail.com>
On Mon, Dec 6, 2010 at 5:27 PM, Tobias Nipkow <nipkow@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

Last updated: Apr 26 2024 at 12:28 UTC