Re: [isabelle] Isabelle2009 in Cygwin
On Tue, 12 May 2009, jd at cococo.de wrote:
after having extracted Isabelle2009 to /usr/local I called my script in
bash --login -i -c /home/Jens/.isabelle
where .isabelle contains
/usr/local/Isabelle/bin/isabelle emacs -p xemacs
Using /home/Jens/.isabelle is a bit odd in general and in Isabelle2009
$HOME/.isabelle is now the ISABELLE_HOME_USER directory per default. So
strange effects can be anticipated, although the present problem probably
stems from somewhere else.
Since option -c of bash accepts a command line script, you can do it
directly like this:
bash --login -i -c "/usr/local/Isabelle/bin/isabelle emacs -p xemacs"
Note that without starting X11 first (e.g. via startxwin.sh), you will not
be able to use XEmacs with X-Symbol mode.
Now PG started, but the buttons do not work
I've tried this myself on an older Cygwin installation that was updated
via "setup". Here Proof General with XEmacs 21.4.22 failed completely,
due to strange autoload problems.
On a fresh install of Cygwin, everything worked as described on
(When discarding a Cygwin installation you normally want to preserve your
/home and probably also /use/local stuff.)
and the menu item "Next.Step" yields
Unknown logic "HOL" -- no heap file found in:
Everything else is like in Isabelle2008. What can be wrong?
This looks like you did not update Poly/ML, which is 5.2.1 in
Isabelle2009. With the install location directly in /usr/local you will
get need some extra care, if you want to preserve Isabelle2008. Multiple
versions work better if extra components are put into Isabelle/contrib/
with the following directory layout:
/usr/local/Isabelle2009/contrib/polyml -> polyml-5.2.1
/usr/local/Isabelle2009/contrib/ProofGeneral -> ProofGeneral-3.7.1
This archive was generated by a fusion of
Pipermail (Mailman edition) and