[CakeML-dev] Basis library strings
S.A.Owens at kent.ac.uk
Mon Mar 27 08:29:14 UTC 2017
> 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.
More information about the Developers