[isabelle-dev] Towards the next release
makarius at sketis.net
Thu Nov 29 18:22:31 CET 2012
On Thu, 29 Nov 2012, Lawrence Paulson wrote:
> Will it run without compiled files? And will it run efficiently enough?
> Certainly I've always compiled my copy.
> On 21 Nov 2012, at 10:35, Makarius <makarius at sketis.net> wrote:
>> * A version of Proof General as Isabelle component, like
>> (it must be platform/emacs independent, without .elc files).
As far as I remember, we've never had a bundled version of Proof General
with compiled .elc files. These are non-portable across Emacs versions,
so it will not work by default. Working a bit slower is better than not
working at all.
Once users start recompiling and rearranging things, it gets more like
IKEA do-it-yourself software. (I am myself an expert of IKEA hardware
assembly for the kitchen and usually enjoy it. Not for software, though.)
BTW, for recompiling you need Unix "make", and that is not installed by
default on any of the 3 platform families: Linux, Mac OS X, Windows.
Generally, it touches the question if Proof General should be bundled at
all. I started that a long time ago to approximate an out-of-the-box
experience for Isabelle, but never succeeded in the last consequence.
Right now there are PG 188.8.131.52, 4.0, 4.1 being activly used, so which one
to chose? (I would have taken the latest stable version.)
Coq never had a PG bundled either, and expert users expect it like that.
David Aspinall never liked the bundling of Isabelle Proof General in the
So is it time to stop it?
More information about the isabelle-dev