[isabelle-dev] Isabelle on Leopard/i386

[Fernando Costa]

Hi All,

I'm new to the list and I could not find any information regarding this in
the archives. Please let me know if this is not a pertinent discussion.

I've used Isabelle in PPC architecture with no issue in the past, but in
Intel Macs I've been having some issues that you may be able to help. I've
installed Isabelle and xemacs with Fink, and it's working just fine. The
problem is in polyml and compiling the logics:

First, the script to detect the Polyml architecture fails on Intel Macs. The
"uname -m" returns only i386, which fails to search for the ppc-darwin file
in polyml directory. Second, when I try to compile the logics, this is what
I get:

Press RETURN to compilation of

  FOL


Started at Mon Oct 29 00:41:42 BRST 2007 (polyml-4.1.4_ppc-darwin on
simone-costas-macbook.local)
Building Pure ...
Pure FAILED
(see also /usr/local/Isabelle2005/heaps/polyml-4.1.4_ppc-darwin/log/Pure)

Poly/ML RTS version PPC-4.1.4 (14:25:13 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%)
Mapping /usr/local/Isabelle2005/../polyml/ppc-darwin/ML_dbase
Poly/ML 4.2.0 Release
/usr/local/Isabelle2005/lib/scripts/run-polyml: line 103: 88927
Done                    echo "PolyML.make_database \"$(fixpath
"$OUTFILE")\"; PolyML.quit();"
     88928 Bus error               | "$POLY" -r "$(fixpath "$INFILE")"
Unable to create output heap file: "/usr/local/Isabelle2005/heaps/polyml-
4.1.4_ppc-darwin/Pure"

make[1]: *** [/usr/local/Isabelle2005/heaps/polyml-4.1.4_ppc-darwin/Pure]
Error 2
make: *** [Pure] Error 2
Finished at Mon Oct 29 00:41:43 BRST 2007
0:00:01 total elapsed time
sh-3.2#

Do you guys have any idea?

Thanks,

Fernando
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20071029/9e33e237/attachment.html>