Re: [isabelle] Isabelle's jEdit plugin: some known help documents?
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Isabelle's jEdit plugin: some known help documents?
- From: Gottfried Barrow <gottfried.barrow at gmx.com>
- Date: Tue, 31 Jul 2012 18:36:59 -0500
- In-reply-to: <alpine.LNX.email@example.com>
- References: <op.wibg4tbsule2fv@douda-yannick> <50180DC3.firstname.lastname@example.org> <alpine.LNX.email@example.com>
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0
On 7/31/2012 3:23 PM, Makarius wrote:
On Tue, 31 Jul 2012, Gottfried Barrow 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.
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
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.)
I keep the comments from the cheap seats short(er).
People from different segments of the market will have different
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.
LINK: Coq on Windows.
This archive was generated by a fusion of
Pipermail (Mailman edition) and