Email Gateway (Aug 19 2022 at 08:12): Email Gateway (Aug 19 2022 at 08:12):From: Gergely Buday <gbuday@gmail.com>
Yannick,
I am not a constructivist.
And, I could accept that a menu entry would insert a forty letter long
identifier in the proof text. My concern is usability, not theoretical
elegance. Coming up with a proof is a challenging task in itself, and
it is better that the user interface helps creating it, and you need
not remember technicalities in order to advance your proof.
What do the developers think?
Email Gateway (Aug 19 2022 at 08:12):From: Lawrence Paulson <lp15@cam.ac.uk>
I would say that it has nothing to do with constructibility and everything to do with usability. Even 20 years ago, there was hard evidence that people would not read manuals, no matter how carefully they were written. And that was before people got used to discovering what they can and cannot do using menus.
I'm sure that jEdit development will continue and will provide such things eventually. Makarius has asked for volunteers, and I hope one or two enthusiastic students will step forward to help him make jEdit what it should be.
Larry
Email Gateway (Aug 19 2022 at 08:13):From: Makarius <makarius@sketis.net>
On Wed, 8 Aug 2012, Gergely Buday wrote:
4.3 Where have all the menus gone?
In Proof General many settings of Isabelle and diagnostic commands could
be con
gured and started via menus. This is currently not supported in
Isabelle/jEdit.Is there any technical reason for this?
There are conceptual reasons for that. Isabelle/jEdit is not just another
clone of Proof General, but based on a timeless and stateless model of
continous document processing. This makes it a bit challenging to
implement, but I've found 5 years ago that it was high time for the ITP
community to move on towards genuine interaction, not just tty command
loops.
The model underlying Isabelle/jEdit is still awaiting to be augmented by
diagnostic commands as first-class concept. Moreover, I need to add
stateless management of options for particular situations.
Menus are just a very superficial thing. Emacs has little other GUI
elements than menus, so we used them 15 years ago. jEdit has more
possibilities to be put into proper use eventually. So don't wait for an
imitation of Proof General Emacs on the jEdit platform. It has quite
different side conditions.
Makarius
Email Gateway (Aug 19 2022 at 08:16):From: Gergely Buday <gbuday@gmail.com>
Dear Makarius,
you wrote:
Genuine interaction in interactive theorem proving is to be able to
concentrate on the course of the proof without more than needed
distraction of technicalities. I think menus could help this, you say
they wouldn't, and they do not fit the picture. What other
possibilites does jEdit have you refer to?
Email Gateway (Aug 19 2022 at 08:16):From: Makarius <makarius@sketis.net>
Try yourself with a clear mind. There is a small README popup to start
with.
So far the old-time Proof General users had more problems getting
acquainted with Isabelle/jEdit than newcomers.
Makarius
Email Gateway (Aug 19 2022 at 08:18):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Gergely,
To be content, it helps to know what else is out there, which might not
be new news to you:
http://www.cs.ru.nl/~freek/comparison/comparison.pdf
<http://www.cs.ru.nl/%7Efreek/comparison/comparison.pdf>
I found some others, so I have about 25 in my browser bookmarks.
Here's something that looked interesting:
But then, it uses automatic theorem provers:
http://naproche.net/downloads/2009/emergingsystems.pdf
There's Lamports TLA+2:
http://research.microsoft.com/en-us/um/people/lamport/tla/tla2.html
There's http://zermelo.org/
The short of it is that jEdit, as a frontend running on Linux, Windows,
and the Mac, is much better than everything else out there, even in its
incomplete state.
That doesn't mean the others aren't useful to people. The frontend isn't
everything, and someday people will be putting great frontends on a lot
of the other proof assistants, so I predict.
It's a bunch of things: documentation, language syntax, the logic
engine, the editor, support, funding, etc. From my research, Isabelle is
the overall winner, but then, I like it's natural deduction foundation.
Someone else might need something like Coq's logic, not that I know much
about it all. I could decide tomorrow that all this isn't worth the
effort. If I did, I'd go quietly. I can see that people are doing all
they can right now.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:34):From: Gergely Buday <gbuday@gmail.com>
Hi,
at http://arxiv.org/pdf/1208.1368v1.pdf
Christian Sternagel writes:
4.3 Where have all the menus gone?
In Proof General many settings of Isabelle and diagnostic commands
could be con
gured and
started via menus. This is currently not supported in Isabelle/jEdit.
Is there any technical reason for this?
Email Gateway (Aug 19 2022 at 08:35):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Welcome, Gergely,
If you don't mind about a tiny re-interpretation, I would say a more
important question would be “is that really an issue?”. I believe there
are many purely intuitionist proof by exposition of good artifacts, that
the Isabelle jEdit tuple is a good one (teasing and playing with words).
Note that you have the option to set Isabelle's flag from within a theory
file, ex. like writing “using [[simp_trace=true]]” in a proof body. You
may hide from the produced PDF document, using a special comment syntax,
like writing “(<)using [simp_trace=true]”. By the way, I believe
there may be a tiny issue with the simp_trace flags, … will open a thread
about it later.
Cheers
Last updated: Apr 24 2024 at 16:18 UTC