[opentheory-users] Error loading articles

[Robert White]

Dear Joe,

I still get one error from the modular package:

Exception:

Failure

 "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)".

Is there any package missing?

I have loaded the following packages:

stream

probability

natural-bits

natural-divides

natural-prime


Thanks very much!


Regards,

Robert

On 5 October 2015 at 23:27, Robert White <ai.robert.wangshuai at gmail.com>
wrote:

> 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
>
>


-- 

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/20151006/a8d81342/attachment-0001.html>