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

[Mario Carneiro]

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/49c35120/attachment-0001.html>