Re: [isabelle] Isabelle 2014 and proof general



On 10.09.2014 15:02, Ferdinand Vesely wrote:
> 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.

There is no need to do all this manually. As Makarius mentioned, this is
prepared as an component and components are documented in the system manual:

Add the line

   init_component "$SOME_DIR/ProofGeneral-4.2-2"

to your $ISABELLE_HOME_USER/etc/settings file, where $SOME_DIR refers to
the directory where you want to store the extension. ($USER_HOME/contrib
might be a good value for that, as that is the directory the repository
version stores its components by default).

Then execute

    isabelle components -a

to automatically install the missing component. Afterwards,

    isabelle emacs

should give you a Proof General, provided you have an appropriate emacs
installation around.




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