But that’s the *same* mini theory we used before, with only a single Datatype definition:
open HolKernel Parse boolLib bossLib;
val _ = new_theory "Test”;
val _ = Datatype `Dertree = Der 'a (Dertree list)`;
val _ = export_theory ();
I have no way to break that Datatype definition into smaller pieces ...
Regards,
Chun Tian
> Il giorno 01 mag 2017, alle ore 07:42, Ramana Kumar
> <ramana.ku...@cl.cam.ac.uk> ha scritto:
>
> 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?
> >
>
>
>
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
