[bug#38605] [WIP MLton 0/1] Add MLton

[zimoun]

Hi Brett,

Thank you for the explanations.

On Tue, 17 Dec 2019 at 03:21, Brett Gilio <address@hidden> wrote:

> I may be misspeaking, but I think CakeML is formally verified in HOL
> which bootstraps against PolyML or SMLnj, and also requires MLton. So
> the issue of cyclic binary-derived bootstrapping remains an issue. This

I have not checked myself and if I understand well your point: CakeML
requires one PolyML binary to bootstrap (see Bootstrapping locally in
[1] which points to [2]). And this PolyML binary is not small and
requires other not-so-small binaries to be produced. And I am not
talking about the HOL part. So their claim that CakeML bootstraps
really depends on how is defined "bootstrap". :-)


[1] https://cakeml.org/download.html
[2] https://github.com/CakeML/cakeml/blob/master/build-instructions.sh


> is where I think Amin Bandali (CC) and I's idea of writing a C-based
> boostrapping compiler and dedicating it to the GNU project would be
> really valuable.

Yes, for sure a clean path from a reduced set of small binaries to a
full ML compiler would be really great! Challenging project. :-)



All the best,
simon