[opentheory-users] Overflow

[Ramana Kumar]

Thanks! I'll try it out.

On 28 April 2016 at 17:27, Joe Leslie-Hurd <joe at gilith.com> wrote:

> 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
>
> On Wed, Apr 27, 2016 at 2:35 PM, Joe Leslie-Hurd <joe at gilith.com> 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 <ramana at member.fsf.org>
> wrote:
> >> Unfortunately, I have not been able to produce a small test case, but
> there
> >> is a large-ish one (12MB compressed) available here:
> >> https://hol-theorem-prover.org/overflow.tar.gz.
> >>
> >> It contains three files, hol4-words.thy, hol4-words-unint.art, and
> hol4.int.
> >>
> >> 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 <joe at gilith.com> 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 <ramana at member.fsf.org>
> >>> wrote:
> >>> > Hello,
> >>> >
> >>> > I keep running into this problem:
> >>> >
> >>> > FATAL ERROR: opentheory exception:
> >>> > Overflow
> >>> >
> >>> > What does it mean?
> >>> >
> >>> > Thanks,
> >>> > Ramana
> >>> >
> >>> > _______________________________________________
> >>> > 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/20160428/ddb50a1b/attachment-0001.html>