From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:53620) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ihFx7-0004OT-Tu for guix-patches@gnu.org; Tue, 17 Dec 2019 11:44:07 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ihFx5-0006w1-KH for guix-patches@gnu.org; Tue, 17 Dec 2019 11:44:05 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:36345) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ihFx4-0006sV-Bj for guix-patches@gnu.org; Tue, 17 Dec 2019 11:44:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ihFx4-0003ML-9u for guix-patches@gnu.org; Tue, 17 Dec 2019 11:44:02 -0500 Subject: [bug#38605] [WIP MLton 0/1] Add MLton Resent-Message-ID: MIME-Version: 1.0 References: <877e2z7e3x.fsf@posteo.net> <87v9qix001.fsf@gnu.org> <87y2vd43uo.fsf@posteo.net> <87tv60k2pw.fsf@gnu.org> <87k16wdkx0.fsf@gnu.org> <878snbzo8y.fsf@posteo.net> In-Reply-To: <878snbzo8y.fsf@posteo.net> From: zimoun Date: Tue, 17 Dec 2019 17:42:51 +0100 Message-ID: Content-Type: text/plain; charset="UTF-8" List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: Brett Gilio Cc: Ludovic =?UTF-8?Q?Court=C3=A8s?= , Amin Bandali , 38605@debbugs.gnu.org Hi Brett, Thank you for the explanations. On Tue, 17 Dec 2019 at 03:21, Brett Gilio 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