[isabelle-dev] Towards the next release

[Makarius]

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
>>    http://isabelle.in.tum.de/components/ProofGeneral-4.1.tar.gz
>>    (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 3.7.1.1, 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 
first place.

So is it time to stop it?


 	Makarius