[opentheory-users] Importing proofs of version 6

[Joe Leslie-Hurd]

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