<div dir="ltr">Dear Joe,<div><br></div><div>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 <a href="http://hol.ml">hol.ml</a> and then do </div><div>let all = import_article "../../laholide/opentheory/bool.art";; </div><div>I get errors saying I am redefining constants. For instance, the bool.art file:</div><div><br></div><div><div># let all = import_article "../../laholide/opentheory/bool.art";;</div><div>Exception:</div><div>Failure</div><div> "in article ../../laholide/opentheory/bool.art at line 89: defineConst\nstack = [Term; \"Data.Bool.T\"; Thm]\nnew_constant: constant T has already been declared".</div></div><div><br></div><div>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. </div><div><br></div><div>Thanks</div><div>Regards,</div><div>Robert</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 5 June 2015 at 08:38, Robert White <span dir="ltr"><<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">ai.robert.wangshuai@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Thanks Joe!<div><br></div><div>I will have to do some more test. I will let you know if I find any bug.</div><div><br></div><div>Regards,</div><div>Robert</div></div><div class="gmail_extra"><div><div class="h5"><br><div class="gmail_quote">On 5 June 2015 at 04:55, 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">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>
<div><div><br>
<br>
On Wed, Jun 3, 2015 at 2:12 PM, Robert White<br>
<<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">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" target="_blank">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" target="_blank">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 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>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br></div></div><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div class="h5"><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></div><span class=""><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></span></div></div></div></div></div></div></div></div></div></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>