[CakeML-dev] Basis library strings

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Mon Mar 27 08:32:29 UTC 2017


If you can build candle/standard/semantics and candle/standard/ml_kernel
then I think you're done.

On 27 Mar 2017 10:29, "Scott Owens" <S.A.Owens at kent.ac.uk> wrote:

>
> > On 2017/03/27, at 04:31, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> >
> > On 26 Mar 2017 23:40, "Scott Owens" <S.A.Owens at kent.ac.uk> wrote:
> > I’m looking at the String.compare function and wanting to add a String.<
> function, for mlstrings.
> >
> > It appears that string_lt is defined in terms of string_lt for HOL
> strings at the end of the file, and some stuff is proved about it. However,
> the definition won’t lead to good code (if it is even translatable at all).
> It also doesn’t look like these theorems are used anywhere. Furthermore, it
> doesn’t like anything is proved about String.compare, other than side
> conditions for the translator.
> >
> > Is all of the above true? If so, then I’d like get rid of the existing
> string_lt and instead define it in terms of compare, and try to prove some
> theorems about them.
> >
> > I would bet that at least one of string_lt or String.compare are used in
> the Candle kernel. I'm all for you reworking things as long as you also fix
> Candle if necessary.
>
> Which directory do I run Holmake in to build Candle?
>
> > At a higher level, I’m not sure who is working on the basis library,
> what its status is, and what future plans there are for it. I’m starting to
> need to use bits of it somewhat seriously, and finding that it isn’t really
> ready for that.
> >
> > Currently I think nobody is working on it. The status is that various
> modules and functions within them are defined and verified but there's
> certainly more work to be done in cleaning some things up and adding more
> functionality. It makes sense for some of that work to be done on an as
> needed basis and it would be great to have your help.
>
> Ok. Then I’ll not be too shy about changing/improving things.
>
> Scott
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170327/a52a5082/attachment-0001.html>


More information about the Developers mailing list