<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Mario,<div><br><div><div>On 12 Oct 2014, at 03:57, Mario Carneiro <<a href="mailto:di.gama@gmail.com">di.gama@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><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></blockquote><div><br></div><div>Try doing:</div><div><br></div><div>make bin/polyml/selftest.sml</div><div><br></div><div>to make the big source file, and then</div><div><br></div><div>poly < bin/polyml/selftest.sml | tee poly.log</div><div><br></div><div>which will run Poly/ML in its interactive mode.</div><div>This will list the structures that make up the</div><div>program as they are compiled and give some idea</div><div>where the compilation is failing.</div><br><blockquote type="cite"><div dir="ltr"><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></blockquote><div><br></div>I don’t think the opentheory files will be any use to you</div><div>without the opentheory program to process them.</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div><div><br><blockquote type="cite"><div dir="ltr"><div><br></div><div>Mario Carneiro<br></div></div>
_______________________________________________<br>opentheory-users mailing list<br><a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>http://www.gilith.com/opentheory/mailing-list<br></blockquote></div><br></div></body></html>