[CakeML-dev] Using multiple basis modules

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Sun Mar 26 05:48:34 UTC 2017


The same problem applies to quicksortProg (which I can fix).

There's also an unbound variable in the definition of sort in sortProg
(namely, "sorted" in "List.app print sorted" is unbound).
I'll leave you to fix that last one Scott, since I'm not sure exactly what
you wanted to do (app the array, or convert it to a list first?).

On 26 March 2017 at 16:31, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:

> Looking at it now, it seems like the problem is that mlarrayProg doesn't
> add hardly any of the Array functions to the ml_progLib state it exports.
> So for example Array.fromList is out of scope because it was never added to
> the basis. I will try adding the ones you're using (I don't know why
> they're not all added... I think I remember Connor saying things were too
> slow?)
>
> On 26 March 2017 at 07:35, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
>
>> Common problems include:
>> - The spec theorem has type variables that need instantiation,
>> - The function is not in scope,
>> - The function is applied to the wrong number of arguments
>>
>> I think the middle one can reduce your goal to false whereas the others
>> can raise exceptions. Does your p variable have 'ffi ffi_proj type?
>>
>> I'll try to have a look at some point. (Currently at AITP.)
>>
>> On 25 Mar 2017 20:09, "Yong Kiam" <tanyongkiam at gmail.com> wrote:
>>
>>> Those tactics are defined in the tactic libs in characteristic/, I fixed
>>> a few issues back on env-refactor by stepping through them.
>>>
>>> On Sat, Mar 25, 2017 at 2:46 PM, Scott Owens <S.A.Owens at kent.ac.uk>
>>> wrote:
>>>
>>>> Ok. I think I have the dependencies right now. However, I still have 4
>>>> cf_apps where xapp and xapp_spec fail, and I have no idea why, or how to
>>>> even start debugging the problem. This is on the sort_example branch,
>>>> characteristic/examples/sortProgScript.sml. Any hints would be greatly
>>>> appreciated.
>>>>
>>>> Scott
>>>>
>>>> > On 2017/03/25, at 02:46, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
>>>> wrote:
>>>> >
>>>> > Add arrays into the same linear sequence that includes I/O and update
>>>> the basis/dependency-order file accordingly.
>>>> >
>>>> > The longer term solution is to get the abstract translator working.
>>>> (There is an issue, and was some discussion on a wiki page.)
>>>> >
>>>> > On Friday, 24 March 2017, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
>>>> > > I’m trying to verify a program with CF that uses both arrays and
>>>> I/O from the basis. I don’t see how to make this work, since you only seem
>>>> to be able to do 1 translation_extends. Any ideas?
>>>> > >
>>>> > > Scott
>>>> > > _______________________________________________
>>>> > > Developers mailing list
>>>> > > Developers at cakeml.org
>>>> > > https://lists.cakeml.org/listinfo/developers
>>>> > >
>>>>
>>>> _______________________________________________
>>>> Developers mailing list
>>>> Developers at cakeml.org
>>>> https://lists.cakeml.org/listinfo/developers
>>>>
>>>
>>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170326/f6486198/attachment.html>


More information about the Developers mailing list