Re: [isabelle] installing isa2009-test
On Fri, 17 Apr 2009, Randy Pollack wrote:
I just downloaded and installed isa2009-test. "isabelle" seems to be
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.
* Former ISABELLE_INTERFACE is superceded by PROOFGENERAL_HOME
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