GNU bug report logs - #38605
[WIP MLton 0/1] Add MLton

Previous Next

Full log

Message #29 received at 38605 <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: Brett Gilio <brettg <at> posteo.net>
Cc: Ludovic Courtès <ludo <at> gnu.org>,
 Amin Bandali <bandali <at> gnu.org>, 38605 <at> debbugs.gnu.org
Subject: Re: [bug#38605] [WIP MLton 0/1] Add MLton
Date: Tue, 17 Dec 2019 17:42:51 +0100

Hi Brett,

Thank you for the explanations.

On Tue, 17 Dec 2019 at 03:21, Brett Gilio <brettg <at> posteo.net> 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

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.