Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] the Query panel


view this post on Zulip Email Gateway (Aug 19 2022 at 16:59):

From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,

I tried to find the theorem whose name is left_neutral so opened the Query dialog and wrote

name: "left_neutral"

Now the star-shaped widget beside the Apply button runs infinitely showing that the system works.

Is the above query wrong? And, how could I stop this thread and start a new query?

view this post on Zulip Email Gateway (Aug 19 2022 at 16:59):

From: Makarius <makarius@sketis.net>
On Tue, 20 Jan 2015, Buday Gergely wrote:

I tried to find the theorem whose name is left_neutral so opened the
Query dialog and wrote

name: "left_neutral"

Now the star-shaped widget beside the Apply button runs infinitely
showing that the system works.

This "spinning disk" icon can actually have various different states.
The tooltip tells more, e.g. it could be "Waiting for evaluation of
context ...". Sometimes there is just a user confusion about that.

Nonetheless, there could be a genuine problem, e.g. a deadlock. If such a
problem is recurrent, it usually helps to look very closely what really
happens, and tell me about it. People have also made informative
screencasts, leading to successful improvements of the situation
eventually.

Is the above query wrong?

The query is OK. If it were somehow malformed, there should be an
explicit error.

And, how could I stop this thread and start a new query?

It is unrealistic to manage threads manually -- the system mainly works
with future tasks anyway. The Monitor panel might provide some clues what
the system is up to, but it is also hard to interpret the situation.

Makarius


Last updated: Apr 18 2024 at 20:16 UTC