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.
mosml-patch.tgz
Description: application/compressed
------------------------------------------------------------------------- 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
