I also see this bug happen when trying to build examples/acl2/ml. However,
this patch doesn't seem to build right on a Mac running OS X (10.4) with the
following gcc:
$ gcc --version
i686-apple-darwin8-gcc-4.0.1 (GCC) 4.0.1 (Apple Computer, Inc. build 5367)
The Makefile.inc section that is uncommented is
# For Mac OS X 10.x.y (Intel or PowerPC), use:
# --------------------------------------------
CPP=/usr/bin/cpp -no-cpp-precomp -P -traditional -Dunix -Umsdos
STRIP=echo
LD=gcc
DYNLD=gcc -bundle -bundle_loader ${MOSMLHOME}/bin/camlrunm
On starting "make world", the build fails with the last lines being
cd mosmllib; make all
/usr/bin/cpp -no-cpp-precomp -P -traditional -Dunix -Umsdos Array.mlp >
Array.sml
../camlrunm ../mosmlcmp -stdlib ../mosmllib -P none -imptypes Vector.sig
buildrealmap: opcode = 255 at 2332
bad opcode
make[1]: *** [Vector.ui] Error 2
make: *** [world] Error 2
"make world" builds fine without the patch. Any suggestions?
Peter
On Tue, Oct 14, 2008 at 8:02 PM, Michael Norrish <
[EMAIL PROTECTED]> wrote:
> Tom Ridge wrote:
>
>> Hi Mike,
>>
>> I have located some mails I sent in 2005 where exactly this error was
>> reported under mosml. The problem apparently arose because lots of ML
>> level identifiers (val f, val g...) were created, and some internal
>> mosml limit was breached. To get around this problem, Peter Sestoft
>> provided a patched version of mosml that was able to deal with many
>> more identifiers. We then used this version of mosml on the NetSem
>> project.
>>
>> Perhaps Peter can put these changes in the current release of mosml.
>> Alternatively I can probably track down some instructions for patching
>> a release of mosml to fix this problem.
>>
>
> The patch is in the attached file. You need to unpack this file in
> your mosml/src directory. I.e., change to that directory, do
>
> tar xvzf mosml-patch.tgz
>
> and then a complete rebuild of Moscow ML. Assuming your makefile is
> already set up correctly for your installation, something like
>
> make clean ; make world ; make install
>
> should do the trick.
>
> If you're running on Windows, you're probably out of luck, though
> there are Moscow ML instructions on installing from sources for
> Windows. (And we don't have HOL working on Poly/ML on Windows
> either.)
>
> Michael.
>
--
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)
-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
