<div dir="ltr">Thanks! I'll try it out. </div><div class="gmail_extra"> <div class="gmail_quote">On 28 April 2016 at 17:27, 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 Ramana, This turned out to be a simple bug in how numerals were printed in OpenTheory: they were converted into ints by the tool and since your theory contained some large ints this caused an overflow. I've fixed the tool so it no longer converts through an int type, and now I can create the theory for your testcase without an overflow. The fix is both in the latest official version (release 20160428) and also checked into the new github repo. Cheers, Joe <div class="HOEnZb"><div class="h5"> On Wed, Apr 27, 2016 at 2:35 PM, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: > Hi Ramana, > > Thanks for the testcase, I can reproduce your bug and I'll try to root-cause it. > > Cheers, > > Joe > > On Tue, Apr 26, 2016 at 5:45 PM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote: >> Unfortunately, I have not been able to produce a small test case, but there >> is a large-ish one (12MB compressed) available here: >> <a href="https://hol-theorem-prover.org/overflow.tar.gz" rel="noreferrer" target="_blank">https://hol-theorem-prover.org/overflow.tar.gz</a>. >> >> It contains three files, hol4-words.thy, hol4-words-unint.art, and <a href="http://hol4.int" rel="noreferrer" target="_blank">hol4.int</a>. >> >> To produce the error, edit the paths in hol4-words.thy to point to the other >> two files, then try this: >> opentheory info --theory hol4-words.thy >> >> On 21 April 2016 at 02:28, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: >>> >>> It means that an integer overflow is occurring somewhere in the >>> processing, which shouldn't happen. If you give me a test case where >>> this occurs (the smaller the better) I can look into it. >>> >>> Cheers, >>> >>> Joe >>> >>> On Tue, Apr 19, 2016 at 6:12 PM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> >>> wrote: >>> > Hello, >>> > >>> > I keep running into this problem: >>> > >>> > FATAL ERROR: opentheory exception: >>> > Overflow >>> > >>> > What does it mean? >>> > >>> > Thanks, >>> > Ramana >>> > >>> > _______________________________________________ >>> > opentheory-users mailing list >>> > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>> > <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >>> > >>> >>> _______________________________________________ >>> opentheory-users mailing list >>> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >> >> >> >> _______________________________________________ >> opentheory-users mailing list >> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >> _______________________________________________ opentheory-users mailing list <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> </div></div></blockquote></div> </div>