Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle/jedit

view this post on Zulip Email Gateway (Aug 19 2022 at 07:49):

From: Tobias Nipkow <nipkow@in.tum.de>
When I start typing in a proof command, eg apply, jedit eagerly executes it, and
since I am in the middle of typing it, the command typically fails.
Unfortunately the resulting error msg overwrites the proof state. Is there any
way to see the old proof state while I type the proof command?

Thanks
Tobias

view this post on Zulip Email Gateway (Aug 19 2022 at 07:49):

From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users

I am also interested in a possible answer to this question. What I
usually do
in this case is to [repeatedly] move the cursor to the previous [next] line
(command, declaration) to take
a look at the current proof state before resuming
typing or thinking about the current command (declaration).

Cheers

view this post on Zulip Email Gateway (Aug 19 2022 at 07:50):

From: Fabian Immler <immler@in.tum.de>
You could disable "Auto update" in the Output panel and use "Update" manually.

Since "Update" is not exported as an action of the Isabelle-Plugin,
one cannot assign a keyboard shortcut to see the current proof state.

The attached macro (a short hack) emulates a click on "Update" and
could be used for an alternative way of interaction:

Installation instructions:

If this turns out to be a desired/competitive way of interaction, one
could think about having these actions exported by the
Isabelle-Plugin.

Now trying to prove theorems with manual updates of the proof state,
Fabian
update.bsh

view this post on Zulip Email Gateway (Aug 19 2022 at 07:50):

From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear all,

I was going to suggest an alternative to Fabian's setup where we could
use a keyboard shortcut to toggle "Auto update". My idea was that you
turn "Auto update" off in situations where you want to have a look at
the current proof state while typing the next method application (which
is not always the case since often subgoals are easy enough that we do
not really have to think about them) and afterwards turn "Auto update"
on again.

However, when trying this (currently by manually clicking on the "Auto
update" checkbox of the "Output" panel) I noticed what I would consider
undesirable behavior which I will illustrate by the following example
(where [...] indicates the cursor position):

lemma "A & B --> B & A"[]

At this point we have the subgoal

1. A ∧ B ⟶ B ∧ A

Now I turn off "Auto update" and type Enter to go to the next line.
Unfortunately, even with "Auto update" turned off, the "Output" panel is
"updated" to an empty state. The same happens when starting from

lamme "A & B --> B & A"
[]

and typing anything (already in the new line). Wouldn't it be preferable
if "Output" would not change at all, after switching off "Auto update"?

cheers

chris

view this post on Zulip Email Gateway (Aug 19 2022 at 07:51):

From: Tobias Nipkow <nipkow@in.tum.de>
Thank you, that was very helpful, I have installed your macro and will try it
out. Christian's idea of toggling Auto update sounds interesting, too, but I
would need a macro to try it.

This brings me to the next issue. Not updating the output panel does not keep
the prover from evaluating my partially edited proof text in the background. But
since I have edited the beginning of the text, the rest often does not make
sense anymore, or the parser parses it in an unintended way, at least up to the
next synchronisation point like "lemma". Frequently this leads to diverging
proof steps a bit further down, which are shown in purple. Together with the fan
coming on this is a bit distracting and I often feel compelled to comment out
bits of the proof in response. Is there any way to control the over-eager
evaluation to avoid such situations?

Thanks!
Tobias

view this post on Zulip Email Gateway (Aug 19 2022 at 07:51):

From: Fabian Immler <immler@in.tum.de>
2012/7/23 Tobias Nipkow <nipkow@in.tum.de>:

Thank you, that was very helpful, I have installed your macro and will try it
out. Christian's idea of toggling Auto update sounds interesting, too, but I
would need a macro to try it.
Try the attached macro!

Am 22/07/2012 19:42, schrieb Fabian Immler:

You could disable "Auto update" in the Output panel and use "Update" manually.

Since "Update" is not exported as an action of the Isabelle-Plugin,
one cannot assign a keyboard shortcut to see the current proof state.

The attached macro (a short hack) emulates a click on "Update" and
could be used for an alternative way of interaction:
- No "Auto update"
- Keyboard shortcut (e.g. Ctrl-Enter) to see the current proof state

Installation instructions:
- Move the attached update.bsh to
~/.isabelle/Isabelle2012/jedit/macros/ (This script "clicks" on
"Update")
- Assign a shortcut to this Macro:
- either via Utilities->Global Options->Shortcuts (The macro is
called "update")
- or by appending a line like "update.shortcut=A+ENTER A+m" to
~/.isabelle/Isabelle2012/jedit/properties

If this turns out to be a desired/competitive way of interaction, one
could think about having these actions exported by the
Isabelle-Plugin.

Now trying to prove theorems with manual updates of the proof state,
Fabian

2012/7/22 Alfio Martini <alfio.martini@acm.org>:

Dear Isabelle Users

I am also interested in a possible answer to this question. What I
usually do
in this case is to [repeatedly] move the cursor to the previous [next] line
(command, declaration) to take
a look at the current proof state before resuming
typing or thinking about the current command (declaration).

Cheers

On Sun, Jul 22, 2012 at 8:04 AM, Tobias Nipkow <nipkow@in.tum.de> wrote:

When I start typing in a proof command, eg apply, jedit eagerly executes
it, and
since I am in the middle of typing it, the command typically fails.
Unfortunately the resulting error msg overwrites the proof state. Is there
any
way to see the old proof state while I type the proof command?

Thanks
Tobias

--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
auto_update.bsh

view this post on Zulip Email Gateway (Aug 19 2022 at 07:52):

From: Alexander Krauss <krauss@in.tum.de>
It is nice to see how such usability issues can easily be addressed on
the user level...

An idea in a similar direction is to open multiple output panels, to
make it easier to stare at several states simultaneously. The underlying
model should easily support that. Then, each state view could have,
e.g., one of the following modes:

"Fixed" - Never move focus and always display the same state
"Under cursor" - Always show the state under the cursor
"Latest non-error" - Show the state of the latest command which was
processed successfully

Having both "Under cursor" and "Latest non-error" open should cover
Tobias' use case quite intuitively, without continuously requiring extra
"administrative" keystrokes.

Alex

view this post on Zulip Email Gateway (Aug 19 2022 at 07:53):

From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
Hi,

i have this very same problem. especially when "apply auto" follows, but
now applies to a different proof state, which it cannot resolve, it takes
very long, often too long to wait. the obvious workaround is to comment all
those lines, but this is very tedious.
right now i usually cut and paste the line
oops end (*
frequently when i edit larger theory files.

i would also be very happy to see a "parse till cursor"-mode or something
in jedit.
currently it is "parse the visible lines in the editor" (and lines that
were viewed since last edit), but maybe someday Makarius has enough time to
include an option to choose (just like the auto update button).
maybe auto parse [on/off], and when turned off, you can something like
double-click on a line to parse until there.

best regards
Nils

view this post on Zulip Email Gateway (Aug 19 2022 at 07:53):

From: Makarius <makarius@sketis.net>
More refined implicit processing of the editing and checking process is
indeed one of the many things that I still need to do, say with timeouts
for the part after the main editor focus towards the end of the buffer.
But note that the curser as such is somehow an artifact of the TTY with
its single-focus model. I would like to overcome that eventually, e.g. to
allow looking at several relevant sub-proof states at the same time, while
editing the head of an induction proof, say.

In any case it helps to collect observations from users, like on this
thread.

One more hint what can be done right now (in Isabelle2012): the main
control of the implicit checking is the "perspective" of the editor, i.e.
the set of text intervals that are visible to the user. Standard jEdit
Folding and Narrowing can be used to confine proof checking to a smaller
text region, e.g. via the menu action "Folding / Narrow to Selection".

Makarius

Last updated: Apr 25 2024 at 16:19 UTC