Re: [isabelle] install question



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 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.

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




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