[opentheory-users] Error in importing

[Robert White]

Hi Joe,

Thanks. That's what I need for now.

Regards,
Robert

On 8 June 2015 at 19:12, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Robert,
>
> This is every theorem th from basics.ml to realax.ml for which there was
> a call
>
> export_thm th;;
>
> which means that the theorem is part of the standard theory library.
>
> Cheers,
>
> Joe
>
> On Mon, Jun 8, 2015 at 9:50 AM, Robert White
> <ai.robert.wangshuai at gmail.com> wrote:
> > Hello again.
> >
> > One more question:
> >
> > These are the thms exported as a result of loading hol.ml?
> >
> > So am I right to say that these are the thms from basics.ml to relax.ml
> > (according to the order in hol.ml)?
> >
> > Thanks.
> >
> > Regards,
> > Robert
> >
> >
> > On 8 June 2015 at 18:47, Robert White <ai.robert.wangshuai at gmail.com>
> wrote:
> >>
> >> Dear Joe,
> >>
> >> Thanks very much!
> >>
> >> It is really helpful.
> >>
> >> Thanks a lot for your help :)
> >>
> >> Regards,
> >> Robert
> >>
> >> On 8 June 2015 at 18:13, Joe Leslie-Hurd <joe at gilith.com> wrote:
> >>>
> >>> Hi Robert,
> >>>
> >>> If you do a pull I've added a function that will list every exported
> >>> theorem, so you can do:
> >>>
> >>> #use "hol.ml";;
> >>> Export.list_the_exported_thms ();;
> >>>
> >>> Please let me know if that gives you what you need.
> >>>
> >>> Cheers,
> >>>
> >>> Joe
> >>>
> >>> On Mon, Jun 8, 2015 at 8:50 AM, Robert White
> >>> <ai.robert.wangshuai at gmail.com> wrote:
> >>> > Dear Joe,
> >>> >
> >>> > I need to do some checking and proofs of these proofs. so Logically
> >>> > using
> >>> > these proofs directly is a good thing but I can't find a "list" I can
> >>> > simply
> >>> > use. So I was trying to load from the .art files.
> >>> >
> >>> > Do you know if there is any way to get a list of these thms? If so
> then
> >>> > the
> >>> > problem is solved.
> >>> >
> >>> > Thanks
> >>> > Robert
> >>> >
> >>> >
> >>> >
> >>> > On 8 June 2015 at 17:45, Joe Leslie-Hurd <joe at gilith.com> wrote:
> >>> >>
> >>> >> Hi Robert,
> >>> >>
> >>> >> Did you have a specific reason for wanting to load the standard
> theory
> >>> >> library into HOL Light? You could regard this as already being
> loaded
> >>> >> when you execute
> >>> >>
> >>> >> #use "hol.ml";;
> >>> >>
> >>> >> It would be possible to reload articles from the standard theory
> into
> >>> >> HOL Light with some changes to import.ml, but right now I can't
> see a
> >>> >> use-case for it.
> >>> >>
> >>> >> Cheers,
> >>> >>
> >>> >> Joe
> >>> >>
> >>> >> On Mon, Jun 8, 2015 at 8:35 AM, Robert White
> >>> >> <ai.robert.wangshuai at gmail.com> wrote:
> >>> >> > Dear Joe,
> >>> >> >
> >>> >> > Okay, looks I have no way to load the others for now then.
> >>> >> > I will just play with these three first.
> >>> >> >
> >>> >> > Thanks again for your advice.
> >>> >> >
> >>> >> > Regards,
> >>> >> > Rob
> >>> >> >
> >>> >> > On 8 June 2015 at 17:27, Joe Leslie-Hurd <joe at gilith.com> wrote:
> >>> >> >>
> >>> >> >> Hi Robert,
> >>> >> >>
> >>> >> >> The theories that are causing you errors are part of the standard
> >>> >> >> theory library:
> >>> >> >>
> >>> >> >> $ opentheory list 'Includes base'
> >>> >> >> bool-1.36
> >>> >> >> function-1.55
> >>> >> >> list-1.103
> >>> >> >> natural-1.104
> >>> >> >> option-1.72
> >>> >> >> pair-1.27
> >>> >> >> real-1.61
> >>> >> >> relation-1.60
> >>> >> >> set-1.71
> >>> >> >> sum-1.61
> >>> >> >> unit-1.20
> >>> >> >>
> >>> >> >> Since HOL Light already implements the standard theory library,
> >>> >> >> trying
> >>> >> >> to reload it will generate errors about defining symbols, as you
> >>> >> >> have
> >>> >> >> experienced.
> >>> >> >>
> >>> >> >> My advice is to focus on theories that are not part of the
> standard
> >>> >> >> theory library, the easiest to obtain being those on the
> OpenTheory
> >>> >> >> repo:
> >>> >> >>
> >>> >> >> http://opentheory.gilith.com/packages/
> >>> >> >>
> >>> >> >> Cheers,
> >>> >> >>
> >>> >> >> Joe
> >>> >> >>
> >>> >> >> On Mon, Jun 8, 2015 at 4:34 AM, Robert White
> >>> >> >> <ai.robert.wangshuai at gmail.com> wrote:
> >>> >> >> > Dear Joe,
> >>> >> >> >
> >>> >> >> > Hello. I have the following errors:
> >>> >> >> >
> >>> >> >> > # extend_the_interpretation
> >>> >> >> > "opentheory/theories/list/list.int";;
> >>> >> >> > val it : unit = ()
> >>> >> >> > # let all= import_article "opentheory/articles/list.art";;
> >>> >> >> > Exception:
> >>> >> >> > Failure
> >>> >> >> >  "in article opentheory/articles/list.art at line 467:
> >>> >> >> > 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_list\"; \"HOLLight._mk_list\";
> >>> >> >> > \"Data.List.list\";
> >>> >> >> > TypeOp<fun>; \"NULL\"; \"Data.List.null\"; Var; [];
> >>> >> >> > Thm]\nnew_constant:
> >>> >> >> > constant NUMSUM has already been declared".
> >>> >> >> >
> >>> >> >> > # let all= import_article "opentheory/articles/sum.art";;
> >>> >> >> > Exception:
> >>> >> >> > Failure
> >>> >> >> >  "in article opentheory/articles/sum.art at line 499:
> >>> >> >> > 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\"; Type; TypeOp<fun>;
> >>> >> >> > \"_15483\";
> >>> >> >> > Var; Var; \"HOLLight.CONSTR\"; Var; [\"A\"; \"B\"];
> >>> >> >> > \"HOLLight._dest_sum\";
> >>> >> >> > \"HOLLight._mk_sum\"; \"Data.Sum.+\"; TypeOp<fun>; \"ISL\";
> >>> >> >> > \"Data.Sum.isLeft\"; Var; []; Var; Thm; Thm]\nnew_constant:
> >>> >> >> > constant
> >>> >> >> > NUMSUM
> >>> >> >> > has already been declared".
> >>> >> >> >
> >>> >> >> >
> >>> >> >> > # extend_the_interpretation
> >>> >> >> > "opentheory/theories/bool/bool.int";;
> >>> >> >> > Exception:
> >>> >> >> > Sys_error "opentheory/theories/bool/bool.int: No such file or
> >>> >> >> > directory".
> >>> >> >> >
> >>> >> >> > # extend_the_interpretation
> >>> >> >> > "opentheory/theories/bool/bool.int";;
> >>> >> >> > Exception:
> >>> >> >> > Sys_error "opentheory/theories/bool/bool.int: No such file or
> >>> >> >> > directory".
> >>> >> >> > # let all= import_article "opentheory/articles/bool.art";;
> >>> >> >> > Exception:
> >>> >> >> > Failure
> >>> >> >> >  "in article opentheory/articles/bool.art at line 89:
> >>> >> >> > defineConst\nstack
> >>> >> >> > =
> >>> >> >> > [Term; \"Data.Bool.T\"; Thm]\nnew_constant: constant T has
> >>> >> >> > already
> >>> >> >> > been
> >>> >> >> > declared".
> >>> >> >> >
> >>> >> >> >
> >>> >> >> >
> >>> >> >> > # let all= import_article "opentheory/articles/real.art";;
> >>> >> >> > Exception:
> >>> >> >> > Failure
> >>> >> >> >  "in article opentheory/articles/real.art at line 283:
> >>> >> >> > defineConst\nstack =
> >>> >> >> > [Term; \"HOLLight.is_nadd\"; [[]; [[Var; Term]]]; [[]; [[Var;
> >>> >> >> > Term]]];
> >>> >> >> > [];
> >>> >> >> > \"HOLLight.dest_nadd\"; \"HOLLight.mk_nadd\";
> \"HOLLight.nadd\";
> >>> >> >> > TypeOp<fun>; \"s\"; []; \"HOLLight.dest_hreal\";
> >>> >> >> > \"HOLLight.mk_hreal\";
> >>> >> >> > \"HOLLight.hreal\"; TypeOp<prod>; TypeOp<fun>; TypeOp<fun>;
> >>> >> >> > Const<!>]\nnew_constant: constant is_nadd has already been
> >>> >> >> > declared".
> >>> >> >> >
> >>> >> >> >
> >>> >> >> > # let all= import_article "opentheory/articles/option.art";;
> >>> >> >> > Exception:
> >>> >> >> > Failure
> >>> >> >> >  "in article opentheory/articles/option.art at line 478:
> >>> >> >> > 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\"; Type; TypeOp<fun>;
> >>> >> >> > \"_15483\";
> >>> >> >> > Var; Var; \"HOLLight.CONSTR\"; Var; [\"A\"];
> >>> >> >> > \"HOLLight._dest_option\";
> >>> >> >> > \"HOLLight._mk_option\"; \"Data.Option.option\"; TypeOp<fun>;
> >>> >> >> > \"is_none\";
> >>> >> >> > \"Data.Option.isNone\"; Var; []; Thm]\nnew_constant: constant
> >>> >> >> > NUMSUM
> >>> >> >> > has
> >>> >> >> > already been declared".
> >>> >> >> >
> >>> >> >> >
> >>> >> >> >
> >>> >> >> > So far I have only the three ones you showed in previous email
> >>> >> >> > working.
> >>> >> >> > :
> >>> >> >> > "natural-divides.art", "stream.art" and "natural-prime.art"
> >>> >> >> >
> >>> >> >> > I wonder how I should load the rest.
> >>> >> >> >
> >>> >> >> > Thanks a lot.
> >>> >> >> > --
> >>> >> >> >
> >>> >> >> > Regards,
> >>> >> >> > Robert White (Shuai Wang)
> >>> >> >> > INRIA Deducteam
> >>> >> >> > [Moving to ILLC of UvA from this Sep. ]
> >>> >> >> > [New email address will be shuai.wang at student.uva.nl]
> >>> >> >> >
> >>> >> >
> >>> >> >
> >>> >> >
> >>> >> >
> >>> >> > --
> >>> >> >
> >>> >> > Regards,
> >>> >> > Robert White (Shuai Wang)
> >>> >> > INRIA Deducteam
> >>> >> > [Moving to ILLC of UvA from this Sep. ]
> >>> >> > [New email address will be shuai.wang at student.uva.nl]
> >>> >> >
> >>> >
> >>> >
> >>> >
> >>> >
> >>> > --
> >>> >
> >>> > Regards,
> >>> > Robert White (Shuai Wang)
> >>> > INRIA Deducteam
> >>> > [Moving to ILLC of UvA from this Sep. ]
> >>> > [New email address will be shuai.wang at student.uva.nl]
> >>> >
> >>
> >>
> >>
> >>
> >> --
> >>
> >> Regards,
> >> Robert White (Shuai Wang)
> >> INRIA Deducteam
> >> [Moving to ILLC of UvA from this Sep. ]
> >> [New email address will be shuai.wang at student.uva.nl]
> >>
> >
> >
> >
> > --
> >
> > Regards,
> > Robert White (Shuai Wang)
> > INRIA Deducteam
> > [Moving to ILLC of UvA from this Sep. ]
> > [New email address will be shuai.wang at student.uva.nl]
> >
>



-- 

Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
[Moving to ILLC of UvA from this Sep. ]
[New email address will be shuai.wang at student.uva.nl]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150608/5aa19705/attachment-0001.html>