[polyml] problem with polyml on ubuntu on virtualbox

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