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

[Rob Arthan]

Mario,

On 12 Oct 2014, at 03:57, Mario Carneiro <di.gama at gmail.com> wrote:

> 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?
> 

Try doing:

make bin/polyml/selftest.sml

to make the big source file, and then

poly < bin/polyml/selftest.sml | tee poly.log

which will run Poly/ML in its interactive mode.
This will list the structures that make up the
program as they are compiled and give some idea
where the compilation is failing.

> 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.

I don’t think the opentheory files will be any use to you
without the opentheory program to process them.

Regards,

Rob.

> 
> Mario Carneiro
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141012/adf61456/attachment.html>