Email Gateway (Aug 19 2022 at 10:10): Email Gateway (Aug 19 2022 at 10:10):From: John Wickerson <jpw48@cam.ac.uk>
Dear Isabelle,
Following on from a point Tobias made a while ago, that ...
jedit ... forces you to wait until sledgehammer has returned before you can scroll around - otherwise s/h is interrupted and restarts
... can I suggest a new feature: that sledgehammer gives some sort of audible feedback? Because I can't do anything until the sledgehammer is finished, I usually type "sledgehammer", then go and browse the internet or look out of my window for a minute or so, then come back and see if it worked. So, I think it would be nice if sledgehammer made some sort of noise to tell me when it has succeeded or timed-out.
John
Email Gateway (Aug 19 2022 at 10:10):From: Makarius <makarius@sketis.net>
The JVM might support sound and more, but I don't know how it works out in
practice. JavaFX might be another starting point for multi-media etc.
I am myself not as ambitious right now. For Isabelle2013 I have dared to
use pupup windows with a little bit of focus change, and it caused a lot
of trouble that is not fully settled yet (e.g. with strange Linux window
managers).
Generally note that the synchronous behaviour of sledgehammer in
Isabelle/jEdit is accidental. The documement model is meant to be as
asynchronous and parallel as feasible, so you don't wait in the first
place. Having 5 sledgehammers in parallel would also cause a lot of noise
if they would produce audible feedback.
I had already sketched an approach to integrate "asynchronous agents"
natively into the document model around 2009, but got distracted by
endless other problems, like maintaining Proof General at the same time,
people asking for imitation of Proof General features in Isabelle/jEdit,
Oracle and Apple fighting each other etc.
After stopping Proof General maintenance in October 2011, progress with
Isabelle/jEdit has become much faster. And I hope to have a chance to
revisit the old "asynchronous agents" idea soon, if there are not again
all these distractions and complaints about things changing.
Makarius
Email Gateway (Aug 19 2022 at 10:10):From: Lawrence Paulson <lp15@cam.ac.uk>
I certainly hope instead to see a restoration of one of sledgehammer's key advantages, namely that it ran in the background so that you could indeed continue to work on your proof. This was one of its design goals from the very beginning.
The entire internal architecture supports this background execution, so it should be possible.
Larry Paulson
Email Gateway (Aug 19 2022 at 10:10):From: Makarius <makarius@sketis.net>
Which version of the architecture do you mean? Fabian Immler and myself
rewrote most of it from scratch in 2008, to make it work without Unix
process fork, and thus on Cygwin for the first time. Later Jasmin also
rewrote it again.
All of that is for the TTY loop, though. It has to be re-integrated into
the native Isabelle document model, and this is where I am stuck for
several years for no particular technical reasons, just social ones.
Makarius
Last updated: Apr 27 2024 at 04:17 UTC