[opentheory-users] Error loading articles

[Joe Leslie-Hurd]

Hi Robert,

The theory lazy-list was contributed by Ramana Kumar. It was exported
from HOL4 but hasn't been kept up to date with the standard theory
library, so in its present state I don't think it can be imported into
HOL Light.

gfp is another parametric theory:

$ opentheory info --theory gfp-witness
3 external type operators: -> bool natural
14 external constants: = ! /\ ==> ~ F T + bit0 bit1 odd prime suc zero
16 satisfied assumptions: hidden
1 defined constant: oddprime
2 theorems:
  |- odd oddprime
  |- prime oddprime

So follow the same pattern as modular.

Cheers,

Joe

On Tue, Oct 6, 2015 at 3:31 AM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> Dear Joe,
>
> I also have problem loading lazy-list and gfp:
>
> For lazy-list :
>
> Exception:
>
> Failure
>
>  "in article lazy-list.art at line 234: const\nstack =
> [\"Data.Option.NONE\"; Var; Term; Term; Term; Var; Term; Term; Var; Term;
> Var; \"llist.lrep_ok\"; Var; Term; Term; [\"A\"]; \"llist.llist.rep\";
> \"llist.llist.abs\"; \"llist.llist\"; \"a0\"; \"llist.LFINITE\"; Var; Thm;
> Thm]\nunknown constant \"Data.Option.NONE\"".
>
>
> For gfp;
>
>
> Exception:
>
> Failure
>
>  "in article gfp.art at line 676: axiom\nstack = [Term; []; Thm; Thm;
> Thm]\nunknown assumption:\n|- prime oddprime".
>
>
> Could you please help on that? Thanks a lot!
>
> Regards
>
> Robert
>
>
>
>
>
> On 6 October 2015 at 12:15, 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
>>
>
>
>
> --
>
> 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
>