[opentheory-users] Error loading articles

[Joe Leslie-Hurd]

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
>