[opentheory-users] Error loading articles

Robert White ai.robert.wangshuai at gmail.com
Tue Oct 6 21:22:36 UTC 2015
Previous message: [opentheory-users] Error loading articles
Next message: [opentheory-users] Error loading articles
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Dear Joe,

Okay, please let me know when it's ready.

Thanks
Robert

On 6 October 2015 at 23:09, Joe Leslie-Hurd <joe at gilith.com> wrote:

> 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
> >
>
> _______________________________________________
> 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/4474ca7f/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