<div dir="ltr">Dear Joe,<div><br></div><div>I also noticed that parser is has the following errors:</div><div><br></div><div>







<p class=""><span class="">Exception:</span></p>
<p class=""><span class="">Failure</span></p>
<p class=""><span class=""> "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".</span></p><p class=""><span class=""><br></span></p><p class=""><span class="">I looked into it and found that NUMSUM has been declared in <a href="http://int_type.ml">int_type.ml</a> which is  loaded in <a href="http://hol.ml">hol.ml</a>. </span></p><p class=""><span class="">Could you please update this package?</span></p><p class=""><span class="">Thanks!</span></p><p class=""><span class="">Robert</span></p></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 6 October 2015 at 12:31, Robert White <span dir="ltr"><<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">ai.robert.wangshuai@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Dear Joe,<div><br></div><div>I also have problem loading lazy-list and gfp:</div><div><br></div><div>For lazy-list :</div><div><br></div><div>







<p><span>Exception:</span></p>
<p><span>Failure</span></p>
<p><span> "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\"".</span></p><p><span><br></span></p><p><span>For gfp;</span></p><p><span><br></span></p><p><span>Exception:</span></p><p><span>Failure</span></p><p><span>









</span></p><p><span> "in article gfp.art at line 676: axiom\nstack = [Term; []; Thm; Thm; Thm]\nunknown assumption:\n|- prime oddprime".</span></p><p><span><br></span></p><p><span>Could you please help on that? Thanks a lot!</span></p><p><span>Regards</span></p><span class="HOEnZb"><font color="#888888"><p><span>Robert</span></p><p><span><br></span></p><p><span><br></span></p></font></span></div><div><br></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 6 October 2015 at 12:15, Robert White <span dir="ltr"><<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">ai.robert.wangshuai@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Dear Joe,<div><br></div><div>I still get one error from the modular package:</div><div>







<p><span>Exception:</span></p>
<p><span>Failure</span></p>
<p><span> "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)".</span></p><p>Is there any package missing?</p><p>I have loaded the following packages:</p><p>stream<br></p><p>probability<br></p><p>natural-bits<br></p><p>natural-divides<br></p><p>natural-prime<br></p><p><br></p><p>Thanks very much!</p><p><br></p><p>Regards,</p><p>Robert</p></div></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On 5 October 2015 at 23:27, Robert White <span dir="ltr"><<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">ai.robert.wangshuai@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Thanks very much Joe. <div>I also noticed that there is kind of dependency going on but I don't know how to fix it.<div><br></div></div></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On 5 October 2015 at 22:56, 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">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 it's<br>
unreasonable to expect people to discover this information. I'll work<br>
on fixing it so these multiple extend_the_interpretation commands are<br>
unnecessary.<br>
<br>
Cheers,<br>
<br>
Joe<br>
<div><div><br>
On Sun, Oct 4, 2015 at 2:57 PM, Robert White<br>
<<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">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>; 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 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" target="_blank">shuai.wang@student.uva.nl</a><br>
> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901<br>
><br>
><br>
</div></div>> _______________________________________________<br>
> opentheory-users mailing list<br>
> <a href="mailto:opentheory-users@gilith.com" target="_blank">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" target="_blank">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>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div><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>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div><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>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div><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>
</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>