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.