Email Gateway (Aug 19 2022 at 11:40): Email Gateway (Aug 19 2022 at 11:40):From: selinger@mathstat.dal.ca
Hi,
here is my first newbie question. Sorry if this is covered elsewhere,
but my web searches did not turn up useful information.
I am a relatively experienced Emacs user, and I have used Proof
General other proof assistants (Coq). Yet I am having trouble getting
Isabelle to work.
I followed the installation instructions at
http://isabelle.in.tum.de/installation.html, I did the following:
cd /tmp
wget http://isabelle.in.tum.de/dist/Isabelle2013_linux.tar.gz
tar zxf Isabelle2013_linux.tar.gz
Isabelle2013/bin/isabelle emacs
The emacs window immediately started up, with the following error
message on the status line:
"Symbol isar is not in proof-assistant-table (in proof-site)"
The Isabelle mode was not loaded and the Scratch.thy buffer not
opened.
I repeated the exact steps on 3 different machines running Ubuntu
12.10 and 13.04, with the same results.
Then I tried it on a completely fresh installation of Ubuntu 13.04 (on
a virtual machine - nothing at all customized), and indeed I got it to
work:
apt-get install emacs
wget http://isabelle.in.tum.de/dist/Isabelle2013_linux.tar.gz
tar zxf Isabelle2013_linux.tar.gz
Isabelle2013/bin/isabelle emacs
Worked with no problems. However, if I install another copy of
proofgeneral (to use with Coq, see above):
apt-get install proofgeneral
Isabelle2013/bin/isabelle emacs
I get again the same error as above.
I think this should not really happen, because the Isabelle scripts
are set up to use the local copy of proofgeneral. Yet somehow, Emacs
loads the wrong one.
Is there a standard solution to this problem? It must be possible to
use Proof General with Coq and Isabelle at the same time.
Thanks, -- Peter
Email Gateway (Aug 19 2022 at 11:43):From: Makarius <makarius@sketis.net>
On Mon, 19 Aug 2013, Peter Selinger wrote:
I am a relatively experienced Emacs user, and I have used Proof
General other proof assistants (Coq). Yet I am having trouble getting
Isabelle to work.I followed the installation instructions at
http://isabelle.in.tum.de/installation.html, I did the following:cd /tmp
wget http://isabelle.in.tum.de/dist/Isabelle2013_linux.tar.gz
tar zxf Isabelle2013_linux.tar.gz
Isabelle2013/bin/isabelle emacs
At that point "Isabelle2013/bin/isabelle jedit" should work out of the
box. It will give you the better system at small cost -- retraining your
fingers to unlearn ESCAPE META ALT CONTROL SHIFT. (As quite experienced
Emacs user this required myself about 2 weeks in 2006, when I finally gave
up that old LISP machine with its add-on editing macros.)
Since you are also using Proof General with Coq their might be a real
danger, though, that you will no longer be efficient with the other system
afterwards.
The emacs window immediately started up, with the following error
message on the status line:"Symbol isar is not in proof-assistant-table (in proof-site)"
I repeated the exact steps on 3 different machines running Ubuntu
12.10 and 13.04, with the same results.Then I tried it on a completely fresh installation of Ubuntu 13.04 (on
a virtual machine - nothing at all customized), and indeed I got it to
work:apt-get install emacs
wget http://isabelle.in.tum.de/dist/Isabelle2013_linux.tar.gz
tar zxf Isabelle2013_linux.tar.gz
Isabelle2013/bin/isabelle emacsWorked with no problems. However, if I install another copy of
proofgeneral (to use with Coq, see above):apt-get install proofgeneral
Isabelle2013/bin/isabelle emacsI get again the same error as above.
I think this should not really happen, because the Isabelle scripts
are set up to use the local copy of proofgeneral. Yet somehow, Emacs
loads the wrong one.Is there a standard solution to this problem? It must be possible to
use Proof General with Coq and Isabelle at the same time.
It is probably just the Debian package of proofgeneral that locks it into
Coq. As often, it helps to de-install some debs and install directly from
the source: http://proofgeneral.inf.ed.ac.uk/
When starting up one Emacs with Proof General, it has initially one chance
to change its personality to "coq", "isar", etc. and then locks into that.
To switch to a different prover you would need a different instance of
Emacs.
That is an old problem of Emacs / Proof General. Divinating around such
issues, especially with Debian defaults, used to be second nature for me
until October 2011, when Isabelle/jEdit became "official and stable" as
Isabelle front-end for the first time. Since then we've had Isabelle2012
(May 2012) and Isabelle2013 (February 2013) with Isabelle/jEdit getting
more and more advanced and leaving Proof General further and further
behind, so it is mostly a nostalgic thing now.
Makarius
Last updated: Apr 19 2024 at 16:20 UTC