[opentheory-users] Importing proofs of version 6

[Robert White]

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 <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. ]
> [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. ]
[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/20150605/ee21c02d/attachment.html>