[opentheory-users] Error loading articles

Joe Leslie-Hurd joe at gilith.com
Tue Oct 6 21:04:12 UTC 2015
Previous message: [opentheory-users] Error loading articles
Next message: [opentheory-users] Error loading articles
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Hi Robert,

This is a case of a theory-local definition clashing with an existing
definition of the same name. It will be solved by the same change that
I'm working on that will make the extra extend_the_interpretation
commands unnecessary.

Cheers,

Joe

On Tue, Oct 6, 2015 at 4:00 AM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> Dear Joe,
>
> I also noticed that parser is has the following errors:
>
> Exception:
>
> Failure
>
>  "in article parser.art at line 457: defineConst\nstack = [Term;
> \"HOLLight.NUMSUM\"; Term; Term; Term; Var; Term; Var; Term; Var; Term; Var;
> [[\"HOLLight.NUMLEFT\"; Var]]; Term; Var; Var; Var; Var; \"HOLLight.INJP\";
> \"HOLLight.ZBOT\"; Term; Term; Term; Var; Term; Term; Var; Term; Var;
> \"HOLLight.ZRECSPACE\"; [\"A\"]; \"HOLLight._dest_rec\";
> \"HOLLight._mk_rec\"; \"HOLLight.recspace\"; \"a1\"; Var; [\"A\"];
> \"HOLLight._dest_pstream\"; \"HOLLight._mk_pstream\";
> \"Parser.Stream.stream\"; TypeOp<fun>; TypeOp<fun>; Const<!>;
> Term]\nnew_constant: constant NUMSUM has already been declared".
>
>
> I looked into it and found that NUMSUM has been declared in int_type.ml
> which is  loaded in hol.ml.
>
> Could you please update this package?
>
> Thanks!
>
> Robert
>
>
> On 6 October 2015 at 12:31, 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
>>
>
>
>
> --
>
> 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
>
Previous message: [opentheory-users] Error loading articles
Next message: [opentheory-users] Error loading articles
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
More information about the opentheory-users mailing list