[isabelle-dev] PG 3.x vs. 4.x settings
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