[opentheory-users] Importing proofs of version 6

[Robert White]

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]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150605/ee759ef0/attachment.html>