Email Gateway (Aug 18 2022 at 13:24): Email Gateway (Aug 18 2022 at 13:24):From: Randy Pollack <rpollack@inf.ed.ac.uk>
I just downloaded and installed isa2009-test. "isabelle" seems to be installed
$isabelle version
isa2009-test: April 2009
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.
(Actually "Isabelle -p emacs something.thy" still works, bringing up
my older version, because the old "Isabelle" wasn't over-written by
the new install.)
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.
Thanks,
Randy
Email Gateway (Aug 18 2022 at 13:24):From: Makarius <makarius@sketis.net>
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:
Isabelle2008/
isa2009-test/
ProofGeneral-3.7.1/
ProofGeneral -> ProofGeneral-3.7.1
Now both Isabelle installations should detect this ProofGeneral by
default, without any extra settings.
Makarius
Last updated: May 03 2024 at 12:27 UTC