[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[bug#38605] [WIP MLton 0/1] Add MLton
From: |
zimoun |
Subject: |
[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 <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
- [bug#38605] [WIP MLton 0/1] Add MLton, Brett Gilio, 2019/12/13
- [bug#38605] [WIP MLton 1/1] gnu: Add mlton., Brett Gilio, 2019/12/13
- [bug#38605] [WIP MLton 0/1] Add MLton, Ludovic Courtès, 2019/12/14
- [bug#38605] [WIP MLton 0/1] Add MLton, Brett Gilio, 2019/12/15
- [bug#38605] [WIP MLton 0/1] Add MLton, Ludovic Courtès, 2019/12/16
- [bug#38605] [WIP MLton 0/1] Add MLton, zimoun, 2019/12/16
- [bug#38605] [WIP MLton 0/1] Add MLton, Ludovic Courtès, 2019/12/16
- [bug#38605] [WIP MLton 0/1] Add MLton, Brett Gilio, 2019/12/16
- [bug#38605] [WIP MLton 0/1] Add MLton,
zimoun <=
- [bug#38605] [WIP MLton 0/1] Add MLton, Ludovic Courtès, 2019/12/18
- [bug#38605] [WIP MLton 0/1] Add MLton, Brett Gilio, 2019/12/20