[opentheory-users] Error in importing

[Joe Leslie-Hurd]

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]
>