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

[Mario Carneiro]

Hm, it's a little better, but the last lines are

val main = fn: unit -> unit

and I think that the "main" function is created by the script as well, and
is also huge. There is no error message, it just quits after this. Or does
that mean it worked? (PS: Poly/ML needs to work on their error reporting.)



Mario



On Sun, Oct 12, 2014 at 2:14 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:

> 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
> >
>
> _______________________________________________
> 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/a7eccdf1/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: poly.log
Type: application/octet-stream
Size: 3937 bytes
Desc: not available
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141012/a7eccdf1/attachment-0001.obj>