<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 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 class="h5"><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>; 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">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">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>
</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>