[opentheory-users] Question about Lazy-list

[Robert White]

Dear Ramana (and Joe as cc-ed),

We found the error and I have manged to update Holide2 and it turned out
that there was an unbounded type variable somewhere in the proof (not from
the conclusion, but from something like EQ_MP). Now that this is manged by
the new version of Holide, all the existing packages are verified by
Holide2+Dedukti.

Yappy!

Regards,
Robert

On 9 June 2015 at 15:23, Robert White <ai.robert.wangshuai at gmail.com> wrote:

> 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]
>
>


-- 

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/20150705/b2095f19/attachment.html>