[opentheory-users] Question about Lazy-list

[Ramana Kumar]

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150608/1b52a0c8/attachment-0001.html>