Isabelle you bitch!

I finally got Isabelle working. The installation instructions on the website make it seem simple. And it is. It’s just that many things can go wrong and they don’t account for them.

Here’s what I did: Got the source for polyml, built and installed it in /usr/local. Got the sources for Isabelle and Proof General (nothing prebuilt). Built Isabelle. But in Proof General’s makefile, it said:

EMACS=$(shell if [ -z "`which emacs`" ]; then echo xemacs; else echo emacs; fi)

I have both GNU Emacs and XEmacs installed, which means that EMACS got set to GNU Emacs. This was very confusing, since Isabelle started XEmacs anyway, but all the elc files were compiled by GNU Emacs.

I changed it to:


And all was well. Whew.

Now I get to see what all this Isabelle hype is about.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s