[CakeML-dev] Using multiple basis modules

[Ramana Kumar]

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