[CakeML-dev] Using multiple basis modules

[Scott Owens]

Thanks for fixing this. We definitely need to be able to export and use the basis functions :) 

Scott

> On 2017/03/26, at 06: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
> 
>