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 <makar...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
