[opentheory-users] Error loading articles

Joe Leslie-Hurd joe at gilith.com
Tue Oct 6 21:09:23 UTC 2015
Previous message: [opentheory-users] Error loading articles
Next message: [opentheory-users] Error loading articles
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
No, but you should shortly be able to download a new version of the
opentheory tool that will fix it.

Cheers,

Joe

On Tue, Oct 6, 2015 at 2:08 PM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
>> 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.
>
> So looks like i can't do anything for now on it?
>
>
>
> On 6 October 2015 at 23:04, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>
>> 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
>> >
>>
>> _______________________________________________
>> 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
>
>
> _______________________________________________
> 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