From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:45468) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1igcS3-0007hy-Iw for guix-patches@gnu.org; Sun, 15 Dec 2019 17:33:44 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1igcRi-0007XZ-Ke for guix-patches@gnu.org; Sun, 15 Dec 2019 17:33:23 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:59642) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1igcRi-0007WA-F0 for guix-patches@gnu.org; Sun, 15 Dec 2019 17:33:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1igcRi-0002ne-De for guix-patches@gnu.org; Sun, 15 Dec 2019 17:33:02 -0500 Subject: [bug#38605] [WIP MLton 0/1] Add MLton Resent-Message-ID: From: Brett Gilio References: <877e2z7e3x.fsf@posteo.net> <87v9qix001.fsf@gnu.org> Date: Sun, 15 Dec 2019 16:32:31 -0600 In-Reply-To: <87v9qix001.fsf@gnu.org> ("Ludovic \=\?utf-8\?Q\?Court\=C3\=A8s\=22'\?\= \=\?utf-8\?Q\?s\?\= message of "Sat, 14 Dec 2019 18:58:22 +0100") Message-ID: <87y2vd43uo.fsf@posteo.net> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable 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: Ludovic =?UTF-8?Q?Court=C3=A8s?= Cc: 38605@debbugs.gnu.org Ludovic Court=C3=A8s writes: > Hi Brett, > > Brett Gilio skribis: > >> MLton is a little bit tricker to package properly as it runs in to the i= ssue >> of requiring a non-source, pre-compiled bootstrap. There is a way to get= it to >> build against SMLnj though (which will be my next WIP bug report). This = patch >> series uses a series of patched ELFs to compile MLton from source. But o= bviously >> this will not be permissable upstream. > > =E2=80=9CNot permissible=E2=80=9D is strong (in the sense that Guix doesn= =E2=80=99t have such a > strong policy because there are cases where there=E2=80=99s no known way = to > bootstrap from source), but clearly, if there=E2=80=99s a documented way = to > build MLton from source, this is what we should be aiming for. > > Thanks! > > Ludo=E2=80=99. It's a little off of the subject at hand, but to my knowledge (as provided by this issue: https://github.com/MLton/mlton/issues/350) I am going to cherry pick a few things of note. "In general, it has been the position of MLton developers that "build from source" is an unrealistic goal for a self-hosting compiler. While it is possible (albeit, very, very slow) to build MLton using another SML compiler, we are not aware of any other SML compiler that meets the spirit of "build from source" (although some might meet the law). In particular, Poly/ML simply includes pre-built compilers in their source repository (see https://github.com/polyml/polyml/blob/master/Makefile.am#L22 and https://github.com/polyml/polyml/tree/master/imports); admittedly these are (space inefficient) text files rather than binary blobs, but they are hardly artifacts meant for human consumption. Similarly, SML/NJ "builds from source" by downloading pre-built binary bootstrap images. We find the "solution" of MLton building by downloading a pre-built MLton to be satisfactory and both more performant and more robust." As Matthew Fluet notes here, even the PolyML repository has some blobs, though they are not ELF blobs. SMLnj repeats this same behavior. I follow this up with: "Taking from the spirit of what Aaron said in the Debian issue (back in 2003), "I agree. A larger circular dependency is worse than depending on oneself. The only way I could see depending on another SML compiler is if that compiler was written in another language such that no dependency cycle would exist." Perhaps a longer-term goal of mine would be to help accomplish this such that the dependency cycle is indeed broken. I know of projects like https://github.com/thepowersgang/mrustc doing this for the Rust toolchain, and https://www.gnu.org/software/mes/ for bootstrapping a seedless GCC." I wonder if the best long-term solution for melding Guix and the ML language community is to try and write an ML compiler in a language like C or Scheme based on a reduced-sized specification of the language. The reason I say all this is because I would really love to see the philosophies of ML/Formal Methods/Proof and the deterministic/functional philosophy of Guix work together. They seem naturally synergistic, but there seems be a difference in history here that is making this quite antagonistic. I'd really like to spark some insight and discussion here because it would be amazing if the formal methods community (like Coq, seL4, HOL/Isabelle, etc.) could really begin to benefit from the Guix model. Sorry for the extra long message. Thanks! --=20 Brett M. Gilio Homepage -- https://scm.pw/ GNU Guix -- https://guix.gnu.org/