Email Gateway (Aug 19 2022 at 15:46): Email Gateway (Aug 19 2022 at 15:46):From: bnord <bnord01@gmail.com>
When typing fast and using tab completion in Isabelle204-RC2 I often end
up with e.g. "sle<tab>" instead of "sledgehammer" when the system is
under some load. In 2013-2 no matter how hard I try I always get the
completion. I believe that I have changed all relevant settings to
intermediate/0.
Best
Benedikt
Email Gateway (Aug 19 2022 at 15:48):From: Makarius <makarius@sketis.net>
You probably mean "immediate". I think you also need to switch off the
option "Completion Context" -- thus you are back to old-style syntactic
completion, independently of prover markup (which might get delayed and
thus cause non-determinism).
Instead of such a nostalgic mode that imitates old versions of
Isabelle/jEdit, I recommend to study the Isabelle/jEdit manual section
"3.5 Completion" and practice a little with the new defaults, which were
made for mixed syntactic / semantic completion.
To improve determinism on very light machines under load it might also
help to switch off the main "Completion" option and use the explicit key
sequence C+b instead.
For sledgehammer in particular, the canonical way is to use the
Sledgehammer panel instead of inserting a command.
Makarius
Email Gateway (Aug 19 2022 at 15:48):From: bnord <bnord01@gmail.com>
Am 08.08.14 12:22, schrieb Makarius:
On Wed, 6 Aug 2014, bnord wrote:
When typing fast and using tab completion in Isabelle204-RC2 I often
end up with e.g. "sle<tab>" instead of "sledgehammer" when the system
is under some load. In 2013-2 no matter how hard I try I always get
the completion. I believe that I have changed all relevant settings
to intermediate/0.
You probably mean "immediate". I think you also need to switch off
the option "Completion Context" -- thus you are back to old-style
syntactic completion, independently of prover markup (which might get
delayed and thus cause non-determinism).
Thanks that helped.
Instead of such a nostalgic mode that imitates old versions of
Isabelle/jEdit, I recommend to study the Isabelle/jEdit manual section
"3.5 Completion" and practice a little with the new defaults, which
were made for mixed syntactic / semantic completion.To improve determinism on very light machines under load it might also
help to switch off the main "Completion" option and use the explicit
key sequence C+b instead.
Sounds nice. But I'd like to have the "old" context insensitive
completions (at least the first one) at the default and the possibility
to always select it immediately. Maybe the completion list should be
updated with additional completions that take more time.
For sledgehammer in particular, the canonical way is to use the
Sledgehammer panel instead of inserting a command.
Have you tried setting up the sledgehammer panel on a regular 1080p
display? There's just not enough vertical space to have the editor, the
output and the Sledgehammer panel for my taste. Switching views or using
the mouse is not an option for me. Also I'd like some marker in the text
showing me "here is some sledgehammer instance running click me to get
to the results".
Best
Benedikt
Email Gateway (Aug 19 2022 at 15:48):From: Makarius <makarius@sketis.net>
Mobile devices have strange screen formats, but the dockable window
manager allows to dock left or right, too.
The "Locate" button of the panel indicates where the presently active
instance is located.
Makarius
Email Gateway (Aug 19 2022 at 15:48):From: bnord <bnord01@gmail.com>
Am 08.08.14 12:51, schrieb Makarius:
On Fri, 8 Aug 2014, bnord wrote:
For sledgehammer in particular, the canonical way is to use the
Sledgehammer panel instead of inserting a command.
Have you tried setting up the sledgehammer panel on a regular 1080p
display? There's just not enough vertical space to have the editor,
the output and the Sledgehammer panel for my taste. Switching views
or using the mouse is not an option for me. Also I'd like some marker
in the text showing me "here is some sledgehammer instance running
click me to get to the results".Mobile devices have strange screen formats, but the dockable window
manager allows to dock left or right, too.
Mobile devices? No regular displays. All new displays at our place are
1080p these days. And the Output of the sledgehammer tool and the panel
itself don't really fit on the side if you give it a try. You can't see
which suggestion is the shortest nor the timing.
The "Locate" button of the panel indicates where the presently active
instance is located.
No I mean the other way around. While sledgehammer is running I'm
usually already writing the next statement what ever. So I'm looking at
the code not at some panel at the side. I usually just wait till the
"sledgehammer" command isn't marked as running any more. Also I think
you already noticed that I don't like buttons. ;)
Best
Benedikt
Email Gateway (Aug 19 2022 at 15:48):From: Joachim Breitner <breitner@kit.edu>
Hi,
I’d like to support that suggestion. The complete lack of feedback in
the editor pane about sledgehammer is one of the reasons why I continue
to invoke sledgehammer by typing.
(Of course there is more to it. In the editor, I can change "by (metis
foo bar baz)" relatively easily to "sledgehammer (add: foo bar baz)". I
don’t know how I would do a similar thing with the panel. Maybe with
more interaction in the panel (such as “update this failing metis call
by using its lemmas in the sledgehammer panel”).
But UI guided interaction will always be limited in expressiveness and
efficiency, compared to a textual interface. There is a reason why we
_write_ Isar, and do not use a “proof block panel” to click together the
fixes and assumes, and elsewhere select the initial proof method (not to
speak of the “apply script assembly panel”).
Greetings,
Joachim
who dreams of a document model based ITP that requires nothing
but interacting with the model
signature.asc
Email Gateway (Aug 19 2022 at 15:48):From: Makarius <makarius@sketis.net>
Both the writing and clicking that is sketched here is cumbersome, and
conceptually not really different. A more high-level editing model of
interactice proof documents is required, and apply scripts should be left
behind altogether.
I've started working on more than 15 years ago, but even today people
still think of the source text as a "script" that is somehow linear.
Makarius
Email Gateway (Aug 19 2022 at 15:48):From: bnord <bnord01@gmail.com>
Well I'd like a voice interface where I just explain the proof idea and
sledgehammer and friends pick up keywords to generate a proof from that.
But maybe let's focus on what can be improved on the current state of
the art.
Last updated: Apr 18 2024 at 20:16 UTC