[CakeML-dev] Using multiple basis modules

Yong Kiam tanyongkiam at gmail.com
Sat Mar 25 19:08:57 UTC 2017


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


More information about the Developers mailing list