[opentheory-users] Error loading articles

Joe Leslie-Hurd joe at gilith.com
Tue Oct 27 03:04:16 UTC 2015
Previous message: [opentheory-users] Error loading articles
Next message: [opentheory-users] Error loading articles
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Hi Robert,

I have worked a little more on the HOL Light/OpenTheory interface, and
now include the HOL Light names of theorems in the theory packages, in
addition to the HOL Light names of type operators and constants. For
example, the following command results in the theorems in the modular
theory having Ocaml names just like they'd been proved in an
interactive session:

# import_theory "modular";;
auto-imported theory stream : {128} |> {55}
auto-imported theory probability : {39} |> {18}
auto-imported theory natural-bits : {205} |> {210}
auto-imported theory natural-divides : {177} |> {136}
imported sub-theory modular-witness : {8} |> {1}
imported theory modular : {75} |> {68}
val it : Theory.t = modular : {75} |> {68}
# modular_exp_add;;
val it : thm =
  |- !x m n.
         modular_mult (modular_exp x m) (modular_exp x n) =
         modular_exp x (m + n)

I have also added an interpret_theory command to "interpret" a theory
in another context. For example, the following command interprets the
modular theory inside the word theory, renaming the type operators and
constants according to the word-def-modular.int file, and renaming the
theorems by replacing the "modular" with "word" and "modulus" with
"word_size".

# interpret_theory
    {Import.source_theory = "modular";
     Import.interpretation = "opentheory/theories/word/word-def-modular.int";
     Import.theorem_renamer = Import.replace "modular" "word" o
                              Import.replace "modulus" "word_size";
     Import.destination_theory = "word-def"};;
val it : Theory.t = modular : {75} |> {68}
# word_exp_add;;
val it : thm =
  |- !x m n. word_mult (word_exp x m) (word_exp x n) = word_exp x (m + n)

Hopefully this will make it easier to import OpenTheory theories into HOL Light.

Cheers,

Joe

On Fri, Oct 9, 2015 at 12:43 AM, Joe Leslie-Hurd <joe at gilith.com> wrote:
> 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
>>>
Previous message: [opentheory-users] Error loading articles
Next message: [opentheory-users] Error loading articles
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
More information about the opentheory-users mailing list