<div dir="ltr">Hi Joe,<div><br></div><div>At the moment I am only trying to load the old proofs. but if I don't change the <a href="http://hol.ml">hol.ml</a> file there will be conflict then. So seems the only solution is that I completely comment out the rest of the files loaded in <a href="http://hol.ml">hol.ml</a> if so?</div><div><br></div><div>No, I don't have new theories so far. </div><div>Regards,</div><div>Robert </div></div><div class="gmail_extra"><br><div class="gmail_quote">On 5 June 2015 at 19:00, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Robert,<br>
<br>
You are using it correctly. The intent of the import facility is to<br>
extend the current logical context by bringing in a new theory, not to<br>
change the current logical context. The error that you are redefining<br>
the T constant is an indication that you are trying to change the<br>
current logical context.<br>
<br>
What is your eventual goal using the OpenTheory importer in HOL Light?<br>
I assume you have some new theories you want to import that are not<br>
already in HOL Light.<br>
<br>
Cheers,<br>
<br>
Joe<br>
<br>
<br>
On Fri, Jun 5, 2015 at 5:44 AM, Robert White<br>
<div class="HOEnZb"><div class="h5"><<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote:<br>
> Dear Joe,<br>
><br>
> I am wondering if I am using it correctly. I would like to load some thm in<br>
> and do some proof checking and proof optimisation. However, after loading<br>
> the <a href="http://hol.ml" target="_blank">hol.ml</a> and then do<br>
> let all = import_article "../../laholide/opentheory/bool.art";;<br>
> I get errors saying I am redefining constants. For instance, the bool.art<br>
> file:<br>
><br>
> # let all = import_article "../../laholide/opentheory/bool.art";;<br>
> Exception:<br>
> Failure<br>
>  "in article ../../laholide/opentheory/bool.art at line 89:<br>
> defineConst\nstack = [Term; \"Data.Bool.T\"; Thm]\nnew_constant: constant T<br>
> has already been declared".<br>
><br>
> I could solve the problem by either not loading some of the files in HOL, so<br>
> constants won't be redefined, or try to detect the problems that are defined<br>
> but going to be redefined the same way. I would you solve the problem for<br>
> the OpenTheory version of HOL.<br>
><br>
> Thanks<br>
> Regards,<br>
> Robert<br>
><br>
><br>
> On 5 June 2015 at 08:38, Robert White <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote:<br>
>><br>
>> Thanks Joe!<br>
>><br>
>> I will have to do some more test. I will let you know if I find any bug.<br>
>><br>
>> Regards,<br>
>> Robert<br>
>><br>
>> On 5 June 2015 at 04:55, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:<br>
>>><br>
>>> Robert and I have updated the HOL Light importer to work with version<br>
>>> 6 articles, which is now available from<br>
>>><br>
>>> <a href="http://src.gilith.com/hol-light.html" target="_blank">http://src.gilith.com/hol-light.html</a><br>
>>><br>
>>> It is very lightly tested at this point, so it may well be buggy. I<br>
>>> was able to read in the standard theory library as a version 6<br>
>>> article, which I generated using the command<br>
>>><br>
>>> opentheory info --article -o base.art base<br>
>>><br>
>>> but I didn't even look closely at the results.<br>
>>><br>
>>> Cheers,<br>
>>><br>
>>> Joe<br>
>>><br>
>>><br>
>>> On Wed, Jun 3, 2015 at 2:12 PM, Robert White<br>
>>> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote:<br>
>>> > Thanks for the reply.<br>
>>> ><br>
>>> > I would like to give it a try so I choose option 3 for now. I will use<br>
>>> > option 1 to continue my project alongside.<br>
>>> ><br>
>>> > Regards,<br>
>>> > Robert<br>
>>> ><br>
>>> > On 3 June 2015 at 22:46, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:<br>
>>> >><br>
>>> >> Hi Robert,<br>
>>> >><br>
>>> >> Unfortunately I have not yet updated the import capability in my HOL<br>
>>> >> Light fork to work with version 6 theories. You can either:<br>
>>> >><br>
>>> >> 1. Use the command I showed you before to convert version 6 articles<br>
>>> >> to version 5 before importing them.<br>
>>> >> 2. Wait for me to implement this functionality.<br>
>>> >> 3. Implement it yourself and send me a pull request.<br>
>>> >><br>
>>> >> Please let me know what you decide: it may affect the wait time in<br>
>>> >> solution 2 :-)<br>
>>> >><br>
>>> >> Cheers,<br>
>>> >><br>
>>> >> Joe<br>
>>> >><br>
>>> >> On Wed, Jun 3, 2015 at 7:58 AM, Robert White<br>
>>> >> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote:<br>
>>> >> > Dear Joe,<br>
>>> >> ><br>
>>> >> > I noticed that I can't using import for the current version (version<br>
>>> >> > 6).<br>
>>> >> > I<br>
>>> >> > am using the one from:<br>
>>> >> ><br>
>>> >> > git clone <a href="http://src.gilith.com/hol-light" target="_blank">http://src.gilith.com/hol-light</a><br>
>>> >> ><br>
>>> >> ><br>
>>> >> > I wonder if you have implemented it/updated the <a href="http://import.ml" target="_blank">import.ml</a> file, so I<br>
>>> >> > won't<br>
>>> >> > have to redo your work.<br>
>>> >> ><br>
>>> >> ><br>
>>> >> > Thanks<br>
>>> >> ><br>
>>> >> > Robert<br>
>>> >> ><br>
>>> >> ><br>
>>> ><br>
>>> ><br>
>>> ><br>
>>> ><br>
>>> > --<br>
>>> ><br>
>>> > Regards,<br>
>>> > Robert White (Shuai Wang)<br>
>>> > INRIA Deducteam<br>
>><br>
>><br>
>><br>
>><br>
>> --<br>
>><br>
>> Regards,<br>
>> Robert White (Shuai Wang)<br>
>> INRIA Deducteam<br>
>> [Moving to ILLC of UvA from this Sep. ]<br>
>> [New email address will be <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a>]<br>
>><br>
><br>
><br>
><br>
> --<br>
><br>
> Regards,<br>
> Robert White (Shuai Wang)<br>
> INRIA Deducteam<br>
> [Moving to ILLC of UvA from this Sep. ]<br>
> [New email address will be <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a>]<br>
><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><br></div><div>Regards,</div><div><a href="http://www.dptinfo.ens-cachan.fr/~swang/" target="_blank">Robert White </a>(Shuai Wang)</div><div><a href="https://www.rocq.inria.fr/deducteam/" target="_blank">INRIA Deducteam</a></div><div>[Moving to ILLC of UvA from this Sep. ]</div><div>[New email address will be <a href="mailto:shuai.wang@student.uva.nl" target="_blank">shuai.wang@student.uva.nl</a>]</div><div><br></div></div></div></div></div></div></div></div></div></div></div>
</div>