<div dir="ltr">Dear Joe,<div> </div><div>Okay, please let me know when it's ready.</div><div> </div><div>Thanks</div><div>Robert</div></div><div class="gmail_extra"> <div class="gmail_quote">On 6 October 2015 at 23:09, 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">No, but you should shortly be able to download a new version of the opentheory tool that will fix it. Cheers, Joe On Tue, Oct 6, 2015 at 2:08 PM, Robert White <div class="HOEnZb"><div class="h5"><<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: >> 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. > > So looks like i can't do anything for now on it? > > > > On 6 October 2015 at 23:04, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: >> >> 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 >> <<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> > > > > > -- > > 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>