[opentheory-users] Error loading articles
Joe Leslie-Hurd
joe at gilith.com
Thu Oct 8 08:05:19 UTC 2015
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