Re: [isabelle] Isabelle's jEdit plugin: some known help documents?

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 developers.

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 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.


LINK: Coq on Windows.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.