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

[Mario Carneiro]

Since this same error is happening for a hello world program, I'm going to
try asking the Poly/ML people instead. I'll write back if I have any other
issues once this is resolved.

On Sun, Oct 12, 2014 at 7:04 PM, Mario Carneiro <di.gama at gmail.com> wrote:

> I just tried running the commands in polyc manually:
>
> $ echo "use \"selftest.sml\"; PolyML.export(\"selftest\", main);" | poly
> -q --error-exit
> [no errors, selftest.obj created]
> $ gcc -O3 -I../libffi/include selftest.obj -o selftest -L/usr/local/lib
> -lpolymain -lpolyml -lgdi32 -lwsock32 -lstdc++ -lgcc_s -lgcc
> /usr/lib/gcc/i686-pc-cygwin/4.8.3/../../../../i686-pc-cygwin/bin/ld:
> cannot find -lpolymain
> /usr/lib/gcc/i686-pc-cygwin/4.8.3/../../../../i686-pc-cygwin/bin/ld:
> cannot find -lpolyml
> collect2: error: ld returned 1 exit status
>
> I'm still trying to figure out what's going on in that last error message,
> but it might be a Poly/ML configuration problem.
>
> On Sun, Oct 12, 2014 at 6:47 PM, Mario Carneiro <di.gama at gmail.com> wrote:
>
>> The log was obtained via your earlier instruction:
>>
>> make bin/polyml/selftest.sml
>> poly < bin/polyml/selftest.sml | tee poly.log
>>
>> Executing "make polyml" yields the error message in the original email,
>>
>>
>> +-------------------------------------+
>> | 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:271: recipe for target 'bin/polyml/selftest' failed
>> make: *** [bin/polyml/selftest] Error 1
>>
>>
>> I'm not sure where the SysErr is coming from, since the other command
>> showed no trace of an exception. The two executables are never created - it
>> fails in the first compilation.
>>
>> On Sun, Oct 12, 2014 at 6:42 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>
>>> 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
>>> >
>>>
>>> _______________________________________________
>>> 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/836fd758/attachment-0001.html>