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

[Joe Leslie-Hurd]

Hi Mario,

How did you obtain this log? Did you type "make polyml" in the
opentheory directory, as per

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

This should invoke polyc on the concatenated source code and produce
two executables in the bin/polyml directory: selftest and opentheory.
It then runs a self-test to make sure everything is working. If
anything fails then the "make polyml" command will result in an error,
otherwise you should have a working opentheory tool in bin/polyml.

Cheers,

Joe

On Sun, Oct 12, 2014 at 1:34 PM, Mario Carneiro <di.gama at gmail.com> wrote:
> 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
>>
>>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>