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 are in attach. Regards, Chun Tian
Test.ot.art
Description: Binary data
> 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?
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
