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

[Mario Carneiro]

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/06067025/attachment.html>