<div dir="ltr"><div>I just tried running the commands in polyc manually: $ echo "use \"selftest.sml\"; PolyML.export(\"selftest\", main);" | poly -q --error-exit </div>[no errors, selftest.obj created] <div>$ 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 </div><div>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. </div></div><div class="gmail_extra"> <div class="gmail_quote">On Sun, Oct 12, 2014 at 6:47 PM, Mario Carneiro <<a href="mailto:di.gama@gmail.com" target="_blank">di.gama@gmail.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>The log was obtained via your earlier instruction: make bin/polyml/selftest.sml poly < bin/polyml/selftest.sml | tee poly.log </div>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 </div>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. </div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"> <div class="gmail_quote">On Sun, Oct 12, 2014 at 6:42 PM, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Mario, How did you obtain this log? Did you type "make polyml" in the opentheory directory, as per <a href="http://www.gilith.com/software/opentheory/install.html" target="_blank">http://www.gilith.com/software/opentheory/install.html</a> 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 <div><div> On Sun, Oct 12, 2014 at 1:34 PM, Mario Carneiro <<a href="mailto:di.gama@gmail.com" target="_blank">di.gama@gmail.com</a>> 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 <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote: >> >> Hi Mario, >> >> I've just made a new release of the opentheory tool >> >> <a href="http://www.gilith.com/software/opentheory/download.html" target="_blank">http://www.gilith.com/software/opentheory/download.html</a> >> >> 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 >> >> <a href="http://opentheory.gilith.com/?pkg=base" target="_blank">http://opentheory.gilith.com/?pkg=base</a> >> >> as one OpenTheory article file, and the result can be found here: >> >> <a href="http://www.gilith.com/base.art" target="_blank">http://www.gilith.com/base.art</a> >> >> 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 <<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>> wrote: >> > Mario, >> > >> > On 12 Oct 2014, at 03:57, Mario Carneiro <<a href="mailto:di.gama@gmail.com" target="_blank">di.gama@gmail.com</a>> 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 (<a href="http://opentheory.gilith.com/" target="_blank">http://opentheory.gilith.com/</a>) 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 >> > <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a> >> > <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >> > >> > >> > >> > _______________________________________________ >> > opentheory-users mailing list >> > <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a> >> > <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >> > >> >> _______________________________________________ >> opentheory-users mailing list >> <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a> >> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >> >> > > > _______________________________________________ > opentheory-users mailing list > <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a> > <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> > _______________________________________________ opentheory-users mailing list <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> </div></div></blockquote></div> </div> </div></div></blockquote></div> </div>