[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