<div dir="ltr"><div><div><div><div><div>Hi Robert,<br><br></div>The article was generated following the instructions at <a href="http://www.gilith.com/research/opentheory/faq.html#export-from-hol4" target="_blank">http://www.gilith.com/research/opentheory/faq.html#export-from-hol4</a> applied to llistScript.sml.<br><br></div>If the article is accepted by the opentheory tool but not by Dedukti, perhaps there is a problem in Holide or in the Dedukti checker?<br><br></div>For debugging maybe you could try exporting only a part of llistScript.sml (by deleting the rest). Or even translating only a small part of the generated llist.art to Dedukti.<br><br></div>Cheers,<br></div>Ramana<br><div class="gmail_extra"><br><div class="gmail_quote">On 8 June 2015 at 16:45, 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">Dear Ramana,<div><br></div><div>I am not sure how to deal with it. Do you have any advice please. I am not familiar with generating / extracting *.art files. Neither debugging though a .art file.</div><div><br></div><div>Thanks</div></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On 8 June 2015 at 17:36, Ramana Kumar <span dir="ltr"><<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</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"><div>The lazy-list package is based on a HOL4 theory of lazy lists, which can be found here: <a href="https://github.com/HOL-Theorem-Prover/HOL/tree/master/src/llist" target="_blank">https://github.com/HOL-Theorem-Prover/HOL/tree/master/src/llist</a>.<br></div></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On 8 June 2015 at 16:33, 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 wait for further updates then.</div><div><br></div><div>Regards,</div><div>Robert</div></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On 8 June 2015 at 17:31, 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>
In terms of the OpenTheory package, you are correct that lazy-list is<br>
monolithic:<br>
<br>
$ opentheory info --theory-source lazy-list<br>
main {<br>
  article: "llist.art"<br>
}<br>
<br>
However, Ramana may be able to dig up source files for the article<br>
that could be restructured into subpackages.<br>
<br>
Cheers,<br>
<br>
Joe<br>
<div><div><br>
On Mon, Jun 8, 2015 at 2:44 AM, Robert White<br>
<<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">ai.robert.wangshuai@gmail.com</a>> wrote:<br>
> Dear Joe and Ramana,<br>
><br>
> I used the new Holide and dedukti for proof checking of the whole Opentheory<br>
> repos. There is one good news and one bad news.<br>
><br>
> The good news is:<br>
><br>
> I have checked through the whole library of the rest apart from lazy-list<br>
> without problems. They all passed the checking.<br>
><br>
> The bad news is:<br>
><br>
> lazy-list didn't pass the check.<br>
><br>
> --------this is the error line by Dedukti --------------------------------<br>
> Processing file 'dedukti/<a href="http://lazy-list.dk" target="_blank">lazy-list.dk</a>'...<br>
> ERROR line:106697 column:149 Cannot find symbol 'lazy_2Dlist.A'.<br>
><br>
> I searched online and found there isn't sub-packages for me to check<br>
> individually. I wonder if this one is just as a big whole file or maybe I<br>
> can somehow unpack it to different files and check through each<br>
> individually.<br>
><br>
> Thanks!<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" target="_blank">shuai.wang@student.uva.nl</a>]<br>
><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div><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>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div><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>
</div></div><br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div></div>