<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><div><div>Hm, it's a little better, but the last lines are<br><br>val main = fn: unit -> unit<br><br></div>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.)<span class="HOEnZb"></span><br><span class="HOEnZb"></span><br><span class="HOEnZb"></span><br><span class="HOEnZb"></span><br><span class="HOEnZb"><font color="#888888">Mario</font></span><div><div class="h5"><br><div><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Oct 12, 2014 at 2:14 PM, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Mario,<br>
<br>
I've just made a new release of the opentheory tool<br>
<br>
<a href="http://www.gilith.com/software/opentheory/download.html" target="_blank">http://www.gilith.com/software/opentheory/download.html</a><br>
<br>
that fixes the Poly/ML compile script (I was using polyc, but had left<br>
the old export directive in the source). Perhaps that will fix the<br>
problem? Unfortunately, I can't test it because I don't have access to<br>
a Cygwin setup.<br>
<br>
In case it doesn't, I ran the command<br>
<br>
opentheory info --article -o base.art base<br>
<br>
which exports the standard theory library<br>
<br>
<a href="http://opentheory.gilith.com/?pkg=base" target="_blank">http://opentheory.gilith.com/?pkg=base</a><br>
<br>
as one OpenTheory article file, and the result can be found here:<br>
<br>
<a href="http://www.gilith.com/base.art" target="_blank">http://www.gilith.com/base.art</a><br>
<br>
This may help you evaluate whether OpenTheory will be suitable for your project.<br>
<br>
Cheers,<br>
<br>
Joe<br>
<div><div><br>
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:<br>
> Mario,<br>
><br>
> On 12 Oct 2014, at 03:57, Mario Carneiro <<a href="mailto:di.gama@gmail.com" target="_blank">di.gama@gmail.com</a>> wrote:<br>
><br>
> Hello, I'm trying to run the opentheory program, and I believe I have<br>
> correctly installed Poly/ML for compilation on Cygwin in Windows 8. However,<br>
> it appears to be crashing in the self-test:<br>
><br>
><br>
> $ make<br>
> make[1]: Entering directory<br>
> '/cygdrive/c/Users/Mario/Documents/hol-light/ot/opentheory'<br>
><br>
> +-------------------------------------+<br>
> | Build and test the Poly/ML programs |<br>
> +-------------------------------------+<br>
><br>
><br>
> +---------------------------+<br>
> | Compile a Poly/ML program |<br>
> +---------------------------+<br>
><br>
> bin/polyml/selftest<br>
> cd bin/polyml && polyc  -o selftest selftest.sml<br>
> Exception- SysErr ... raised<br>
> Makefile:270: recipe for target 'bin/polyml/selftest' failed<br>
> make[1]: *** [bin/polyml/selftest] Error 1<br>
> rm bin/polyml/selftest.sml<br>
> make[1]: Leaving directory<br>
> '/cygdrive/c/Users/Mario/Documents/hol-light/ot/opentheory'<br>
> Makefile:14: recipe for target 'default' failed<br>
> make: *** [default] Error 2<br>
><br>
><br>
> Since there isn't any additional information, I'm not sure what about the<br>
> self-test is causing problems, and in the bin/polyml folder the selftest.sml<br>
> file that is created is gigantic, 67833 lines, and appears to be the<br>
> concatenation of all the source files, so I have no idea what is going on or<br>
> how to diagnose it. Suggestions?<br>
><br>
><br>
> Try doing:<br>
><br>
> make bin/polyml/selftest.sml<br>
><br>
> to make the big source file, and then<br>
><br>
> poly < bin/polyml/selftest.sml | tee poly.log<br>
><br>
> which will run Poly/ML in its interactive mode.<br>
> This will list the structures that make up the<br>
> program as they are compiled and give some idea<br>
> where the compilation is failing.<br>
><br>
> Alternatively, is there any other way to download the opentheory files<br>
> decompiled from HOL Light (which is my actual goal)? There appears to be a<br>
> repository of such files (<a href="http://opentheory.gilith.com/" target="_blank">http://opentheory.gilith.com/</a>) but it recommends<br>
> installation of this program in order to do the download and since it's not<br>
> precompiled this is giving me a lot of trouble.<br>
><br>
><br>
> I don't think the opentheory files will be any use to you<br>
> without the opentheory program to process them.<br>
><br>
> Regards,<br>
><br>
> Rob.<br>
><br>
><br>
> Mario Carneiro<br>
> _______________________________________________<br>
> opentheory-users mailing list<br>
> <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
><br>
><br>
><br>
> _______________________________________________<br>
> opentheory-users mailing list<br>
> <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
><br>
<br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</div></div></blockquote></div></div></div></div></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><div><div class="h5"><div class="gmail_extra"><br></div></div></div></div>
</blockquote></div><br></div></div>