From mboxrd@z Thu Jan 1 00:00:00 1970 From: Brett Gilio Subject: Re: [Proposal] The Formal Methods in GNU Guix Working Group Date: Fri, 27 Dec 2019 20:55:00 -0600 Message-ID: <87imm1qhvf.fsf@gnu.org> References: <87tv616q5s.fsf@posteo.net> <1D33E23C-E6D6-4410-AAEF-75FE64A1E785@lepiller.eu> <87o8vtcofu.fsf@gnu.org> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Return-path: Received: from eggs.gnu.org ([2001:470:142:3::10]:60107) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1il2Fw-0004Zi-Vq for guix-devel@gnu.org; Fri, 27 Dec 2019 21:55:09 -0500 In-Reply-To: <87o8vtcofu.fsf@gnu.org> ("Ludovic \=\?utf-8\?Q\?Court\=C3\=A8s\=22'\?\= \=\?utf-8\?Q\?s\?\= message of "Sat, 28 Dec 2019 00:56:53 +0100") List-Id: "Development of GNU Guix and the GNU System distribution." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-devel-bounces+gcggd-guix-devel=m.gmane.org@gnu.org Sender: "Guix-devel" To: Ludovic =?utf-8?Q?Court=C3=A8s?= Cc: guix-devel@gnu.org Ludovic Court=C3=A8s writes: > Hi! > > Julien Lepiller skribis: > >> I'm afraid OCaml is not bootstrappable. It uses a bytecode version of >> itself (using a bootstrapped bytecode interpreter written in C) to >> build itself. Fortunately this situation is being worked on by a phd >> student of Xavier Leroy (and nixOS user) :). >> >> The plan is to write a compiler in C or Scheme (it currently exists, >> but is written in OCaml) for "miniML" a small subset of the OCaml >> language. Then, there is already an interpreter in miniML able to >> interpret the OCaml compiler compiling itself. Once the miniML >> compiler is bootstrapped, we will have a path from C to OCaml :) > > Do you have pointers to this work? > > Hannes of MirageOS also mentioned it at the Reproducible Builds Summit. > It sounds exciting! > > Ludo=E2=80=99. > I am also interested in this. MirageOS has a long lineage of making sensible decisions in their development aside from just designing their unikernel. So i'd really like to see if this becomes a possible bridge from C or Scheme to a bootstrappable OCaml. For what I wonder, I think this is something a formal methods community in Guix would be able to contribute to so we see to it that GNU Guix has a good foundation for making OCaml properly bootstrappable. --=20 Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]