[opentheory-users] Question about Lazy-list

[Joe Leslie-Hurd]

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
>