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
CygWin

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 http://isabelle.in.tum.de/installation.html

(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:
 /home/Jens/.isabelle/heaps/Isabelle2009/polyml-5.2_x86-cygwin
 /usr/local/Isabelle2009/heaps/polyml-5.2_x86-cygwin

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
  /usr/local/Isabelle2009/contrib/polyml -> polyml-5.2.1
  /usr/local/Isabelle2009/contrib/polyml-5.2.1
  /usr/local/Isabelle2009/contrib/ProofGeneral -> ProofGeneral-3.7.1
  /usr/local/Isabelle2009/contrib/ProofGeneral-3.7.1

etc.


	Makarius





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