[isabelle-dev] Isabelle on Leopard/i386
cusquinho at gmail.com
Mon Oct 29 03:50:31 CET 2007
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
Press RETURN to compilation of
Started at Mon Oct 29 00:41:42 BRST 2007 (polyml-4.1.4_ppc-darwin on
Building Pure ...
(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%)
Poly/ML 4.2.0 Release
/usr/local/Isabelle2005/lib/scripts/run-polyml: line 103: 88927
Done echo "PolyML.make_database \"$(fixpath
88928 Bus error | "$POLY" -r "$(fixpath "$INFILE")"
Unable to create output heap file: "/usr/local/Isabelle2005/heaps/polyml-
make: *** [/usr/local/Isabelle2005/heaps/polyml-4.1.4_ppc-darwin/Pure]
make: *** [Pure] Error 2
Finished at Mon Oct 29 00:41:43 BRST 2007
0:00:01 total elapsed time
Do you guys have any idea?
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev