[opentheory-users] Overflow

[Joe Leslie-Hurd]

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
>>