[opentheory-users] Question about Lazy-list

[Robert White]

Dear Joe and Ramana,

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.
Thanks
Regards,
Robert

On 8 June 2015 at 18:17, Joe Leslie-Hurd <joe at gilith.com> wrote:

> It is possibly helpful to note that every prefix of a valid article is
> a valid article (as long as you break at a newline), so if you need a
> smaller testcase you could delete everything after some newline in
> llist.art.
>
> Cheers,
>
> Joe
>
> On Mon, Jun 8, 2015 at 9:13 AM, Robert White
> <ai.robert.wangshuai at gmail.com> wrote:
> > Thanks for the link.
> >
> >> 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?
> >
> > I have also been diving into it on my side to see where the problem could
> > be.
> >
> > Thanks for your advice. I will try that.
> >
> > Regards,
> > Robert
> >
> > On 8 June 2015 at 17:58, Ramana Kumar <ramana at member.fsf.org> wrote:
> >>
> >> Hi Robert,
> >>
> >> The article was generated following the instructions at
> >> http://www.gilith.com/research/opentheory/faq.html#export-from-hol4
> applied
> >> to llistScript.sml.
> >>
> >> 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?
> >>
> >> 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.
> >>
> >> Cheers,
> >> Ramana
> >>
> >> On 8 June 2015 at 16:45, Robert White <ai.robert.wangshuai at gmail.com>
> >> wrote:
> >>>
> >>> Dear Ramana,
> >>>
> >>> 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.
> >>>
> >>> Thanks
> >>>
> >>> On 8 June 2015 at 17:36, Ramana Kumar <ramana at member.fsf.org> wrote:
> >>>>
> >>>> The lazy-list package is based on a HOL4 theory of lazy lists, which
> can
> >>>> be found here:
> >>>> https://github.com/HOL-Theorem-Prover/HOL/tree/master/src/llist.
> >>>>
> >>>> On 8 June 2015 at 16:33, Robert White <ai.robert.wangshuai at gmail.com>
> >>>> wrote:
> >>>>>
> >>>>> Thanks Joe,
> >>>>>
> >>>>> I will wait for further updates then.
> >>>>>
> >>>>> Regards,
> >>>>> Robert
> >>>>>
> >>>>> On 8 June 2015 at 17:31, Joe Leslie-Hurd <joe at gilith.com> wrote:
> >>>>>>
> >>>>>> Hi Robert,
> >>>>>>
> >>>>>> In terms of the OpenTheory package, you are correct that lazy-list
> is
> >>>>>> monolithic:
> >>>>>>
> >>>>>> $ opentheory info --theory-source lazy-list
> >>>>>> main {
> >>>>>>   article: "llist.art"
> >>>>>> }
> >>>>>>
> >>>>>> However, Ramana may be able to dig up source files for the article
> >>>>>> that could be restructured into subpackages.
> >>>>>>
> >>>>>> Cheers,
> >>>>>>
> >>>>>> Joe
> >>>>>>
> >>>>>> On Mon, Jun 8, 2015 at 2:44 AM, Robert White
> >>>>>> <ai.robert.wangshuai at gmail.com> wrote:
> >>>>>> > Dear Joe and Ramana,
> >>>>>> >
> >>>>>> > I used the new Holide and dedukti for proof checking of the whole
> >>>>>> > Opentheory
> >>>>>> > repos. There is one good news and one bad news.
> >>>>>> >
> >>>>>> > The good news is:
> >>>>>> >
> >>>>>> > I have checked through the whole library of the rest apart from
> >>>>>> > lazy-list
> >>>>>> > without problems. They all passed the checking.
> >>>>>> >
> >>>>>> > The bad news is:
> >>>>>> >
> >>>>>> > lazy-list didn't pass the check.
> >>>>>> >
> >>>>>> > --------this is the error line by Dedukti
> >>>>>> > --------------------------------
> >>>>>> > Processing file 'dedukti/lazy-list.dk'...
> >>>>>> > ERROR line:106697 column:149 Cannot find symbol 'lazy_2Dlist.A'.
> >>>>>> >
> >>>>>> > I searched online and found there isn't sub-packages for me to
> check
> >>>>>> > individually. I wonder if this one is just as a big whole file or
> >>>>>> > maybe I
> >>>>>> > can somehow unpack it to different files and check through each
> >>>>>> > individually.
> >>>>>> >
> >>>>>> > Thanks!
> >>>>>> > --
> >>>>>> >
> >>>>>> > 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 (Shuai Wang)
> >>> INRIA Deducteam
> >>> [Moving to ILLC of UvA from this Sep. ]
> >>> [New email address will be shuai.wang at student.uva.nl]
> >>>
> >>>
> >>> _______________________________________________
> >>> opentheory-users mailing list
> >>> opentheory-users at gilith.com
> >>> http://www.gilith.com/opentheory/mailing-list
> >>>
> >>
> >
> >
> >
> > --
> >
> > 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]
> >
> >
> > _______________________________________________
> > opentheory-users mailing list
> > opentheory-users at gilith.com
> > http://www.gilith.com/opentheory/mailing-list
> >
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>



-- 

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 to continue my masters. ]
[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/20150609/a255c152/attachment.html>