[opentheory-users] Importing proofs of version 6

[Joe Leslie-Hurd]

Hi Robert,

You are using it correctly. The intent of the import facility is to
extend the current logical context by bringing in a new theory, not to
change the current logical context. The error that you are redefining
the T constant is an indication that you are trying to change the
current logical context.

What is your eventual goal using the OpenTheory importer in HOL Light?
I assume you have some new theories you want to import that are not
already in HOL Light.

Cheers,

Joe


On Fri, Jun 5, 2015 at 5:44 AM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> Dear Joe,
>
> I am wondering if I am using it correctly. I would like to load some thm in
> and do some proof checking and proof optimisation. However, after loading
> the hol.ml and then do
> let all = import_article "../../laholide/opentheory/bool.art";;
> I get errors saying I am redefining constants. For instance, the bool.art
> file:
>
> # let all = import_article "../../laholide/opentheory/bool.art";;
> Exception:
> Failure
>  "in article ../../laholide/opentheory/bool.art at line 89:
> defineConst\nstack = [Term; \"Data.Bool.T\"; Thm]\nnew_constant: constant T
> has already been declared".
>
> I could solve the problem by either not loading some of the files in HOL, so
> constants won't be redefined, or try to detect the problems that are defined
> but going to be redefined the same way. I would you solve the problem for
> the OpenTheory version of HOL.
>
> Thanks
> Regards,
> Robert
>
>
> On 5 June 2015 at 08:38, Robert White <ai.robert.wangshuai at gmail.com> wrote:
>>
>> Thanks Joe!
>>
>> I will have to do some more test. I will let you know if I find any bug.
>>
>> Regards,
>> Robert
>>
>> On 5 June 2015 at 04:55, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>>
>>> Robert and I have updated the HOL Light importer to work with version
>>> 6 articles, which is now available from
>>>
>>> http://src.gilith.com/hol-light.html
>>>
>>> It is very lightly tested at this point, so it may well be buggy. I
>>> was able to read in the standard theory library as a version 6
>>> article, which I generated using the command
>>>
>>> opentheory info --article -o base.art base
>>>
>>> but I didn't even look closely at the results.
>>>
>>> Cheers,
>>>
>>> Joe
>>>
>>>
>>> On Wed, Jun 3, 2015 at 2:12 PM, Robert White
>>> <ai.robert.wangshuai at gmail.com> wrote:
>>> > Thanks for the reply.
>>> >
>>> > I would like to give it a try so I choose option 3 for now. I will use
>>> > option 1 to continue my project alongside.
>>> >
>>> > Regards,
>>> > Robert
>>> >
>>> > On 3 June 2015 at 22:46, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>> >>
>>> >> Hi Robert,
>>> >>
>>> >> Unfortunately I have not yet updated the import capability in my HOL
>>> >> Light fork to work with version 6 theories. You can either:
>>> >>
>>> >> 1. Use the command I showed you before to convert version 6 articles
>>> >> to version 5 before importing them.
>>> >> 2. Wait for me to implement this functionality.
>>> >> 3. Implement it yourself and send me a pull request.
>>> >>
>>> >> Please let me know what you decide: it may affect the wait time in
>>> >> solution 2 :-)
>>> >>
>>> >> Cheers,
>>> >>
>>> >> Joe
>>> >>
>>> >> On Wed, Jun 3, 2015 at 7:58 AM, Robert White
>>> >> <ai.robert.wangshuai at gmail.com> wrote:
>>> >> > Dear Joe,
>>> >> >
>>> >> > I noticed that I can't using import for the current version (version
>>> >> > 6).
>>> >> > I
>>> >> > am using the one from:
>>> >> >
>>> >> > git clone http://src.gilith.com/hol-light
>>> >> >
>>> >> >
>>> >> > I wonder if you have implemented it/updated the import.ml file, so I
>>> >> > won't
>>> >> > have to redo your work.
>>> >> >
>>> >> >
>>> >> > Thanks
>>> >> >
>>> >> > Robert
>>> >> >
>>> >> >
>>> >
>>> >
>>> >
>>> >
>>> > --
>>> >
>>> > Regards,
>>> > Robert White (Shuai Wang)
>>> > INRIA Deducteam
>>
>>
>>
>>
>> --
>>
>> Regards,
>> Robert White (Shuai Wang)
>> INRIA Deducteam
>> [Moving to ILLC of UvA from this Sep. ]
>> [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. ]
> [New email address will be shuai.wang at student.uva.nl]
>