[isabelle-dev] PG 3.x vs. 4.x settings

Makarius makarius at sketis.net
Fri Dec 14 13:56:21 CET 2012

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.


More information about the isabelle-dev mailing list