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