[opentheory-users] Error loading articles
Joe Leslie-Hurd
joe at gilith.com
Fri Oct 9 07:43:14 UTC 2015
Hi Robert,
I've worked a little more on the HOL Light import, so now all you need
to do is the following:
# logfile "test-import";;
val it : unit = ()
# import_theory "word10";;
auto-importing theory stream
auto-importing theory probability
auto-importing theory natural-bits
auto-importing theory natural-divides
importing theory word10
val it : thm list * thm list = ...
# imported_theories ();;
val it : string list =
["base"; "stream"; "probability"; "natural-bits"; "natural-divides";
"word10"]
Under the covers it calls the opentheory tool to recursively import
all the required theories, extends the interpretation for the new
theory, converts the theory into an article with cleared local symbol
names, and finally reads the article into HOL Light.
Hopefully this should make things a little easier.
Cheers,
Joe
On Thu, Oct 8, 2015 at 1:05 AM, Joe Leslie-Hurd <joe at gilith.com> wrote:
> Hi Robert,
>
> I've just released a new version of the opentheory tool with a new
> option that should solve the name clashing problem when importing into
> HOL Light. Here's how you use it:
>
> opentheory info --clear-local-names --article -o parser.art parser
>
> This replaces the names of all symbols that are local to the theory
> with the special empty name (which prints as _). You can see this with
> the following command:
>
> $ opentheory info --symbols parser.art
> 7 external type operators: -> bool Data.List.list Data.Option.option
> Data.Pair.* Data.Sum.+ Number.Natural.natural
> 46 external constants: = select ! /\ ==> ? ?! \/ ~ cond F T Data.List.::
> Data.List.@ Data.List.[] Data.List.concat Data.List.length Data.List.map
> Data.Option.case.none.some Data.Option.map Data.Option.none
> Data.Option.some Data.Pair., Data.Pair.fst Data.Pair.snd
> Data.Sum.case.left.right Data.Sum.left Data.Sum.right Function.const
> Function.o Function.surjective Number.Natural.* Number.Natural.+
> Number.Natural.- Number.Natural.< Number.Natural.<= Number.Natural.^
> Number.Natural.bit0 Number.Natural.bit1 Number.Natural.even
> Number.Natural.suc Number.Natural.zero Relation.irreflexive
> Relation.measure Relation.subrelation Relation.wellFounded
> 3 defined type operators: _ Parser.parser Parser.Stream.stream
> 59 defined constants: _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
> Parser.any Parser.apply Parser.dest Parser.filter Parser.fold
> Parser.fold.prs Parser.foldN Parser.invariant Parser.inverse Parser.map
> Parser.mapPartial Parser.mapPartial.prs Parser.mk Parser.none
> Parser.orelse Parser.orelse.prs Parser.pair Parser.parse Parser.sequence
> Parser.sequence.prs Parser.some Parser.strongInverse Parser.token
> Parser.token.prs Parser.Stream.append Parser.Stream.case.error.eof.cons
> Parser.Stream.cons Parser.Stream.eof Parser.Stream.error
> Parser.Stream.fromList Parser.Stream.isProperSuffix
> Parser.Stream.isSuffix Parser.Stream.length Parser.Stream.map
> Parser.Stream.toList
>
> Here you can see there is one occurrence of a local type operator and
> many occurrences of local constants. Local symbols are defined and
> used internally in the theory but do not appear in any exported
> theorem (or assumption).
>
> It was local symbols that were causing name clashes when importing
> theories into HOL Light. I have updated the import mechanism so that
> fresh symbol names are generated when an empty name is encountered.
> You will need to execute a git pull of the OpenTheory HOL Light fork
> to get this update.
>
> The parser theory now imports without issue, and word10 theory imports
> without needing the extra extend_the_interpretation commands
> beforehand.
>
> Please give the new HOL Light import flow a try and let me know of any
> problems. It was a bit trickier than expected getting it all to work,
> so it wouldn't surprise me if there were issues.
>
> Cheers,
>
> Joe
>
> On Tue, Oct 6, 2015 at 2:22 PM, Robert White
> <ai.robert.wangshuai at gmail.com> wrote:
>> 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
>>
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
More information about the opentheory-users
mailing list