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
ProofGeneral setup.

Best wishes,
Ferdinand

> Hence I use the setup from the
> -dev version:
> 
> $ cat .isabelle/etc/settings
> if [[ $ISABELLE_HOME = *2014* ]]; then
>     init_components "$USER_HOME/.isabelle/contrib"
> "$USER_HOME/isabelle/Isabelle-dev/Admin/components/optional"
> fi
> 
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.