Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] duplicate Emacs.app on MacOSX


view this post on Zulip Email Gateway (Aug 18 2022 at 17:06):

From: Perry Wagle <wagle@mac.com>
Isabelle 2011 for MacOSX comes with its own version of Emacs.app for proof general.

This means that its distinct from the Emacs.app I have already installed even though the two are identical. What's the thinking? 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?

-- Perry

view this post on Zulip Email Gateway (Aug 18 2022 at 17:06):

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Perry,

Yes. From the command line, you can specify the -p option to point to any emacs client. For example,

/Applications/Isabelle2011.app/Isabelle/bin/isabelle emacs -p /Applications/Isabelle2009-2.app/Contents/Resources/Emacs.app/Contents/MacOS/Emacs

(all on one line) will launch Isabelle2011 with the Emacs from Isabelle2009-2, assuming the applications are installed at the same places as on my Mac (they should be by default).

Regards,

Jasmin

view this post on Zulip Email Gateway (Aug 18 2022 at 17:07):

From: Makarius <makarius@sketis.net>
On Tue, 22 Feb 2011, Perry Wagle wrote:

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

This means that its distinct from the Emacs.app 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 Isabelle.app it is hard to start an
independent copy of the Emacs.app 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 Isabelle2011.app/Contents/Resources/script
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
Isabelle2011.app/Contents/Resources/script and the general Isabelle
environment is somehow observed by the already running Emacs process.
This might require some Emacs lisp for Proof General initialization.

Makarius


Last updated: Apr 23 2024 at 16:19 UTC