jjduan wrote:
I have a Virtualbox set up on Windows 7 64 bit. On top of it I run Ubuntu.
My intention is to build HOL on Ubuntu.
However I ran into some issue which is weird. It appears on Ubuntu
9.10/9.04, 32 or 64 bit, Polyml 5.3 or 5.2.1. Seems to be a universal
issue. I know someone who runs 64bit Ubuntu 9.10 with Polyml 5.3 and HOL on
a real machine and he doesn't have problems.
Below is a trace. Any help?
This is a HOL problem; it's trying to compile Moscow ML specific code
(hence the references to Polyhash, which exists in Moscow ML, and not
Poly/ML).
You should check that you have a recent version of HOL from Subversion,
and that when you install/configure HOL, it properly recognises that
it's being built with Poly.
Michael
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
