Re: [isabelle] Isabelle 2014 and proof general
On Wed, 10 Sep 2014 12:25:48 +0200
René Neumann <rene.neumann at in.tum.de> wrote:
> Am 10.09.2014 10:06, schrieb Florian Haftmann:
> > Hi Vadim,
> >> Does it mean 2014 version is no longer support emacs/Proof
> >> General?
> > indeed, yes. There might still be some tricks to keep that alive
> > (which I anyway do not know about), but in the middle run there
> > will be no other way than to use Isabelle/JEdit.
> > Cheers, Florian
> I'm running Isabelle 2014 with PG here. But setting it up was quite a
> hassle. The important thing I noted was: With Isabelle-dev it's
> simple, with the releases it is not.
I'm using PG with the release version. Now I don't remember all the
details but I've took the ProofGeneral package from
http://isabelle.in.tum.de/components/ and unpacked it inside
Isabele2014/contrib (I think it can go anywhere as long as you set the
PROOFGENERAL_HOME environment var). Then I copied the 'emacs' script
from the previous release's 'lib/Tools' folder into the 2014's
'lib/Tools' folder. I think I've set the PROOFGENERAL_HOME environment
variable in my '.bashrc'. Now 'isabelle emacs' works as before.
The jEdit Prover IDE is great but it's greedy compared to the
> Hence I use the setup from the
> -dev version:
> $ cat .isabelle/etc/settings
> if [[ $ISABELLE_HOME = *2014* ]]; then
> init_components "$USER_HOME/.isabelle/contrib"
This archive was generated by a fusion of
Pipermail (Mailman edition) and