Re: [isabelle] installing isa2009-test

On Fri, 17 Apr 2009, Randy Pollack wrote:

I just downloaded and installed isa2009-test. "isabelle" seems to be installed

but there is no "Isabelle".

There used to be an executable "Isabelle".  After installation in the
path, I could run

 Isabelle -p emacs something.thy

and emacs would come up with proof general and isabelle.  The last
update I had was unofficial from September 2008.

How do I get new isabelle, emacs and Proof General to start up?
Following the instructions I tried

 isabelle emacs -p emacs something.thy

but it didn't find proof general.

Do you have a local ISABELLE_INTERFACE setting in ~/isabelle/etc/settings to point to Proof General? If so, you need to adapt it in two ways:

  * User settings are now in ~/.isabelle/etc/settings so former ~/isabelle
    needs to be renamed to ~/.isabelle

    Note that old Isabelle2008/etc/settings:ISABELLE_HOME_USER can be
    adapted to refer to the new directory as well -- no need to keep
    several copies here.


As usual you can avoid local settings by putting Proof General into a standard place (or symlinking it), e.g. like this:

  ProofGeneral -> ProofGeneral-3.7.1

Now both Isabelle installations should detect this ProofGeneral by default, without any extra settings.


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