[isabelle] Fresh Install?

[Jens Doll]

Hello all,

after doing a fresh install with all the packages recommended on the
download.html page and unzipping Isabelle there is still something
missing. When trying to make my theories, the attached messages occur.
Can someone tell me, what's wrong?

Jens

--------------------------------------------------------------------------------------------
msg ----------------------------------------------------
$ isabelle make
cygpath: can't convert empty path
Running HOL-Theorien ...
Unknown logic "HOL" -- no heap file found in:
/home/Jens/.isabelle/Isabelle2011-1/heaps/polyml-undefined_x86-cygwin
/Isabelle2011-1/heaps/polyml-undefined_x86-cygwin
HOL-Theorien FAILED
(see also
/home/Jens/.isabelle/Isabelle2011-1/heaps/polyml-undefined_x86-cygwin/log/HOL-Theorien)

IsaMakefile:25: recipe for target
`/home/Jens/.isabelle/Isabelle2011-1/heaps/polyml-undefined_x86-cygwin/log/HOL-Theorien.gz'
failed
make: ***
[/home/Jens/.isabelle/Isabelle2011-1/heaps/polyml-undefined_x86-cygwin/log/HOL-Theorien.gz]
Error 2
---------------------------------------------------------------------------------------------------
end msg ----------------------------------------------------

[Lars Noschinski]

Post by Jens Doll
--------------------------------------------------------------------------------------------
msg ----------------------------------------------------
$ isabelle make
cygpath: can't convert empty path
Running HOL-Theorien ...
/home/Jens/.isabelle/Isabelle2011-1/heaps/polyml-undefined_x86-cygwin
/Isabelle2011-1/heaps/polyml-undefined_x86-cygwin
HOL-Theorien FAILED
(see also
/home/Jens/.isabelle/Isabelle2011-1/heaps/polyml-undefined_x86-cygwin/log/HOL-Theorien)
---------------------------------------------------------------------------------------------------
end msg ----------------------------------------------------

This error message strikes me a bit odd. The precompiled heaps are
somewhere under $ISABELLE_HOME/heaps (i.e. somewhere in the installation
directory), not under $ISABELLE_HOME_USER/heaps (i.e. your .isabelle
directory). $ISABELLE_PATH should contain both.

If you (or your makefile) does not specify paths explicitly (check with
'isabelle getenv ISABELLE_PATH'), HOL should be found.

If you cannot / don't want to change your makefile, as a workaround you
can rebuild HOL as a user by executing 'isabelle make' in
$ISABELLE_HOME/src/HOL -- this puts the heap image into
$ISABELLE_HOME_USER/heaps, where your makefile is looking for it.

-- Lars.

[Makarius]

Post by Jens Doll
$ isabelle make
cygpath: can't convert empty path

This one looks already odd. You can get a bash trace by putting the
command "set -x" close to the start of Isabelle2011-1/bin/isabelle and
then run the above again.

Post by Jens Doll
/home/Jens/.isabelle/Isabelle2011-1/heaps/polyml-undefined_x86-cygwin

polyml-undefined means that the poly executable could not be run (within
its proper process environment provided by Isabelle). Do you actually
have polyml as part of the official
http://isabelle.in.tum.de/dist/Isabelle2011-1_bundle_x86-cygwin.tar.gz ?

The latter also includes Isabelle/HOL prebuilt. Nothing left to do, apart
from saturating Cygwin packages as described on
http://isabelle.in.tum.de/download.html


Makarius

[Makarius]

Post by Makarius

Post by Jens Doll
$ isabelle make
cygpath: can't convert empty path

This one looks already odd.

A secret MS user tells me that this occurred first a few days ago, after
updating Cygwin. The error should be harmless and can be ignored. If you
want to silence it nontheless, you have two possibilities:

* make sure CLASSPATH is non-empty, e.g. setting it to "."

* or edit Isabelle scripts like this:

--- a/lib/scripts/getsettings Thu Mar 01 14:12:18 2012 +0100
+++ b/lib/scripts/getsettings Thu Mar 01 14:42:05 2012 +0100
@@ -55,8 +55,8 @@

#JVM path wrapper
if [ "$OSTYPE" = cygwin ]; then
- CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
- function jvmpath() { cygpath -C UTF8 -w -p "$@"; }
+ CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
+ function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
THIS_CYGWIN="$(jvmpath "/")"
else
function jvmpath() { echo "$@"; }


Your problem with polyml should be independent of that.


Makarius