[opentheory-users] Importing proofs of version 6

[Robert White]

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 <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/79ea4c66/attachment.html>