<div dir="ltr">Hello, I'm trying to run the opentheory program, and I believe I have correctly installed Poly/ML for compilation on Cygwin in Windows 8. However, it appears to be crashing in the self-test:<br><div><br><br>$ make<br>make[1]: Entering directory '/cygdrive/c/Users/Mario/Documents/hol-light/ot/opentheory'<br><br>+-------------------------------------+<br>| Build and test the Poly/ML programs |<br>+-------------------------------------+<br><br><br>+---------------------------+<br>| Compile a Poly/ML program |<br>+---------------------------+<br><br>bin/polyml/selftest<br>cd bin/polyml && polyc  -o selftest selftest.sml<br>Exception- SysErr ... raised<br>Makefile:270: recipe for target 'bin/polyml/selftest' failed<br>make[1]: *** [bin/polyml/selftest] Error 1<br>rm bin/polyml/selftest.sml<br>make[1]: Leaving directory '/cygdrive/c/Users/Mario/Documents/hol-light/ot/opentheory'<br>Makefile:14: recipe for target 'default' failed<br>make: *** [default] Error 2<br><br><br></div><div>Since there isn't any additional information, I'm not sure what about the self-test is causing problems, and in the bin/polyml folder the selftest.sml file that is created is gigantic, 67833 lines, and appears to be the concatenation of all the source files, so I have no idea what is going on or how to diagnose it. Suggestions?<br><br></div><div>Alternatively, is there any other way to download the opentheory files decompiled from HOL Light (which is my actual goal)? There appears to be a repository of such files (<a href="http://opentheory.gilith.com/">http://opentheory.gilith.com/</a>) but it recommends installation of this program in order to do the download and since it's not precompiled this is giving me a lot of trouble.<br></div><div><br></div><div>Mario Carneiro<br></div></div>