> As for avoiding the error above, you might like to try the fixes-5.6 branch > of Poly/ML rather than the released version, since I think there were some > bug fixes made that are relevant to parallel Holmake (I'm not sure). > Alternatively, try passing the -j1 option to bin/build (or Holmake), which > turns off the parallelism.
Okay, that seems to have solved that particular error. Now I'm getting this one: Theory "gcd" took 0.83000s to build Holmake failed with exception: LEX_ERROR "numpairScript.sml 39.9 '.'-whitespace unexpected" Build failed in directory /home/lars/work/reify/HOL/src/num/extra_theories (exited with code 1) Could that also be related to a wrong Poly/ML version? Cheers Lars ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
