[isabelle-dev] PG 3.x vs. 4.x settings
Lawrence Paulson
lp15 at cam.ac.uk
Fri Dec 14 13:57:51 CET 2012
But for the Mac version we bundle a specific Emacs binary anyway.
Larry
On 14 Dec 2012, at 12:56, Makarius <makarius at sketis.net> wrote:
> On Wed, 12 Dec 2012, Lawrence Paulson wrote:
>
>> I compiled 4.2, no problem.
>
> You mean byte-compiled .el -> .elc? This causes a lock-in to a particular Emacs version, so it reduces chances of users being able to run it.
>
> I used to have the principle that even in the Isabelle.app bundle the included Emacs.app is merely a sensible default that users may override. On Linux, Emacs is not bundled at all, so one needs to expect a certain range of GNU Emacs 23 .. 24 versions, probably not Emacs 22 anymore.
>
> Shipping byte-compiled files works against that. The Isabelle "component" for Proof General needs to work with the variety of situations uniformly -- we don't have component variants. Whatever is done in the component wrapper scripts, it needs to work without the "make" tool, which is absent on the majority of systems now.
>
>
> Makarius
More information about the isabelle-dev
mailing list