[opentheory-users] Error loading articles

Robert White ai.robert.wangshuai at gmail.com
Tue Oct 6 21:08:05 UTC 2015
Previous message: [opentheory-users] Error loading articles
Next message: [opentheory-users] Error loading articles
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151006/a8100a1b/attachment-0001.html>
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