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

[Joe Leslie-Hurd]

Hi Mario,

I've just made a new release of the opentheory tool

http://www.gilith.com/software/opentheory/download.html

that fixes the Poly/ML compile script (I was using polyc, but had left
the old export directive in the source). Perhaps that will fix the
problem? Unfortunately, I can't test it because I don't have access to
a Cygwin setup.

In case it doesn't, I ran the command

opentheory info --article -o base.art base

which exports the standard theory library

http://opentheory.gilith.com/?pkg=base

as one OpenTheory article file, and the result can be found here:

http://www.gilith.com/base.art

This may help you evaluate whether OpenTheory will be suitable for your project.

Cheers,

Joe

On Sun, Oct 12, 2014 at 2:39 AM, Rob Arthan <rda at lemma-one.com> wrote:
> 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
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>