[opentheory-users] Error in 'make' for opentheory

Mario Carneiro di.gama at gmail.com
Sun Oct 12 02:57:31 UTC 2014


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:


$ make
make[1]: Entering directory
'/cygdrive/c/Users/Mario/Documents/hol-light/ot/opentheory'

+-------------------------------------+
| Build and test the Poly/ML programs |
+-------------------------------------+


+---------------------------+
| Compile a Poly/ML program |
+---------------------------+

bin/polyml/selftest
cd bin/polyml && polyc  -o selftest selftest.sml
Exception- SysErr ... raised
Makefile:270: recipe for target 'bin/polyml/selftest' failed
make[1]: *** [bin/polyml/selftest] Error 1
rm bin/polyml/selftest.sml
make[1]: Leaving directory
'/cygdrive/c/Users/Mario/Documents/hol-light/ot/opentheory'
Makefile:14: recipe for target 'default' failed
make: *** [default] Error 2


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?

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 (http://opentheory.gilith.com/) 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.

Mario Carneiro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141011/a63cc77a/attachment.html>


More information about the opentheory-users mailing list