<div dir="ltr"><div>> This is a case of a theory-local definition clashing with an existing definition of the same name. It will be solved by the same change that I'm working on that will make the extra extend_the_interpretation commands unnecessary. </div><div> </div>So looks like i can't do anything for now on it?<div> </div><div> </div></div><div class="gmail_extra"> <div class="gmail_quote">On 6 October 2015 at 23:04, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Robert, This is a case of a theory-local definition clashing with an existing definition of the same name. It will be solved by the same change that I'm working on that will make the extra extend_the_interpretation commands unnecessary. Cheers, Joe On Tue, Oct 6, 2015 at 4:00 AM, Robert White <div class="HOEnZb"><div class="h5"><<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: > Dear Joe, > > I also noticed that parser is has the following errors: > > Exception: > > Failure > > "in article parser.art at line 457: defineConst\nstack = [Term; > \"HOLLight.NUMSUM\"; Term; Term; Term; Var; Term; Var; Term; Var; Term; Var; > [[\"HOLLight.NUMLEFT\"; Var]]; Term; Var; Var; Var; Var; \"HOLLight.INJP\"; > \"HOLLight.ZBOT\"; Term; Term; Term; Var; Term; Term; Var; Term; Var; > \"HOLLight.ZRECSPACE\"; [\"A\"]; \"HOLLight._dest_rec\"; > \"HOLLight._mk_rec\"; \"HOLLight.recspace\"; \"a1\"; Var; [\"A\"]; > \"HOLLight._dest_pstream\"; \"HOLLight._mk_pstream\"; > \"Parser.Stream.stream\"; TypeOp<fun>; TypeOp<fun>; Const<!>; > Term]\nnew_constant: constant NUMSUM has already been declared". > > > I looked into it and found that NUMSUM has been declared in <a href="http://int_type.ml" rel="noreferrer" target="_blank">int_type.ml</a> > which is loaded in <a href="http://hol.ml" rel="noreferrer" target="_blank">hol.ml</a>. > > Could you please update this package? > > Thanks! > > Robert > > > On 6 October 2015 at 12:31, Robert White <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> > wrote: >> >> Dear Joe, >> >> I also have problem loading lazy-list and gfp: >> >> For lazy-list : >> >> Exception: >> >> Failure >> >> "in article lazy-list.art at line 234: const\nstack = >> [\"Data.Option.NONE\"; Var; Term; Term; Term; Var; Term; Term; Var; Term; >> Var; \"llist.lrep_ok\"; Var; Term; Term; [\"A\"]; \"llist.llist.rep\"; >> \"llist.llist.abs\"; \"llist.llist\"; \"a0\"; \"llist.LFINITE\"; Var; Thm; >> Thm]\nunknown constant \"Data.Option.NONE\"". >> >> >> For gfp; >> >> >> Exception: >> >> Failure >> >> "in article gfp.art at line 676: axiom\nstack = [Term; []; Thm; Thm; >> Thm]\nunknown assumption:\n|- prime oddprime". >> >> >> Could you please help on that? Thanks a lot! >> >> Regards >> >> Robert >> >> >> >> >> >> On 6 October 2015 at 12:15, Robert White <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> >> wrote: >>> >>> Dear Joe, >>> >>> I still get one error from the modular package: >>> >>> Exception: >>> >>> Failure >>> >>> "in article modular.art at line 11928: axiom\nstack = [Term; []; Thm; >>> Thm; [[]; [[Var; Term]]]; Thm; Thm; Thm; Thm; Thm; Thm; Thm; Thm; Thm; Var; >>> Thm; Thm; Thm; Thm; Thm; Var; Thm; Thm; Thm; Thm; >>> [[\"Number.Modular.toNatural\"; Var]]; Term; Var; Var; >>> \"Number.Modular.<=\"; Term; Var; [[]; [[Var; Term]]]; Var; Thm]\nunknown >>> assumption:\n|- ~(modulus = 0)". >>> >>> Is there any package missing? >>> >>> I have loaded the following packages: >>> >>> stream >>> >>> probability >>> >>> natural-bits >>> >>> natural-divides >>> >>> natural-prime >>> >>> >>> Thanks very much! >>> >>> >>> Regards, >>> >>> Robert >>> >>> >>> On 5 October 2015 at 23:27, Robert White <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> >>> wrote: >>>> >>>> Thanks very much Joe. >>>> I also noticed that there is kind of dependency going on but I don't >>>> know how to fix it. >>>> >>>> >>>> On 5 October 2015 at 22:56, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: >>>>> >>>>> Hi Robert, >>>>> >>>>> There are a couple of different obstacles here. >>>>> >>>>> Firstly, it is important that the dependent theories have been >>>>> imported before the theory. To show all the dependent theories, use >>>>> the following command: >>>>> >>>>> $ opentheory list --dependency-order 'Requires+ natural-prime' >>>>> base-1.200 >>>>> natural-divides-1.62 >>>>> stream-1.46 >>>>> >>>>> Now this sequence will succeed: >>>>> >>>>> extend_the_interpretation >>>>> "opentheory/theories/natural-divides/<a href="http://natural-divides.int" rel="noreferrer" target="_blank">natural-divides.int</a>";; >>>>> import_article "natural-divides.art";; >>>>> >>>>> extend_the_interpretation >>>>> "opentheory/theories/stream/<a href="http://stream.int" rel="noreferrer" target="_blank">stream.int</a>";; >>>>> import_article "stream.art";; >>>>> >>>>> extend_the_interpretation >>>>> "opentheory/theories/natural-prime/<a href="http://natural-prime.int" rel="noreferrer" target="_blank">natural-prime.int</a>";; >>>>> import_article "natural-prime.art";; >>>>> >>>>> The second obstacle is that the theory word10 includes the theory >>>>> word, which in turn includes the theory modular. So to successfully >>>>> import word10 you need to extend the interpretation with the >>>>> interpretations for these theories, too: >>>>> >>>>> $ opentheory list --dependency-order 'Requires+ word10' >>>>> base-1.200 >>>>> stream-1.46 >>>>> probability-1.49 >>>>> natural-bits-1.66 >>>>> natural-divides-1.62 >>>>> >>>>> extend_the_interpretation >>>>> "opentheory/theories/stream/<a href="http://stream.int" rel="noreferrer" target="_blank">stream.int</a>";; >>>>> import_article "stream.art";; >>>>> >>>>> extend_the_interpretation >>>>> "opentheory/theories/probability/<a href="http://probability.int" rel="noreferrer" target="_blank">probability.int</a>";; >>>>> import_article "probability.art";; >>>>> >>>>> extend_the_interpretation >>>>> "opentheory/theories/natural-bits/<a href="http://natural-bits.int" rel="noreferrer" target="_blank">natural-bits.int</a>";; >>>>> import_article "natural-bits.art";; >>>>> >>>>> extend_the_interpretation >>>>> "opentheory/theories/natural-divides/<a href="http://natural-divides.int" rel="noreferrer" target="_blank">natural-divides.int</a>";; >>>>> import_article "natural-divides.art";; >>>>> >>>>> extend_the_interpretation >>>>> "opentheory/theories/modular/<a href="http://modular.int" rel="noreferrer" target="_blank">modular.int</a>";; >>>>> extend_the_interpretation >>>>> "opentheory/theories/word/<a href="http://word.int" rel="noreferrer" target="_blank">word.int</a>";; >>>>> extend_the_interpretation >>>>> "opentheory/theories/word10/<a href="http://word10.int" rel="noreferrer" target="_blank">word10.int</a>";; >>>>> import_article "word10.art";; >>>>> >>>>> I regard this second problem as a defect in the theories, because it's >>>>> unreasonable to expect people to discover this information. I'll work >>>>> on fixing it so these multiple extend_the_interpretation commands are >>>>> unnecessary. >>>>> >>>>> Cheers, >>>>> >>>>> Joe >>>>> >>>>> On Sun, Oct 4, 2015 at 2:57 PM, Robert White >>>>> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: >>>>> > Dear Joe, >>>>> > >>>>> > I have problem importing article files. For example: >>>>> > >>>>> > Failure >>>>> > >>>>> > "in article word10.art at line 7495: defineConst\nstack = [Term; >>>>> > \"Number.Modular.equivalent\"; Term; Var; Term; Var; []; >>>>> > \"HOLLight.modular_to_class\"; \"HOLLight.modular_from_class\"; >>>>> > \"Data.Word10.word10\"; TypeOp<fun>; TypeOp<fun>; Const<!>]\nunknown >>>>> > constant \"Number.Modular.equivalent\"". >>>>> > >>>>> > I also have problems with the following packages: >>>>> > >>>>> > natural-prime >>>>> > >>>>> > gfp >>>>> > >>>>> > natural-fibonacci >>>>> > >>>>> > Could you please check if that is because opentheory packages got >>>>> > updated >>>>> > but the int files haven't? >>>>> > >>>>> > Thanks a lot. >>>>> > >>>>> > >>>>> > -- >>>>> > >>>>> > Regards, >>>>> > Robert >>>>> > >>>>> > New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> >>>>> > New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> >>>>> > Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 >>>>> > >>>>> > >>>>> > _______________________________________________ >>>>> > opentheory-users mailing list >>>>> > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>>>> > <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >>>>> > >>>>> >>>>> _______________________________________________ >>>>> opentheory-users mailing list >>>>> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>>>> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >>>> >>>> >>>> >>>> >>>> -- >>>> >>>> Regards, >>>> Robert >>>> >>>> New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> >>>> New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> >>>> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 >>>> >>> >>> >>> >>> -- >>> >>> Regards, >>> Robert >>> >>> New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> >>> New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> >>> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 >>> >> >> >> >> -- >> >> Regards, >> Robert >> >> New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> >> New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> >> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 >> > > > > -- > > Regards, > Robert > > New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> > New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> > Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 > > > _______________________________________________ > opentheory-users mailing list > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> > <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> > _______________________________________________ opentheory-users mailing list <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> </div></div></blockquote></div> <div> </div>-- <div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div> </div><div>Regards,</div><div>Robert </div><div> </div><div>New homepage at Github: <a href="https://airobert.github.io/" target="_blank">https://airobert.github.io/</a> </div><div>New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl" style="font-size:12.8px" target="_blank">shuai.wang@student.uva.nl</a> </div><div>Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 </div><div> </div></div></div></div></div></div></div></div></div></div></div></div> </div>