[opentheory-users] Error in importing

[Joe Leslie-Hurd]

Hi Robert,

In the latest version of the OpenTheory HOL Light fork I think it is
the case that hol.ml now loads all the theorems that are exported to
the standard theory library:

# length (Export.list_the_exported_thms ());;
val it : int = 1214

which is the same as the number of theorems in base.

Cheers,

Joe

On Mon, Jun 8, 2015 at 11:57 AM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> So thanks a lot in advance.
>
> It would be nice to see all of them got included.
>
> Cheers
> Robert
>
> On 8 June 2015 at 20:46, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>
>> Hi Robert,
>>
>> Your question on hol-info boils down to the following: is every
>> theorem in the standard theory library included from basics.ml to
>> realax.ml?
>>
>> And I think right now the answer is no, but I'll work on fixing that.
>>
>> Cheers,
>>
>> Joe
>>
>> On Mon, Jun 8, 2015 at 10:30 AM, Robert White
>> <ai.robert.wangshuai at gmail.com> wrote:
>> > 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 (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]
>