Email Gateway (Aug 19 2022 at 08:03): Email Gateway (Aug 19 2022 at 08:03):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi all Isabelle/jEdit users,
Any body know a location for the Isabelle plugin for jEdit help?
I feel the Isabelle community favors Emacs's ProofGeneral over jEdit (or I
may be wrong), and feel there are fewer documents for Isabelle used with
jEdit.
Some documents could be an exhaustive list of the abbreviations which pops
up the character list box (Isabelle plugin's abbreviations, not jEdit own
abbreviations system). I have issue with the input of some characters.
That's also an opportunity to note there are some issues with the
characters used in some of the PDF documenting Isabelle, …some seems wrong.
Interesting documentation topic could also be how to set Isabelle
configuration variables, like how to always have “use
[[simp_trace=true]]”, setting trace depth limits and some others as there
are.
Well, some documentation about the Isabelle plugin for jEdit in its whole.
I had a look at the jEdit plugin manager, but the Help button is disabled
on the Isabelle plugin entry. Searching the web could just return me two
introductory documents, which do not covers the points mentioned above:
* Getting Started with Isabelle/jEdit
http://www.jaist.ac.jp/~c-sterna/publications/S-IUW12.pdf
* Isabelle/jEdit — a Prover IDE within the PIDE framework
http://www4.in.tum.de/~wenzelm/papers/isabelle-jedit-2011-1.pdf
Thanks for any pointers :-)
Email Gateway (Aug 19 2022 at 08:03):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Oops, missed it. For that particular point, go to
Plugins->Isabelle->Prover Session, then select the ReadMe tab. It's in the
middle of the ReadMe tab.
Email Gateway (Aug 19 2022 at 08:04):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 7/31/2012 10:25 AM, Yannick Duchêne (Hibou57) wrote:
Any body know a location for the Isabelle plugin for jEdit help?
Yannick,
I've never seen an Isabelle plugin help. All the helps for plugins show
up under the "Plugins" tree of "Help / jEdit help". Like Emacs, most of
what pertains to using jEdit isn't specific to Isabelle.
I feel the Isabelle community favors Emacs's ProofGeneral over jEdit
(or I may be wrong), and feel there are fewer documents for Isabelle
used with jEdit.
I think the commitment has already been made that jEdit is the future.
Emacs lovers can only savor the present, and long for the past in the
future. I'd get philosophical about all the pros and cons, but it's a
mute point. Lots of things are decided for us by the developers.
If you get used to jEdit, you'll find out that, like Emacs, it's very
powerful, user configurable, has a powerful scripting language, and has
lots of great plugins. Not having got tied into Emacs, ignorance is
bliss for me.
As to how you use jEdit is used with Isabelle, at this point, Isabelle's
operation with jEdit is fairly streamlined. There's the edit buffer, the
output panel to show you current proof information, sidekick to give you
a tree view, and the continuous prover which is always on.
To control all of that, there's essentially the Isar language, and
knowing Isar will get you most of what Emacs makes available through menus.
Menus are nice to show you what's available, but it's not all upside
when I go 3 levels deep in a menu and see 40 items available that I know
nothing about.
With jEdit, anything that's available as na Isar command, you can make
into a menu item and keyborad shortcut with jEdit macros. In fact, any
macro you put under ".isabell/Isabelle2012/jedit/macros" will show up
under the menu "Macros" in the toolbar.
For example, I have a macro "declare[[show_types=false]].bsh", which
contains:
textArea.setSelectedText("declare[[show_types=false]]");
And I have a keyboard shortcut of "Cntl-j-i-t". You assign keyboard
shorcuts to macros with "Plugin options / jEdit / Shortcuts".
That's how I was doing things. Now I put a bunch of commands in a file I
import, like:
declare[[show_brackets=true]] declare[[show_types=true]]
declare[[names_long=false]] declare[[show_sorts=false]]
declare[[names_unique=true]] declare[[show_consts=true]]
Like with Emacs, there's lots of ways to do things. If you know how to
use Isar, then you can get most of the same thing. As far as setting
trace depth, I haven't found anything about that.
Some of the these features will get worked out. From my research,
there's no one else close to Isabelle, what with Isar, jEdit, and
powerful tools like Sledgehammer and Nitpick.
The jEdit plugins are powerful.
The "Console" plugin comes by default. I'm starting to use that because
I get into the same Cygwin environment that jEdit is using. It also
makes it easy to execute commands on the current buffer.
jEdit also has a standard scripting language, Beanshell, and so you get
a standard scripting language with the power of Java. I'm also using the
Jython plugin, http://plugins.jedit.org/plugins/?JythonInterpreter
That will let you tie into Beanshell, and a Jython script can be run as
a jEdit macro. I get the benefits of Python and Beanshell.
All together it's powerful. Learning it's a pain, but there's always a
learning curve to these things.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:04):From: Makarius <makarius@sketis.net>
On Tue, 31 Jul 2012, Yannick Duchêne (Hibou57) wrote:
I feel the Isabelle community favors Emacs's ProofGeneral over jEdit (or
I may be wrong), and feel there are fewer documents for Isabelle used
with jEdit.
Note that Isabelle/jEdit as stable release is younger than 12 months
(October 2011), but Proof General older than 12 years. Just last year at
this time I was still busy chasing critical performace issues in the Scala
actor communication network, which rendered the Prover IDE unusable before
September 2011.
Searching the web could just return me two introductory documents, which
do not covers the points mentioned above:
Getting Started with Isabelle/jEdit
http://www.jaist.ac.jp/~c-sterna/publications/S-IUW12.pdfIsabelle/jEdit — a Prover IDE within the PIDE framework
http://www4.in.tum.de/~wenzelm/papers/isabelle-jedit-2011-1.pdf
These are indeed the two main introductory articles that I know. Users
are invited to share their own experience and tricks with current
Isabelle/jEdit (as of Isabelle2012). See also
https://isabelle.in.tum.de/community for a still somewhat blank and boring
spot for links to interesting user-contributed materials, say your own
blogs, video channels etc.
Googling for Proof General (for Isabelle or Coq), one finds many funny
videos for this ancient editor technology. I am particularly fond of the
Proof General / Coq intro by Andrej Bauer, where he first pretends to
download Proof General 4.x from the website, and then uses the
specifically patched version Proof General 3.7.1.1 that is only available
from the Isabelle distribution :-)
With Isabelle/jEdit one could imagine nice videos that demonstrate the
dynamics of certain popups and other plugins, for example. I am myself
still working on the upgrade of the platform to Java 1.7 and JavaFX 2.2,
so that one might see more onboard multimedia gimmicks in the future, with
HTML5 etc.
Makarius
Email Gateway (Aug 19 2022 at 08:04):From: Makarius <makarius@sketis.net>
Well it mainly depends who is spending time on what. Historically, I have
worked a lot together with David Aspinall on Proof General. It remains to
be seen how active any Emacs lovers can make themselves to continue its
maintenance. (For Proof General / Coq there is quite some recent activity,
e.g. Hendrik Tews porting the classic PVS proof tree gadget or updating
the integration with the "make" tool for separate compilation in Coq.)
Makarius
Email Gateway (Aug 19 2022 at 08:12):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I keep the comments from the cheap seats short(er).
People from different segments of the market will have different
perspectives.
Isabelle key players should want to maintain whatever market share it
has among people tied into Emacs, but where there will be many new jEdit
users to add user improvements to the jEdit interface, especially if the
Isabelle/jEdit prover hooks are documented, there will only be a few
developers who can maintain the low-level connection between the
Isabelle prover and Emacs.
Coq improving Emacs will never help Coq tie into the Windows market
(unless Coq ports it to Windows, which I haven't found to be the case).
Coq's Windows IDE is very simple and basic. It doesn't even have line
numbers. Of course, if you need Coq's dependent types, then you know
what to be grateful for, similarly with Isabelle's simple types. The Coq
IDE is also significantly slower than jEdit's continuous prover when
stepping through small files. I didn't make a big file comparison.
Coq also doesn't have a high-level language like Isar. They may have
majority market share now, but Isabelle has gotten the edge on them as
far as interface and language. A nice IDE and syntax is meaningless if a
prover has no engine, but that's not the context here.
This is just my perspective, speaking from the cheap seats, as a member
of the Windows masses.
Regards,
GB
LINK: Coq on Windows.
http://coq.inria.fr/cocorico/Installation%20of%20Coq%20on%20Windows
Email Gateway (Aug 19 2022 at 08:12):From: Gottfried Barrow <gottfried.barrow@gmx.com>
More commentary from the cheap seats, but I try to be an Isabelle
evangelist, because any big influx of new users would be beneficial to
what I want to do in the long run.
First, the market is so untapped, at this point any success by any proof
assistant is beneficial to every other proof assistant.
No replies to these kind of comments is a good thing, because I spend
too much time doing this kind of thing anyway.
I look at this link for percentage of OS market share:
http://en.wikipedia.org/wiki/Usage_share_of_operating_systems
The percentage of Windows users, as a percentage of the total
percentages of Linux, Mac, and Windows users, is 88.7%.
For simplicity, I assume that the potential market for users of proof
assistants is broken up the same as OS market share.
And who are these potential users? Potentially, it's every mathematics
and computer science university student taking a single class on proof
assistants. Potentially, it's the complete integration of all upper
level proof-based mathematics courses with proof assistants.
It used to be that most serious software and engineering development was
done on Unix, but that's changed. Many or most engineering students,
such as electrical and mechanical majors, learn all their tools on
Windows. Likewise for physics and mathematics students. Likewise even
for a large percentage of information sciences and computer science
students.
You go into a university computer lab. They'll be 100 Windows machines,
8 Macs going largely unused, and some server somewhere that a computer
science student logs into to complete the requirements for the token
Unix based course.
The 11.3%, at this time, can be considered the maximum developer and
user base, and the 88.7% is the potential user base that, for all
practical purposes, has so far gone untapped.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:13):From: Makarius <makarius@sketis.net>
This is in fact the most important observation. In particular one needs
to avoid childish attitudes of "my proof assistant is better than your's".
I usually try to give the people behind the HOL family and Coq some
helpful hints, to improve the packaging and distribution of their systems.
For the core functionality, they know better themselves.
Makarius
Email Gateway (Aug 19 2022 at 08:16):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Standards always help there. Would be nice if they could be some standard
to help interoperability between different proof edition and/or proof
checker systems.
I can see two useful standard kinds.
The first one, for humane readable proof. Isabelle do this with Isar
(which I am still learning), I just know Coq a little bit, but I feel to
remember it has similar thing. Some coordination could be an option and
leads to a standard there? Isabelle's Isar is generic, I don't know if
Coq's equivalent is too.
The second one, for proof check and validation, not necessarily human
readable. This could be comparable to byte-code interpreted language, but
for proof. This would not necessarily byte-code based, but low level
enough, so that any conforming system could check, validate and trust it
(and import/use it!).
After that two standards, multiple systems could be designed in a
conforming way, either as automated prover, semi‑automated, or not
automated at‑all, with different kind of UI, user experience and so on,
without any fears to see this diversity turning into a kind of jungle.
There are so many systems among the few dominating ones which are Coq,
Isabelle (and something named VDM? still in the place?) and Z
environments. A common standard for interoperability would be nice.
Markus says:
“In particular one needs to avoid childish attitudes of "my proof
assistant is better than your's".”
Yes, I understand that point, but for the reasons mentioned above, dealing
with standards, I feel Isabelle may be more an option, because it is based
on SML (standard, formally specified and verified and with multiple
implementation, all unlike OCaml) and may be more standard‑ready with it's
rather generic Isar language.
That said, I don't mean Coq is not nice, I just give the reason why I
personally prefer to spend time learning Isabelle instead of Coq (I
already had a quick look at Coq and CoqIDE).
Email Gateway (Aug 19 2022 at 08:19):From: Lawrence Paulson <lp15@cam.ac.uk>
Standards are possible when you have a universally agreed upon formalism, such as first-order logic: we have TPTP format. And there is a common format for SMT problems. But even with higher-order logic, there are a great many significant differences concerning the nature of types, for example. When you get to systems such as Isabelle and Coq, you have formalisms that are intrinsically different with almost no common ground between them.
Larry Paulson
Email Gateway (Aug 19 2022 at 08:28):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Fame and glory on Youtube is there for the taking because there's
nothing out there to show people what an Isabelle session in jEdit can
look like.
I guarantee you, at this point, all you're lacking is marketing. If
Isabelle was a commercial operation, you would already have a flashy
promotional video out there.
For now, people don't need any instructional videos, they just need an
overview of what a proof assistant is, an overview of the associated
tools for Isabelle, some proof examples to show the interaction between
the edit buffer and the output pane, to see what they can make their
installation look like, and see what tools and plugins they're supposed
to look for when after they've installed Isabelle. It'd be like a 3 to 5
minute video.
All the extra menu features that get added in the future, like
automating the use of "usedir" and IsaMakefiles, aren't going to change
the basic three panel view that's the main work space, at least not
because it's no good right now. That part of the interface and how Isar
is implemented in it is already professional quality. And it's not going
to change the different proof methods, like using intro and elim rules,
or automatic proof methods, or resorting to ATPs with Sledgehammer.
People could be shown a demo of those things in the same video.
Regards,
GB
Last updated: Apr 24 2024 at 12:33 UTC