Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2009 in Cygwin

Email Gateway (Aug 18 2022 at 13:29):

From: jd@cococo.de
Hello all,

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

Now PG started, but the buttons do not work 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?

Jens

Email Gateway (Aug 18 2022 at 13:31):

From: Makarius <makarius@sketis.net>
On Tue, 12 May 2009, jd@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

Last updated: Nov 21 2024 at 12:39 UTC