[opentheory-users] Importing proofs of version 6

[Joe Leslie-Hurd]

Hi Robert,

Perhaps a more realistic case study would be to import a new theory
from the OpenTheory repo:

http://opentheory.gilith.com/

For example,

opentheory install natural-divides
opentheory info --article -o natural-divides.art natural-divides

and then import this article file?

Cheers,

Joe

On Fri, Jun 5, 2015 at 10:04 AM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> Hi Joe,
>
> At the moment I am only trying to load the old proofs. but if I don't change
> the hol.ml file there will be conflict then. So seems the only solution is
> that I completely comment out the rest of the files loaded in hol.ml if so?
>
> No, I don't have new theories so far.
> Regards,
> Robert
>
> On 5 June 2015 at 19:00, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>
>> 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]
>> >
>
>
>
>
> --
>
> 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]
>