I think it would help if you could find another "mini" theory that exhibits
the same issue... it's hard to tell what's wrong just from the error
messages you sent.
On 29 April 2017 at 23:25, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> Hi Ramana,
>
> Thanks for fixing the issue. I have rebuilt HOL with 672f27ee9 included,
> now previous error in file "Test.art" around line 37270 has disappeared,
> but we got the next issue round line 99993:
>
> FATAL ERROR: opentheory failed:
> in Article.fromTextFile:
> error in file "Test.art" around line 99993:
> thm
> 13076
> ref
> …
> Rule.alpha: not alpha-equivalent
>
> Full logs in zip is in attach. (the mail is re-sent with compressed
> attachments)
>
> Regards,
>
> Chun Tian
>
>
>
>
> > Il giorno 29 apr 2017, alle ore 15:21, Chun Tian (binghe) <
> binghe.l...@gmail.com> ha scritto:
> >
> >> Il giorno 29 apr 2017, alle ore 01:02, Ramana Kumar <
> ramana.ku...@cl.cam.ac.uk> ha scritto:
> >>
> >> Hi Chun,
> >>
> >> Try with the latest update to HOL (672f27ee9), which I think may fix
> the problem in HOL's OpenTheory Logging module.
> >>
> >> Cheers,
> >> Ramana
> >>
> >> On 28 April 2017 at 19:22, Chun Tian (binghe) <binghe.l...@gmail.com>
> wrote:
> >> Hi,
> >>
> >> I see you have already consulted in OpenTheory mailing list and Joe
> Hurd has suggested to use the development version of OpenTheory. Now I see
> this error:
> >>
> >> Test.ot.art
> FAILED!
> >> ('@temp
> @ind_typeTest0list'
> >> a1))))))
> >> ('@temp @ind_typeTest0list'
> >> a1'))))
> >> ('@temp @ind_typeTest0list' a1')))) <=>
> >> HOL4.Test.@temp @ind_typeTest7 (abs r) = r)) in
> >> P (HOL4.min. P)
> >> different constants at path 10110 subterms: HOL4.min.@ vs HOL4.min.
> >> different constants: HOL4.min.@ vs HOL4.min.
> >> different constant names
> >>
> >> I'm sorry for not understanding things at this level, only wondering:
> is this indicating a bug in HOL's OpenTheory module?
> >>
> >> Regards,
> >>
> >> Chun
> >>
> >>
> >>
> >>
> >> On 26 April 2017 at 03:57, Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
> wrote:
> >> Thanks Chun Tian,
> >>
> >> I can reproduce the issue.
> >>
> >> I tried finding out which theorems were causing the failure. They're
> rather ugly (I will paste at the end of this email), but they look like
> valid inputs to the "trans" function to me. It could be something to do
> with the fact that some of the constants have been deleted, but I don't
> know why this would make a difference to OpenTheory, which never deletes
> anything.
> >>
> >> So maybe we should ask on the OpenTheory mailing list and supply the
> Test.art file?
> >
>
>
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
