Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Fresh Install?

Email Gateway (Aug 18 2022 at 19:04):

From: Jens Doll <jd@cococo.de>
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 ----------------------------------------------------

Email Gateway (Aug 18 2022 at 19:05):

From: Lars Noschinski <noschinl@in.tum.de>
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.

Email Gateway (Aug 18 2022 at 19:05):

From: Makarius <makarius@sketis.net>
On Wed, 29 Feb 2012, Jens Doll wrote:

$ 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.

Unknown logic "HOL" -- no heap file found in:
/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

Email Gateway (Aug 18 2022 at 19:16):

From: Makarius <makarius@sketis.net>
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

Last updated: Nov 21 2024 at 12:39 UTC