[opentheory-users] What's behind the article merging function

[Robert White]

Dear Joe,

Looks like there is again a problem with the number of proofs we have:
# List.length (list_the_exported_thms ());;
val it : int = 1231
# List.length (search[]);;
val it : int = 1686

Could you please update them also?
Thanks a lot.
Robert

On 13 July 2015 at 23:44, Robert White <ai.robert.wangshuai at gmail.com>
wrote:

> Thanks a lot Joe,
>
> I will merge it up :)
>
> Robert
>
> On 13 July 2015 at 23:06, Joe Leslie-Hurd <joe at gilith.com> wrote:
>
>> Hi Robert,
>>
>> If you pull the most recent version of the OpenTheory HOL Light fork,
>> you can use
>>
>> list_the_exported_thms ();;
>>
>> to show a list of exported theorems together with the theory they were
>> exported to (i.e., the argument to logfile).
>>
>> Hopefully that's the information you require.
>>
>> Cheers,
>>
>> Joe
>>
>> On Fri, Jul 10, 2015 at 12:55 AM, Robert White
>> <ai.robert.wangshuai at gmail.com> wrote:
>> > Dear Joe,
>> > Thanks for the reply.
>> >
>> > Yeah, such a function would be helpful
>> >
>> > Regards
>> > Robert
>> >
>> > On Jul 9, 2015 8:35 PM, "Joe Leslie-Hurd" <joe at gilith.com> wrote:
>> >>
>> >> Hi Robert,
>> >>
>> >> Whenever an article is generated, it is normalized so that if a type
>> >> or term is used multiple times then it is built once, saved in a
>> >> dictionary, and then pulled out when needed. For theorems this is
>> >> taken even further, so that theorems that are alpha-equivalent are
>> >> only constructed once.
>> >>
>> >> I'm afraid there's currently no infrastructure for recording which
>> >> article file a theorem was exported to in HOL Light. It probably
>> >> wouldn't be too hard to add, though, if you needed the information.
>> >>
>> >> Cheers,
>> >>
>> >> Joe
>> >>
>> >>
>> >> On Thu, Jul 9, 2015 at 5:12 AM, Robert White
>> >> <ai.robert.wangshuai at gmail.com> wrote:
>> >> > Dear Joe,
>> >> >
>> >> > I wonder what's behind OpenTheory when it's merging two or more
>> article
>> >> > files together. Is there any optimization?
>> >> >
>> >> > By the way, for HOL Light, is there any function I can tell which
>> thm is
>> >> > in
>> >> > which article file after exporting?
>> >> >
>> >> >
>> >> > Thanks a lot!
>> >> >
>> >> > --
>> >> >
>> >> > Regards,
>> >> > Robert White (Shuai Wang)
>> >> > INRIA Deducteam
>> >> > [Moving to ILLC of UvA from this Sep to continue my masters. ]
>> >> > [New email address will be shuai.wang at student.uva.nl]
>> >> >
>> >> >
>> >> > _______________________________________________
>> >> > 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
>> >
>> >
>> > _______________________________________________
>> > 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 White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
> INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
> [Moving to ILLC of UvA from this Sep to continue my masters. ]
> [New email address will be shuai.wang at student.uva.nl]
>
>


-- 

Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
[Moving to ILLC of UvA from this Sep to continue my masters. ]
[New email address will be shuai.wang at student.uva.nl]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150714/bce3be07/attachment-0001.html>