[isabelle] install question



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





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