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?

Error- in '/tmp/MLTEMPSab29r', line 586. Structure (Polyhash) has not been declared Found near open Polyhash Error- in '/tmp/MLTEMPSab29r', line 587. Value or constructor (mkPolyTable) has not been declared Found near mkPolyTable (length vlist, Fail "varmap") Error- in '/tmp/MLTEMPSab29r', line 589. Type error in function application. Function: insert varmap : ''a list -> ''a list Argument: (h, i) : 'a * 'b Reason: Can't unify ''a list to 'a * 'b (Incompatible types) Found near (insert varmap (h, i); enum t (i - 1) (h :: A)) Error- in '/tmp/MLTEMPSab29r', line 591. Value or constructor (peek) has not been declared Found near case peek vmap v of NONE => v | SOME i => Bv i Error- in '/tmp/MLTEMPSab29r', line 592. Value or constructor (transform) has not been declared Found near transform (fn x => x + 1) vmap Error- in '/tmp/MLTEMPSab29r', line 670. Structure (Polyhash) has not been declared Found near open Polyhash Error- in '/tmp/MLTEMPSab29r', line 671. Value or constructor (mkPolyTable) has not been declared Found near mkPolyTable (Array.length prefix, Fail "AV") Error- in '/tmp/MLTEMPSab29r', line 675. Value or constructor (peekInsert) has not been declared Found near case peekInsert AV (n, PREFIX i) of NONE => insertl rst (i + 1) dupls | SOME _ => ... ... (... + ...) ((...) :: dupls) Error- in '/tmp/MLTEMPSab29r', line 680. Type error in function application. Function: insert AV : ''a list -> ''a list Argument: (s, BODY) : 'a * occtype Reason: Can't unify ''a list to 'a * occtype (Incompatible types) Found near ( (fn s => insert AV (s, ...)), (fn (s, ...) => ... ... (...)), peek AV, dupls ) Error- in '/tmp/MLTEMPSab29r', line 681. Type error in function application. Function: insert AV : ''a list -> ''a list Argument: (s, PREFIX i) : 'a * occtype Reason: Can't unify ''a list to 'a * occtype (Incompatible types) Found near ( (fn s => insert AV (s, ...)), (fn (s, ...) => ... ... (...)), peek AV, dupls ) Error- in '/tmp/MLTEMPSab29r', line 682. Value or constructor (peek) has not been declared Found near let open Polyhash; val AV = mkPolyTable (...); fun insertl ... = ... | ...; val ... = ... in ((fn s => ... ... (...)), (fn (...) => ... ...), peek AV, dupls) end Static Errors

Thanks, Jianjun