[opentheory-users] Error loading articles

[Joe Leslie-Hurd]

Hi Robert,

modular is a parametric theory, which means it expects to be imported
in a context where there is a natural number constant called modular
already defined, having the property that ~(modular = 0). The
modular-witness theory defines a suitable signature, to show it is not
inconsistent:

$ opentheory info --theory modular-witness
3 external type operators: -> bool natural
9 external constants: = ! /\ ==> ~ F T suc zero
8 satisfied assumptions: hidden
1 defined constant: modulus
1 theorem:
  |- ~(modulus = 0)

For testing you could simply import the modular-witness theory before
modular, to create a valid context.

Cheers,

Joe

On Tue, Oct 6, 2015 at 3:15 AM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> 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
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>