[opentheory-users] Question about Lazy-list

[Robert White]

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 <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. ]
>>>> [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. ]
>> [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 <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. ]
[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/20150608/f550f1a0/attachment.html>