Re: [isabelle] duplicate on MacOSX

On Tue, 22 Feb 2011, Perry Wagle wrote:

Isabelle 2011 for MacOSX comes with its own version of for proof general.

This means that its distinct from the I have already installed even though the two are identical. What's the thinking?

The general idea is to sacrifice some disk space to approximate a fully integrated application that runs out of the box as far as possible. Unfortunately there are occasional conflicts with how Mac OS X thinks about this. For example, after running it is hard to start an independent copy of the that happens to be used here.

Can I combine Isabelle 2011's version with my already installed version using some sort of "emacsclient -c" interface so that I have only one instance of the app running?

The main plumbing is done in which can in principle be customized by ambitious users, but there are many well-known problems awaiting.

In particular, the version of Emacs and Proof General need to fit together -- before each official Isabelle release 1-2 weeks are set aside for a desparate search of a combination that works most of the time.

Using actual "emacsclient" is even more tricky, but not impossible. Ultimately you need to ensure that the careful environment setup of and the general Isabelle environment is somehow observed by the already running Emacs process. This might require some Emacs lisp for Proof General initialization.


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