<div dir="ltr">Dear Joe and Ramana,<div><br></div><div>It looks like we have a small problem on our side (very hard to notice). Both versions of Holide failed. We are trying to fix this bug. Will let you know how it goes. </div><div>Thanks</div><div>Regards,</div><div>Robert</div></div><div class="gmail_extra"><br><div class="gmail_quote">On 8 June 2015 at 18:17, 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">It is possibly helpful to note that every prefix of a valid article is<br> a valid article (as long as you break at a newline), so if you need a<br> smaller testcase you could delete everything after some newline in<br> llist.art.<br> <br> Cheers,<br> <br> Joe<br> <br> On Mon, Jun 8, 2015 at 9:13 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> > Thanks for the link.<br> ><br> >> If the article is accepted by the opentheory tool but not by Dedukti,<br> >> perhaps there is a problem in Holide or in the Dedukti checker?<br> ><br> > I have also been diving into it on my side to see where the problem could<br> > be.<br> ><br> > Thanks for your advice. I will try that.<br> ><br> > Regards,<br> > Robert<br> ><br> > On 8 June 2015 at 17:58, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote:<br> >><br> >> Hi Robert,<br> >><br> >> The article was generated following the instructions at<br> >> <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<br> >> to llistScript.sml.<br> >><br> >> If the article is accepted by the opentheory tool but not by Dedukti,<br> >> perhaps there is a problem in Holide or in the Dedukti checker?<br> >><br> >> For debugging maybe you could try exporting only a part of llistScript.sml<br> >> (by deleting the rest). Or even translating only a small part of the<br> >> generated llist.art to Dedukti.<br> >><br> >> Cheers,<br> >> Ramana<br> >><br> >> On 8 June 2015 at 16:45, Robert White <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>><br> >> wrote:<br> >>><br> >>> Dear Ramana,<br> >>><br> >>> I am not sure how to deal with it. Do you have any advice please. I am<br> >>> not familiar with generating / extracting *.art files. Neither debugging<br> >>> though a .art file.<br> >>><br> >>> Thanks<br> >>><br> >>> On 8 June 2015 at 17:36, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote:<br> >>>><br> >>>> The lazy-list package is based on a HOL4 theory of lazy lists, which can<br> >>>> be found here:<br> >>>> <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> >>>><br> >>>> On 8 June 2015 at 16:33, Robert White <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>><br> >>>> wrote:<br> >>>>><br> >>>>> Thanks Joe,<br> >>>>><br> >>>>> I will wait for further updates then.<br> >>>>><br> >>>>> Regards,<br> >>>>> Robert<br> >>>>><br> >>>>> On 8 June 2015 at 17:31, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:<br> >>>>>><br> >>>>>> 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> >>>>>><br> >>>>>> On Mon, Jun 8, 2015 at 2:44 AM, Robert White<br> >>>>>> <<a href="mailto:ai.robert.wangshuai@gmail.com">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<br> >>>>>> > 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<br> >>>>>> > 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> >>>>>> > --------------------------------<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<br> >>>>>> > 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">shuai.wang@student.uva.nl</a>]<br> >>>>>> ><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> >>><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> >>> opentheory-users mailing list<br> >>> <a href="mailto:opentheory-users@gilith.com">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> >><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> > opentheory-users mailing list<br> > <a href="mailto:opentheory-users@gilith.com">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> <br> _______________________________________________<br> opentheory-users mailing list<br> <a href="mailto:opentheory-users@gilith.com">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> </div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><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 <span style="font-size:small">to continue my masters</span><span style="font-size:12.8000001907349px">. ]</span></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>