[opentheory-users] Error loading articles

[Robert White]

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 <joe at gilith.com> 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/natural-divides.int";;
> import_article "natural-divides.art";;
>
> extend_the_interpretation
>   "opentheory/theories/stream/stream.int";;
> import_article "stream.art";;
>
> extend_the_interpretation
>   "opentheory/theories/natural-prime/natural-prime.int";;
> 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/stream.int";;
> import_article "stream.art";;
>
> extend_the_interpretation
>   "opentheory/theories/probability/probability.int";;
> import_article "probability.art";;
>
> extend_the_interpretation
>   "opentheory/theories/natural-bits/natural-bits.int";;
> import_article "natural-bits.art";;
>
> extend_the_interpretation
>   "opentheory/theories/natural-divides/natural-divides.int";;
> import_article "natural-divides.art";;
>
> extend_the_interpretation
>   "opentheory/theories/modular/modular.int";;
> extend_the_interpretation
>   "opentheory/theories/word/word.int";;
> extend_the_interpretation
>   "opentheory/theories/word10/word10.int";;
> 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
> <ai.robert.wangshuai at gmail.com> 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: https://airobert.github.io/
> > New email address at ILLC: shuai.wang at student.uva.nl
> > Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901
> >
> >
> > _______________________________________________
> > opentheory-users mailing list
> > opentheory-users at gilith.com
> > http://www.gilith.com/opentheory/mailing-list
> >
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>



-- 

Regards,
Robert

New homepage at Github: https://airobert.github.io/
New email address at ILLC: shuai.wang at student.uva.nl
Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151005/8a71932e/attachment.html>