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

[Joe Leslie-Hurd]

Hi Robert,

On the one hand list_the_exported_thms () is a record of every theorem
that was exported to opentheory using an export_thm command.

On the other hand search [] is a record of every theorem that was
bound to an Ocaml top-level identifier using let thm_name = ...;;;

So even though there will be a large overlap between the two, there's
really no reason that they should be the same.

Cheers,

Joe

On Tue, Jul 14, 2015 at 4:37 AM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> 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 (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]
>>
>
>
>
> --
>
> 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
>