From debbugs-submit-bounces@debbugs.gnu.org Fri Dec 13 22:58:23 2019 Received: (at submit) by debbugs.gnu.org; 14 Dec 2019 03:58:23 +0000 Received: from localhost ([127.0.0.1]:34838 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ifyZS-0005bC-P0 for submit@debbugs.gnu.org; Fri, 13 Dec 2019 22:58:22 -0500 Received: from lists.gnu.org ([209.51.188.17]:40058) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ifyZR-0005b2-1g for submit@debbugs.gnu.org; Fri, 13 Dec 2019 22:58:21 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:41251) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ifyZP-0004Jk-Ho for guix-patches@gnu.org; Fri, 13 Dec 2019 22:58:20 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-2.3 required=5.0 tests=BAYES_20,RCVD_IN_DNSWL_MED, URIBL_BLOCKED autolearn=disabled version=3.3.2 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ifyZN-000348-Aq for guix-patches@gnu.org; Fri, 13 Dec 2019 22:58:18 -0500 Received: from mout02.posteo.de ([185.67.36.66]:43857) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1ifyZJ-0002x4-Qq for guix-patches@gnu.org; Fri, 13 Dec 2019 22:58:16 -0500 Received: from submission (posteo.de [89.146.220.130]) by mout02.posteo.de (Postfix) with ESMTPS id 5E0872400E6 for ; Sat, 14 Dec 2019 04:58:12 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.net; s=2017; t=1576295892; bh=Uh7h8Blc4lfrCzeCgON+Y3u3Re/VywaJKzbdwJyCNoM=; h=From:To:Subject:Date:From; b=RmpeHaIBlGYEEI92ktmQ3swx348x+iEY+7v7ZQdBC7jvEKYkO6ACDrBuWsOH8kzOb vOFfvRkMkeEj7mf/BtfANFWH7seoV0SAtQ5AkfR+EWJFWcIrY6YC7Jz20L7gPwvON4 nJNbPtdJ6OUm26HLpYdXxo4DH5/SjY3xO7joj6qqle+lL0w30yB8luaziQd6y4LT8r gVHQvivGFRzy/2sc5AhLA3KGPUQIyt/tqdEMIWY4h49v0RZfW2kClgRkjjEmHMgaQZ QmD6/mryPStlmmEJJpjH3GwR/eEMiwjP1LBnNaHSaOsOr7NrWShUJ7Ox93BuJH2ZCi IS2sokm/IFIpA== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 47ZYfW1ghcz9rxT for ; Sat, 14 Dec 2019 04:58:11 +0100 (CET) From: Brett Gilio To: guix-patches@gnu.org Subject: [WIP MLton 0/1] Add MLton Date: Fri, 13 Dec 2019 21:58:10 -0600 Message-ID: <877e2z7e3x.fsf@posteo.net> MIME-Version: 1.0 Content-Type: text/x-patch Content-Disposition: inline; filename=0000-cover-letter.patch Content-Description: [WIP MLton 0/1] Add MLton X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-Received-From: 185.67.36.66 X-Spam-Score: -1.3 (-) X-Debbugs-Envelope-To: submit X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -2.3 (--) >From d6e94b0a04bf71e51d29b7228bd4233bf763eaaa Mon Sep 17 00:00:00 2001 From: Brett Gilio Date: Fri, 13 Dec 2019 21:54:59 -0600 Subject: [WIP MLton 0/1] Add MLton MLton is a little bit tricker to package properly as it runs in to the issue 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 obviously this will not be permissable upstream. As such I wanted to share my WIP on this for anybody who has any ideas and so I can keep track of my own progress. Please send revisions by re-rolling n+1. Brett Gilio (1): gnu: Add mlton. gnu/packages/sml.scm | 138 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 138 insertions(+) -- 2.24.1 From debbugs-submit-bounces@debbugs.gnu.org Fri Dec 13 22:59:40 2019 Received: (at 38605) by debbugs.gnu.org; 14 Dec 2019 03:59:40 +0000 Received: from localhost ([127.0.0.1]:34844 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ifyai-0005fS-3O for submit@debbugs.gnu.org; Fri, 13 Dec 2019 22:59:40 -0500 Received: from mout01.posteo.de ([185.67.36.65]:46055) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ifyag-0005f8-Aj for 38605@debbugs.gnu.org; Fri, 13 Dec 2019 22:59:39 -0500 Received: from submission (posteo.de [89.146.220.130]) by mout01.posteo.de (Postfix) with ESMTPS id 29FA316005E for <38605@debbugs.gnu.org>; Sat, 14 Dec 2019 04:59:31 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.net; s=2017; t=1576295972; bh=xKpCCJopby1mDxDgPZbWPxSJ2GqnoNNZTIdqrOxQ64A=; h=From:To:Subject:Date:From; b=G0u+yTQbD6PBZWRP4ke273wsPza2uBwN6XI2MpqHHkKCn0hS+td78E1upfoT9NZBG qhqfX5tBZqi4JemdgsbEPhFRr6cVTUTuIcehJXboWGXRXdMN/UPv2lTM/I3zK5OuzZ 48cOdwOzvHUwCpwmygBXglkKLnGkjY6XvVvtUbhL7B8gmwDlq0kbn1FphFRu5sidp7 x8edN9aZf5kMz5DXiqmZSD1vnsZT4M3LmYd2pl9DzBVJAX7nezBjUo42f7kAw6sAq5 zyItl4q9M240LRQUqgv+ctzIzkMxKNzgZM5imFvsbBHz4QEsrtloHBmczuUidPAFaT BCg0zeD/b/buQ== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 47ZYh25LWmz6tmB for <38605@debbugs.gnu.org>; Sat, 14 Dec 2019 04:59:30 +0100 (CET) From: Brett Gilio To: 38605@debbugs.gnu.org Subject: [WIP MLton 1/1] gnu: Add mlton. Date: Fri, 13 Dec 2019 21:59:32 -0600 Message-ID: <874ky37e1n.fsf@posteo.net> MIME-Version: 1.0 Content-Type: text/x-patch Content-Disposition: inline; filename=0001-gnu-Add-mlton.patch Content-Description: [WIP MLton 1/1] gnu: Add mlton. X-Spam-Score: -1.6 (-) X-Debbugs-Envelope-To: 38605 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -2.6 (--) >From d6e94b0a04bf71e51d29b7228bd4233bf763eaaa Mon Sep 17 00:00:00 2001 From: Brett Gilio Date: Fri, 13 Dec 2019 21:54:13 -0600 Subject: [WIP MLton 1/1] gnu: Add mlton. * gnu/packages/sml.scm (mlton-no-gcc): New variable. --- gnu/packages/sml.scm | 138 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 138 insertions(+) diff --git a/gnu/packages/sml.scm b/gnu/packages/sml.scm index 30ee58c498..e45ce4c59c 100644 --- a/gnu/packages/sml.scm +++ b/gnu/packages/sml.scm @@ -75,3 +75,141 @@ function interface, and a symbolic debugger.") (license (list license:lgpl2.1 license:lgpl2.1+)))) + +(define-private mlton-reduced + (package + (name "mlton") + (version "20180207") + (source (origin + (method url-fetch) + (uri (string-append "https://github.com/MLton/" name + "/releases/download/on-" version + "-release/" name "-" version + "-1.amd64-linux.tgz")) + (sha256 + (base32 + "0f4q575yfm5dpg4a2wsnqn4l2zrar96p6rlsk0dw10ggyfwvsjlf")))) + (build-system trivial-build-system) + ;; TODO: The build arguments can be much more programmatic. + (arguments + '(#:modules + ((guix build utils)) + #:builder + (begin + (use-modules (guix build utils)) + (let* + ((out (assoc-ref %outputs "out")) + (source (assoc-ref %build-inputs "source")) + (tar (string-append (assoc-ref %build-inputs "tar") "/bin/tar")) + (patchelf (string-append (assoc-ref %build-inputs "patchelf") "/bin/patchelf")) + (ld (string-append (assoc-ref %build-inputs "glibc") "/lib/ld-linux-x86-64.so.2")) + (gmp (string-append (assoc-ref %build-inputs "gmp") "/lib")) + (bash (string-append (assoc-ref %build-inputs "bash") "/bin/bash")) + (rm (string-append (assoc-ref %build-inputs "coreutils") "/bin/rm")) + (PATH + (string-append + (assoc-ref %build-inputs "gzip") "/bin" + ":" + (assoc-ref %build-inputs "tar") "/bin"))) + (mkdir-p out) + (mkdir-p (string-append out "/bin")) + (with-directory-excursion out + (setenv "PATH" PATH) + (system* tar "xf" source "--strip-components=1") + ;; PATCHES FOR /LIB/MLTON/MLTON-COMPILE + (system* patchelf + "--set-interpreter" + ld + (string-append out "/lib/mlton/mlton-compile")) + (system* patchelf + "--set-rpath" + gmp + (string-append out "/lib/mlton/mlton-compile")) + ;; PATCHES FOR /BIN/MLLEX + (system* patchelf + "--set-interpreter" + ld + (string-append out "/bin/mllex")) + (system* patchelf + "--set-rpath" + gmp + (string-append out "/bin/mllex")) + ;; PATCHES FOR /BIN/MLYACC + (system* patchelf + "--set-interpreter" + ld + (string-append out "/bin/mlyacc")) + (system* patchelf + "--set-rpath" + gmp + (string-append out "/bin/mlyacc")) + ;; DELETE ALL UNNEEDED COMPONENTS + (system* rm "-rf" + "bin/mlprof" + "bin/mlnlffigen" + "LICENSE" + "Makefile" + "CHANGELOG.adoc" + "README.adoc" + "share") + ;; PATCH SHEBANG FOR BIN/MLTON + (substitute* "bin/mlton" + (("/usr/bin/env bash") + bash))))))) + (native-inputs `(("glibc" ,glibc) + ("patchelf" ,patchelf) + ("tar" ,tar) + ("bash" ,bash) + ("coreutils" ,coreutils) + ("gzip" ,gzip) + ("gmp" ,gmp))) + (supported-systems '("x86_64-linux")) + (synopsis #f) + (description #f) + (home-page #f) + (license #f))) + +(define-public mlton-no-gcc + (package + (name "mlton-no-gcc") + (version "20180207") + (source (origin + (method url-fetch) + (uri (string-append "https://github.com/MLton/" name + "/archive/on-" version + "-release.tar.gz")) + (sha256 + (base32 + "1l1flhxx8hr4n3mf87m02231r3m2f3sh28zfxma3g41jscmj21zi")))) + (build-system gnu-build-system) + (arguments + `(#:parallel-build? #f ; See: https://github.com/MLton/mlton/issues/348 + #:phases + (modify-phases %standard-phases + (delete 'configure) + (replace 'install + (lambda _ + (invoke "make" + (string-append "PREFIX=" (assoc-ref %outputs "out")) + "install")))))) + (native-inputs + `(("mlton" ,mlton-reduced) + ("which" ,which))) + (propagated-inputs + `(("gmp" ,gmp))) + (supported-systems '("x86_64-linux")) + (synopsis "Whole-program, optimizing Standard ML compiler") + (description "MLton is a whole-program optimizing compiler for Standard ML. +MLton generates standalone executables with excellent runtime performance, is +SML '97 compliant, and has a complete basis library. MLton has source-level +profiling, a fast C FFI, an interface to the GNU multiprecision library, and +lots of useful libraries.") + (home-page "http://mlton.org/") + (license license:hpnd))) + +(define-public mlton + (package (inherit mlton-no-gcc) + (name "mlton") + (propagated-inputs + `(("gcc-toolchain" ,gcc-toolchain) + ,@(package-propagated-inputs mlton-no-gcc))))) -- 2.24.1 From debbugs-submit-bounces@debbugs.gnu.org Sat Dec 14 17:43:33 2019 Received: (at 38605) by debbugs.gnu.org; 14 Dec 2019 22:43:33 +0000 Received: from localhost ([127.0.0.1]:35842 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1igG8L-0005kG-Ha for submit@debbugs.gnu.org; Sat, 14 Dec 2019 17:43:33 -0500 Received: from eggs.gnu.org ([209.51.188.92]:32852) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1igG8J-0005jm-3O for 38605@debbugs.gnu.org; Sat, 14 Dec 2019 17:43:31 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:36422) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1igG8D-00080R-PU; Sat, 14 Dec 2019 17:43:25 -0500 Received: from [2a01:e0a:1d:7270:af76:b9b:ca24:c465] (port=38026 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1igBgP-00040a-DJ; Sat, 14 Dec 2019 12:58:26 -0500 From: =?utf-8?Q?Ludovic_Court=C3=A8s?= To: Brett Gilio Subject: Re: [bug#38605] [WIP MLton 0/1] Add MLton References: <877e2z7e3x.fsf@posteo.net> Date: Sat, 14 Dec 2019 18:58:22 +0100 In-Reply-To: <877e2z7e3x.fsf@posteo.net> (Brett Gilio's message of "Fri, 13 Dec 2019 21:58:10 -0600") Message-ID: <87v9qix001.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 38605 Cc: 38605@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) Hi Brett, Brett Gilio skribis: > MLton is a little bit tricker to package properly as it runs in to the is= sue > 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 p= atch > series uses a series of patched ELFs to compile MLton from source. But ob= viously > 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. From debbugs-submit-bounces@debbugs.gnu.org Sun Dec 15 17:32:40 2019 Received: (at 38605) by debbugs.gnu.org; 15 Dec 2019 22:32:40 +0000 Received: from localhost ([127.0.0.1]:37381 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1igcRM-0002mv-03 for submit@debbugs.gnu.org; Sun, 15 Dec 2019 17:32:40 -0500 Received: from mout02.posteo.de ([185.67.36.66]:57495) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1igcRJ-0002mh-DS for 38605@debbugs.gnu.org; Sun, 15 Dec 2019 17:32:38 -0500 Received: from submission (posteo.de [89.146.220.130]) by mout02.posteo.de (Postfix) with ESMTPS id 683682400FF for <38605@debbugs.gnu.org>; Sun, 15 Dec 2019 23:32:31 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.net; s=2017; t=1576449151; bh=5EhXvJdiGVa8MbHglPs2eyDxBJLSsdM1Wx8KV7uzW8Y=; h=From:To:Cc:Subject:Date:From; b=TtKZbFOscYMJpZIpo9wf2oP0F+l9ZRpLXgSS041bMN2fnVY3dw0kfI5+yrZZLyNQ3 uazdXne4o8AoyBMpJs8jagIkJAwhUCZY/aTLMAT6Q0KyOXO32YNps6rg27JFTCDcS/ eTKtx/dNwyRwPgfpXMUuG/VbStRib4rcyK7okNW9D5AOZ156sT9cBNAvKPpImvnfG8 EboPH1Muepm4lwda0xoZpzpVpGsxlhkAQyRhO/q/Lj3yOBabyjFNlkQVSRmqslw0nt VIOM1TP4KvsvgndbYWIdqipdVTfDKup+ar6Z+mVmUQI+FU+XAbuPpt79kuypJPmiCE yni6wzT543gnQ== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 47bfKn6hbJz9rxL; Sun, 15 Dec 2019 23:32:29 +0100 (CET) From: Brett Gilio To: Ludovic =?utf-8?Q?Court=C3=A8s?= Subject: Re: [bug#38605] [WIP MLton 0/1] Add MLton 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> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 38605 Cc: 38605@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) 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/ From debbugs-submit-bounces@debbugs.gnu.org Mon Dec 16 05:02:46 2019 Received: (at 38605) by debbugs.gnu.org; 16 Dec 2019 10:02:46 +0000 Received: from localhost ([127.0.0.1]:37925 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ignDC-0005Tm-DQ for submit@debbugs.gnu.org; Mon, 16 Dec 2019 05:02:46 -0500 Received: from eggs.gnu.org ([209.51.188.92]:34037) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ignDA-0005TY-16 for 38605@debbugs.gnu.org; Mon, 16 Dec 2019 05:02:45 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:56281) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ignD4-0003jV-7M; Mon, 16 Dec 2019 05:02:38 -0500 Received: from [2001:660:6102:320:e120:2c8f:8909:cdfe] (port=53286 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ignD3-00031W-Gf; Mon, 16 Dec 2019 05:02:37 -0500 From: =?utf-8?Q?Ludovic_Court=C3=A8s?= To: Brett Gilio Subject: Re: [bug#38605] [WIP MLton 0/1] Add MLton References: <877e2z7e3x.fsf@posteo.net> <87v9qix001.fsf@gnu.org> <87y2vd43uo.fsf@posteo.net> X-URL: http://www.fdn.fr/~lcourtes/ X-Revolutionary-Date: 26 Frimaire an 228 de la =?utf-8?Q?R=C3=A9volution?= X-PGP-Key-ID: 0x090B11993D9AEBB5 X-PGP-Key: http://www.fdn.fr/~lcourtes/ludovic.asc X-PGP-Fingerprint: 3CE4 6455 8A84 FDC6 9DB4 0CFB 090B 1199 3D9A EBB5 X-OS: x86_64-pc-linux-gnu Date: Mon, 16 Dec 2019 11:02:35 +0100 In-Reply-To: <87y2vd43uo.fsf@posteo.net> (Brett Gilio's message of "Sun, 15 Dec 2019 16:32:31 -0600") Message-ID: <87tv60k2pw.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 38605 Cc: 38605@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) Hi Brett, Brett Gilio skribis: > 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. Thanks for discussing it with upstream! Your reply summarizes current =E2=80=9Cbest practices=E2=80=9D pretty well: for Rust, for Guile (which co= ntains an interpreter in C), for Common Lisp (GNU=C2=A0clisp is written in C), for C (MesCC), etc. > 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. I vaguely recall reading about an SML implementation in Scheme. All I could find is a mention of it in . > 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. I agree that the two should be synergistic. Eventually, all this comes down to how to design a programming language or its implementation in a way that allows is to be built incrementally from =E2=80=9Cnothing=E2=80=9D= , or from a different language (something janneke and I discussed at the R-B summit). This sounds very much like programming language research question. Thanks, Ludo=E2=80=99. From debbugs-submit-bounces@debbugs.gnu.org Mon Dec 16 13:53:23 2019 Received: (at 38605) by debbugs.gnu.org; 16 Dec 2019 18:53:24 +0000 Received: from localhost ([127.0.0.1]:40358 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1igvUh-0008VP-GO for submit@debbugs.gnu.org; Mon, 16 Dec 2019 13:53:23 -0500 Received: from mail-qt1-f175.google.com ([209.85.160.175]:33937) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1igvUf-0008V9-VF for 38605@debbugs.gnu.org; Mon, 16 Dec 2019 13:53:22 -0500 Received: by mail-qt1-f175.google.com with SMTP id 5so6626358qtz.1 for <38605@debbugs.gnu.org>; Mon, 16 Dec 2019 10:53:21 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=k8Bo4hXm83aq5VSQZF7OetSd1VBlxzn08F0Du0US3y4=; b=FMDow1Q46yYeQmYNwU3mAmahstau1Q4sxdzTlTMGAhKpnqgX2tBFstAYqhXtDxqmfT FvhcLhuzBus7qXZSNEoklG9g1yOiysOxG40tRjMdNe4/Pn2eP91hmK+xaMm6lLL53lEs Hsfk8G5TTjtJySqzJNq6losI4aYXMx6ZQ+8JehZTwhbhq7tMNm8cyWGEwHqPnXl9VuFl 081d/g4k3TwoidSVzfkUbN+92+Jtn033M3Ze4B292sraBKmS0UNJm/oR0tq8ozSzWdQr /Pq0Hs7P3bqzR55LyrsoSMAXjD+rALsf0a3QFg0AxbKAsXNzM71oA22om5S05lDTLwds AXqA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc:content-transfer-encoding; bh=k8Bo4hXm83aq5VSQZF7OetSd1VBlxzn08F0Du0US3y4=; b=ANLpheH7dJrMjylKERcS+kLLZUhHH4malRQ+aIYE+H6EXx5EPBVr6XyF3X4a6Q8HP3 71J7Y4DtifrNYkN4MKpZc/6gicOdEwGLkjwIKgLwpDHEUg66aOSDZQ8z53KrYEAaBzzu 8MGEHRol79rglmfoWD/MnGevLGseLx0QGImxzp0psU+eP7+czwuzI4Eue7zITqODVOgQ ytvaxb95OVs3L1qPM8GtsNO8xDhh22vVO2BlUHmY8+3N/MD0QL8lAj+qO/leVGjSEGxM zugmcd4ZK8lT9BM3TCM0eVAMpbIkgCvT/Q+wUnfSH3mMWC2iWrt0fEe49bWb2m1qXZUc sMpw== X-Gm-Message-State: APjAAAXAtkPB4PabFpCtchpaGGKI+58w6bkywMuj3WE5JIveawIGpBYY HQOufFysoxqybayg/G+VRaUo1GrSSQ9Scw1ReCk= X-Google-Smtp-Source: APXvYqxXG8X4Ob2VhNEFqpAfhpcFx85K4xj05d/H6kIxuFMNMIetwQ5/5fk+X3P8lSeoqb8jq4l+Oo6n7vWLI1fMOXA= X-Received: by 2002:ac8:73c3:: with SMTP id v3mr677221qtp.211.1576522396362; Mon, 16 Dec 2019 10:53:16 -0800 (PST) MIME-Version: 1.0 References: <877e2z7e3x.fsf@posteo.net> <87v9qix001.fsf@gnu.org> <87y2vd43uo.fsf@posteo.net> <87tv60k2pw.fsf@gnu.org> In-Reply-To: <87tv60k2pw.fsf@gnu.org> From: zimoun Date: Sun, 15 Dec 2019 02:59:47 +0100 Message-ID: Subject: Re: [bug#38605] [WIP MLton 0/1] Add MLton To: =?UTF-8?Q?Ludovic_Court=C3=A8s?= Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Spam-Score: 0.5 (/) X-Debbugs-Envelope-To: 38605 Cc: Brett Gilio , 38605@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.5 (/) Hi, I am -- for sure -- not in topic. :-) On Mon, 16 Dec 2019 at 11:03, Ludovic Court=C3=A8s wrote: > summit). This sounds very much like programming language research > question. To my knowledge, the most advanced ML-family language able to bootstrap (and verified with prover etc.) is CakeML (subset of Standard ML). (And not packaged in Guix, AFAICT.) https://cakeml.org/ All the best, simon From debbugs-submit-bounces@debbugs.gnu.org Mon Dec 16 16:23:50 2019 Received: (at 38605) by debbugs.gnu.org; 16 Dec 2019 21:23:50 +0000 Received: from localhost ([127.0.0.1]:40418 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1igxqI-0004GJ-GF for submit@debbugs.gnu.org; Mon, 16 Dec 2019 16:23:50 -0500 Received: from eggs.gnu.org ([209.51.188.92]:40481) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1igxqG-0004G4-P9 for 38605@debbugs.gnu.org; Mon, 16 Dec 2019 16:23:49 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:38520) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1igxqB-0001Zh-2f; Mon, 16 Dec 2019 16:23:43 -0500 Received: from [2a01:e0a:1d:7270:af76:b9b:ca24:c465] (port=42904 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1igxq8-0002iF-No; Mon, 16 Dec 2019 16:23:42 -0500 From: =?utf-8?Q?Ludovic_Court=C3=A8s?= To: zimoun Subject: Re: [bug#38605] [WIP MLton 0/1] Add MLton References: <877e2z7e3x.fsf@posteo.net> <87v9qix001.fsf@gnu.org> <87y2vd43uo.fsf@posteo.net> <87tv60k2pw.fsf@gnu.org> X-URL: http://www.fdn.fr/~lcourtes/ X-Revolutionary-Date: 26 Frimaire an 228 de la =?utf-8?Q?R=C3=A9volution?= X-PGP-Key-ID: 0x090B11993D9AEBB5 X-PGP-Key: http://www.fdn.fr/~lcourtes/ludovic.asc X-PGP-Fingerprint: 3CE4 6455 8A84 FDC6 9DB4 0CFB 090B 1199 3D9A EBB5 X-OS: x86_64-pc-linux-gnu Date: Mon, 16 Dec 2019 22:23:39 +0100 In-Reply-To: (zimoun's message of "Sun, 15 Dec 2019 02:59:47 +0100") Message-ID: <87k16wdkx0.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 38605 Cc: Brett Gilio , 38605@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) Hi Simon, zimoun skribis: > To my knowledge, the most advanced ML-family language able to > bootstrap (and verified with prover etc.) is CakeML (subset of > Standard ML). > > (And not packaged in Guix, AFAICT.) > > https://cakeml.org/ Right, thanks for the pointer! CakeML is truly impressive. It=E2=80=99s a= lso nice to see how the tiny diagram to the right of the web page clearly and succinctly describes its compiler/language tower. Ludo=E2=80=99. From debbugs-submit-bounces@debbugs.gnu.org Mon Dec 16 21:21:21 2019 Received: (at 38605) by debbugs.gnu.org; 17 Dec 2019 02:21:21 +0000 Received: from localhost ([127.0.0.1]:40575 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ih2UD-0006Sk-FN for submit@debbugs.gnu.org; Mon, 16 Dec 2019 21:21:21 -0500 Received: from mout01.posteo.de ([185.67.36.65]:46024) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ih2U9-0006SU-JI for 38605@debbugs.gnu.org; Mon, 16 Dec 2019 21:21:20 -0500 Received: from submission (posteo.de [89.146.220.130]) by mout01.posteo.de (Postfix) with ESMTPS id 34A58160062 for <38605@debbugs.gnu.org>; Tue, 17 Dec 2019 03:21:11 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.net; s=2017; t=1576549271; bh=xI9G6xjh2bCBuMYCzIVBx0Agj5w9JWRXfMkgaeC8/6w=; h=From:To:Cc:Subject:Date:From; b=Rr/DQffZztZ/axxPe8rCYXXcxu8NsqcVoqwNN5ilx5w3Jkt8VqON5hHu+tzrmZ5Xn oFMs5Fzd+pmT3JrUifvz78isRL/8+tRLf7/mBBOPd2WNsVr8kMDFXceWrylmAP19wI Igu0cFiffgMU8sbqns0S+fIXu67/uz5e6kfWKFNgE7wKq8OMFAsgX7PZUiX6+wqmoR aHT1qI6+dsIRVyR5+nG6xzo4anTcXoZBJRrJzZpj5JfSMc/btVOEn0QdX3wK3nn9C2 KadmU1DSusIEnvoKGtxEAJFnS9E7NePSu/pAeeGaPQ6zaKGtq2KPI50rRxFCKy9pSO KdRIm05yjggFQ== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 47cMM92dYdz6tm5; Tue, 17 Dec 2019 03:21:09 +0100 (CET) From: Brett Gilio To: Ludovic =?utf-8?Q?Court=C3=A8s?= Subject: Re: [bug#38605] [WIP MLton 0/1] Add MLton References: <877e2z7e3x.fsf@posteo.net> <87v9qix001.fsf@gnu.org> <87y2vd43uo.fsf@posteo.net> <87tv60k2pw.fsf@gnu.org> <87k16wdkx0.fsf@gnu.org> Date: Mon, 16 Dec 2019 20:20:45 -0600 In-Reply-To: <87k16wdkx0.fsf@gnu.org> ("Ludovic \=\?utf-8\?Q\?Court\=C3\=A8s\=22'\?\= \=\?utf-8\?Q\?s\?\= message of "Mon, 16 Dec 2019 22:23:39 +0100") Message-ID: <878snbzo8y.fsf@posteo.net> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 38605 Cc: 38605@debbugs.gnu.org, bandali@gnu.org, zimoun X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) Ludovic Court=C3=A8s writes: > Hi Simon, > > zimoun skribis: > >> To my knowledge, the most advanced ML-family language able to >> bootstrap (and verified with prover etc.) is CakeML (subset of >> Standard ML). >> >> (And not packaged in Guix, AFAICT.) >> >> https://cakeml.org/ > > Right, thanks for the pointer! CakeML is truly impressive. It=E2=80=99s= also > nice to see how the tiny diagram to the right of the web page clearly > and succinctly describes its compiler/language tower. > > Ludo=E2=80=99. 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 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. Ultimately I think we need a vehicle for ML to be fledged out in Guix so that we can have a consistent set of utilities for the formal methods community to work in with Guix (see my formal methods working group proposal email). Maybe at some later date we could even fledge out that bootstrapping compiler to be its own distinct implementation of ML, but i'll save that for a later date. Regardless, the issue of binaries-on-binaries in ML seems to be reaching back to 1993! It's about time we ended that. Stay tuned for more information on what I think we could do about that. --=20 Brett M. Gilio GNU Guix, Contributor From debbugs-submit-bounces@debbugs.gnu.org Tue Dec 17 11:43:10 2019 Received: (at 38605) by debbugs.gnu.org; 17 Dec 2019 16:43:10 +0000 Received: from localhost ([127.0.0.1]:42310 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ihFwE-0003KY-0F for submit@debbugs.gnu.org; Tue, 17 Dec 2019 11:43:10 -0500 Received: from mail-qk1-f176.google.com ([209.85.222.176]:32853) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ihFwC-0003KL-T7 for 38605@debbugs.gnu.org; Tue, 17 Dec 2019 11:43:09 -0500 Received: by mail-qk1-f176.google.com with SMTP id d71so6922040qkc.0 for <38605@debbugs.gnu.org>; Tue, 17 Dec 2019 08:43:08 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=0guW4amzcxJK3PeYus//l+wsxqKPdX7YMaQAH/h0Txc=; b=Gsa+5g4syRlSRRdR2l2thT/mqDA0bkPrMuzWxPmgtuex64JhZzG1M7mkACVpmY9Xhw gE7HXxj2y8jRfIZ1yZgDR4MvRS6nqwbVetrYM63s7aSRf/JZx3AshD8XTFJS7px9oDzN 3hAwdyg7TvRpPmMkc3VflRK2AUGoSjXPsdg1idQyXYS5YyfqdrEg/p0T/t7ZfS4dBQD0 1+5Jvhgps+ugaAR0gTDZpXCN+wg+ZDZtIksLM5zk8GhJdBL/UfSB/sZzT1Q0vqy0NQWl apTR3Kx1gQ6YJe4REc2n/IyTBnQ1UKQS/XXm05EO0KeGfoPic5P6WMITcDnvJBnh+oXO jVBw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=0guW4amzcxJK3PeYus//l+wsxqKPdX7YMaQAH/h0Txc=; b=O6oBa4ll/dTt/E0gTWeFoFT8P4dma91kaQkWBAex6hHNy5WsEW5aJlsCEC1s7nLQq1 H0hE+9uBZPa+UDGmrw3mha6piC+Cpx5ohIoBp4FyuRPjfRQpiBxyF43gKYL22wQvzWE9 TeBMxg875yplKL9FFBElOLvV5yyCET8QBCExCdZUIjGdKzMYKijjqEy+80fNmFlVIyZo gajTf7PSeWpgqfgqrPkYYmjsJM89Q4JpfGJBzDq1uO9eI+F7Qc+mUKybczkLG6iTISnU kpHO8nsqPPMIeYUZnJxfjQ4qeZMx5YwS7mDRJxYr65gfF9+WyjgKcraNfI3sQUMMcLoG HtjA== X-Gm-Message-State: APjAAAWG0gfUmraZikE3tPqnijYpgIQYpC5KmXmBY266zasDLl63ViqH OHoGCRPXZTGloexNtuwLJ2UYOjZZMBFvEn0n0LM= X-Google-Smtp-Source: APXvYqw267AZF3FQ2zrY5xkMJ7bUq9GkImnLolJHE96ki4RFoxm1SreOX4hl0ERlkEO6TBG8RNfpcONdIOrgnWmrqKg= X-Received: by 2002:a05:620a:1592:: with SMTP id d18mr6012276qkk.80.1576600983273; Tue, 17 Dec 2019 08:43:03 -0800 (PST) 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: Subject: Re: [bug#38605] [WIP MLton 0/1] Add MLton To: Brett Gilio Content-Type: text/plain; charset="UTF-8" X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 38605 Cc: =?UTF-8?Q?Ludovic_Court=C3=A8s?= , Amin Bandali , 38605@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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 From debbugs-submit-bounces@debbugs.gnu.org Wed Dec 18 09:49:09 2019 Received: (at 38605) by debbugs.gnu.org; 18 Dec 2019 14:49:09 +0000 Received: from localhost ([127.0.0.1]:42812 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ihadR-0003AN-KW for submit@debbugs.gnu.org; Wed, 18 Dec 2019 09:49:09 -0500 Received: from eggs.gnu.org ([209.51.188.92]:48162) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ihadQ-0003AC-Ao for 38605@debbugs.gnu.org; Wed, 18 Dec 2019 09:49:08 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:44157) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ihadK-0004by-Pg; Wed, 18 Dec 2019 09:49:02 -0500 Received: from [2a01:e0a:1d:7270:af76:b9b:ca24:c465] (port=41346 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ihadI-0001br-Vu; Wed, 18 Dec 2019 09:49:01 -0500 From: =?utf-8?Q?Ludovic_Court=C3=A8s?= To: zimoun Subject: Re: [bug#38605] [WIP MLton 0/1] Add MLton 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> X-URL: http://www.fdn.fr/~lcourtes/ X-Revolutionary-Date: 28 Frimaire an 228 de la =?utf-8?Q?R=C3=A9volution?= X-PGP-Key-ID: 0x090B11993D9AEBB5 X-PGP-Key: http://www.fdn.fr/~lcourtes/ludovic.asc X-PGP-Fingerprint: 3CE4 6455 8A84 FDC6 9DB4 0CFB 090B 1199 3D9A EBB5 X-OS: x86_64-pc-linux-gnu Date: Wed, 18 Dec 2019 15:48:57 +0100 In-Reply-To: (zimoun's message of "Tue, 17 Dec 2019 17:42:51 +0100") Message-ID: <87zhfpofja.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 38605 Cc: Amin Bandali , Brett Gilio , 38605@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) Hi, zimoun skribis: > 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". :-) Their claim is summarized on the home page (emphasis mine): The CakeML compiler has been bootstrapped inside HOL. By bootstrapped we mean that the compiler has compiled itself. [=E2=80=A6] The result is a verified binary that _provably_ implements the compiler itself IOW, their approach is to provide a formal proof that a given byte stream corresponds to the given source code. This approach is very different from everything we=E2=80=99ve been doing so far. In essence, we=E2=80=99ve been focusing on building everything from source, with the assumption that source code is auditable. Instead of doing that, they formally provide the source/binary correspondence, which is much stronger. Once you have this proof, it doesn=E2=80=99t matter how HOL or PolyML or any other dependency is built, = AIUI. In theory, HOL could be the target of a trusting-trust attack. But then again, one could very well check it with paper-and-pen or with HOL plus manual verification. Food for thought! Ludo=E2=80=99. From debbugs-submit-bounces@debbugs.gnu.org Fri Dec 20 23:56:32 2019 Received: (at 38605) by debbugs.gnu.org; 21 Dec 2019 04:56:32 +0000 Received: from localhost ([127.0.0.1]:47518 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iiWoZ-0002m3-P8 for submit@debbugs.gnu.org; Fri, 20 Dec 2019 23:56:32 -0500 Received: from eggs.gnu.org ([209.51.188.92]:54247) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iiWoX-0002lq-Ol for 38605@debbugs.gnu.org; Fri, 20 Dec 2019 23:56:30 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:53142) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1iiWoQ-0005pp-UE; Fri, 20 Dec 2019 23:56:24 -0500 Received: from [2605:6000:1a0d:6320::6a8] (port=42094 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1iiWoO-0000yS-Le; Fri, 20 Dec 2019 23:56:22 -0500 From: Brett Gilio To: Ludovic =?utf-8?Q?Court=C3=A8s?= Subject: Re: [bug#38605] [WIP MLton 0/1] Add MLton 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> <87zhfpofja.fsf@gnu.org> Date: Fri, 20 Dec 2019 22:56:24 -0600 In-Reply-To: <87zhfpofja.fsf@gnu.org> ("Ludovic \=\?utf-8\?Q\?Court\=C3\=A8s\=22'\?\= \=\?utf-8\?Q\?s\?\= message of "Wed, 18 Dec 2019 15:48:57 +0100") Message-ID: <87a77mqnt3.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 38605 Cc: Brett Gilio , 38605@debbugs.gnu.org, Amin Bandali , zimoun X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) Ludovic Court=C3=A8s writes: > Hi, > > zimoun skribis: > >> 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". :-) > > Their claim is summarized on the home page (emphasis mine): > > The CakeML compiler has been bootstrapped inside HOL. By bootstrapped > we mean that the compiler has compiled itself. [=E2=80=A6] The result i= s a > verified binary that _provably_ implements the compiler itself > > IOW, their approach is to provide a formal proof that a given byte > stream corresponds to the given source code. > > This approach is very different from everything we=E2=80=99ve been doing = so > far. In essence, we=E2=80=99ve been focusing on building everything from > source, with the assumption that source code is auditable. > > Instead of doing that, they formally provide the source/binary > correspondence, which is much stronger. Once you have this proof, it > doesn=E2=80=99t matter how HOL or PolyML or any other dependency is built= , AIUI. > > In theory, HOL could be the target of a trusting-trust attack. But then > again, one could very well check it with paper-and-pen or with HOL plus > manual verification. > > Food for thought! > > Ludo=E2=80=99. > > > > I kind of wonder if their method of having a HOL-implemented proof for their source/binary bytestream is a possibility for GNU Guix in the future? It makes for an interesting speculation, especially for system-level proofs of blob trust. Bandli? --=20 Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE] From debbugs-submit-bounces@debbugs.gnu.org Mon Sep 14 13:36:48 2020 Received: (at 38605) by debbugs.gnu.org; 14 Sep 2020 17:36:48 +0000 Received: from localhost ([127.0.0.1]:56106 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kHsPI-0002FH-3R for submit@debbugs.gnu.org; Mon, 14 Sep 2020 13:36:48 -0400 Received: from mail-wr1-f49.google.com ([209.85.221.49]:41498) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kHsPE-0002F0-M0 for 38605@debbugs.gnu.org; Mon, 14 Sep 2020 13:36:47 -0400 Received: by mail-wr1-f49.google.com with SMTP id w5so512352wrp.8 for <38605@debbugs.gnu.org>; Mon, 14 Sep 2020 10:36:44 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:cc:subject:references:date:in-reply-to:message-id :user-agent:mime-version; bh=4kGpYnBpkJLXwciiccaogdvXVdcXTt6d85canf6/aOs=; b=ELaoow68C/OPywtEidyZw3mMnld/CpUf8peYlg26P6vIrqWz/FHfvvS0K8pkmbQJuh e/GNDHB8OX92qmdNO8mNBKBG74LHMbKgl2XazMdGC6xwyGWbfZ9NLCMKzEash0iwFqNx 5ook1x/U7OFLwj9qRXwg6iCE8iB6aRhmnfshA/3+xSCK1uc6898MZjDxULPoSp9WyW9x Y0idI1poAM/8pdvd6eWcuyV3tlxj3FWFTC+pzg0Qoc1FXyK/sZWslB+sGk1xEk90ZuEg Q72SKXyA01vs4s0ovF4PAjy/ggdXja+cqv+vTKL8RFvlVD9XCdofTjpUB9r/xmOlu07z cVSQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to :message-id:user-agent:mime-version; bh=4kGpYnBpkJLXwciiccaogdvXVdcXTt6d85canf6/aOs=; b=VmO0YCJC91L8YLkQ4YejUQ/xjWE/lh5ZxlxNNIA+0aETEB+ogD8/QcG7cj/q8/QFvX qA7xdSNJ8ZzhToZFuaJXKFACbpYh1VAYgb4gPrNjzyak8GX2vh1C7xIt++HR6iCJ4l7N PjDJYRVl5mlfTCLEZPD9uPHxJXeTwoJ/MEPUfxnzqF/06mL2ouDJ8wXSuoNDf7j3s97L krbcR9bTDEMlmI+GDDLVewVgcGFOlP0g3jzkdQgo/zlnZH5FP3aArlCp8jHPrz6U7xh/ ukX2L3bQkBXaINPzskSZv4gUKt5JQ3AhkzMBu33xw3tYmjq9da7O2R0rOsbI9W6jOX7B 16Uw== X-Gm-Message-State: AOAM531oavLcNfSdQ1r6Ud8qRU+qWgFfI1PMDE+xaErduQdXRRHcyh57 XqZGtfLZZOWd7eh83b9SuZndUHI+5hw= X-Google-Smtp-Source: ABdhPJw83outh8x4IvbCpbzdPx6UaAvBk20M0p5KIO/6BJt7U05e/cUfZny8CrUqfGQTUcJtkwI/zA== X-Received: by 2002:a5d:4cc1:: with SMTP id c1mr16998435wrt.122.1600104998526; Mon, 14 Sep 2020 10:36:38 -0700 (PDT) Received: from pfiuh02 ([193.48.40.241]) by smtp.gmail.com with ESMTPSA id a17sm22931159wra.24.2020.09.14.10.36.37 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 14 Sep 2020 10:36:37 -0700 (PDT) From: zimoun To: Brett Gilio Subject: Re: [bug#38605] [WIP MLton 1/1] gnu: Add mlton. References: <877e2z7e3x.fsf@posteo.net> <874ky37e1n.fsf@posteo.net> Date: Mon, 14 Sep 2020 19:36:37 +0200 In-Reply-To: <874ky37e1n.fsf@posteo.net> (Brett Gilio's message of "Fri, 13 Dec 2019 21:59:32 -0600") Message-ID: <87ft7kqmze.fsf@gmail.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.1 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: 0.7 (/) X-Debbugs-Envelope-To: 38605 Cc: 38605@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.3 (/) Hi Brett, Digging in old unmerged patches, I hit this one. :-) On Fri, 13 Dec 2019 at 21:59, Brett Gilio wrote: >>>From d6e94b0a04bf71e51d29b7228bd4233bf763eaaa Mon Sep 17 00:00:00 2001 > From: Brett Gilio > Date: Fri, 13 Dec 2019 21:54:13 -0600 > Subject: [WIP MLton 1/1] gnu: Add mlton. > > * gnu/packages/sml.scm (mlton-no-gcc): New variable. > --- > gnu/packages/sml.scm | 138 +++++++++++++++++++++++++++++++++++++++++++ > 1 file changed, 138 insertions(+) What is the status of the WIP? Have you make progress? > diff --git a/gnu/packages/sml.scm b/gnu/packages/sml.scm > index 30ee58c498..e45ce4c59c 100644 > --- a/gnu/packages/sml.scm > +++ b/gnu/packages/sml.scm > @@ -75,3 +75,141 @@ function interface, and a symbolic debugger.") > (license > (list license:lgpl2.1 > license:lgpl2.1+)))) > + > +(define-private mlton-reduced > + (package > + (name "mlton") > + (version "20180207") > + (source (origin > + (method url-fetch) > + (uri (string-append "https://github.com/MLton/" name > + "/releases/download/on-" version > + "-release/" name "-" version > + "-1.amd64-linux.tgz")) > + (sha256 > + (base32 > + "0f4q575yfm5dpg4a2wsnqn4l2zrar96p6rlsk0dw10ggyfwvsjlf")))) > + (build-system trivial-build-system) > + ;; TODO: The build arguments can be much more programmatic. > + (arguments > + '(#:modules > + ((guix build utils)) > + #:builder > + (begin > + (use-modules (guix build utils)) > + (let* > + ((out (assoc-ref %outputs "out")) > + (source (assoc-ref %build-inputs "source")) > + (tar (string-append (assoc-ref %build-inputs "tar") "/bin/tar")) > + (patchelf (string-append (assoc-ref %build-inputs "patchelf") "/bin/patchelf")) > + (ld (string-append (assoc-ref %build-inputs "glibc") "/lib/ld-linux-x86-64.so.2")) > + (gmp (string-append (assoc-ref %build-inputs "gmp") "/lib")) > + (bash (string-append (assoc-ref %build-inputs "bash") "/bin/bash")) > + (rm (string-append (assoc-ref %build-inputs "coreutils") "/bin/rm")) > + (PATH > + (string-append > + (assoc-ref %build-inputs "gzip") "/bin" > + ":" > + (assoc-ref %build-inputs "tar") "/bin"))) > + (mkdir-p out) > + (mkdir-p (string-append out "/bin")) > + (with-directory-excursion out > + (setenv "PATH" PATH) > + (system* tar "xf" source "--strip-components=1") > + ;; PATCHES FOR /LIB/MLTON/MLTON-COMPILE > + (system* patchelf > + "--set-interpreter" > + ld > + (string-append out "/lib/mlton/mlton-compile")) > + (system* patchelf > + "--set-rpath" > + gmp > + (string-append out "/lib/mlton/mlton-compile")) > + ;; PATCHES FOR /BIN/MLLEX > + (system* patchelf > + "--set-interpreter" > + ld > + (string-append out "/bin/mllex")) > + (system* patchelf > + "--set-rpath" > + gmp > + (string-append out "/bin/mllex")) > + ;; PATCHES FOR /BIN/MLYACC > + (system* patchelf > + "--set-interpreter" > + ld > + (string-append out "/bin/mlyacc")) > + (system* patchelf > + "--set-rpath" > + gmp > + (string-append out "/bin/mlyacc")) > + ;; DELETE ALL UNNEEDED COMPONENTS > + (system* rm "-rf" > + "bin/mlprof" > + "bin/mlnlffigen" > + "LICENSE" > + "Makefile" > + "CHANGELOG.adoc" > + "README.adoc" > + "share") > + ;; PATCH SHEBANG FOR BIN/MLTON > + (substitute* "bin/mlton" > + (("/usr/bin/env bash") > + bash))))))) > + (native-inputs `(("glibc" ,glibc) > + ("patchelf" ,patchelf) > + ("tar" ,tar) > + ("bash" ,bash) > + ("coreutils" ,coreutils) > + ("gzip" ,gzip) > + ("gmp" ,gmp))) > + (supported-systems '("x86_64-linux")) > + (synopsis #f) > + (description #f) > + (home-page #f) > + (license #f))) > + > +(define-public mlton-no-gcc > + (package > + (name "mlton-no-gcc") > + (version "20180207") > + (source (origin > + (method url-fetch) > + (uri (string-append "https://github.com/MLton/" name > + "/archive/on-" version > + "-release.tar.gz")) > + (sha256 > + (base32 > + "1l1flhxx8hr4n3mf87m02231r3m2f3sh28zfxma3g41jscmj21zi")))) > + (build-system gnu-build-system) > + (arguments > + `(#:parallel-build? #f ; See: https://github.com/MLton/mlton/issues/348 > + #:phases > + (modify-phases %standard-phases > + (delete 'configure) > + (replace 'install > + (lambda _ > + (invoke "make" > + (string-append "PREFIX=" (assoc-ref %outputs "out")) > + "install")))))) > + (native-inputs > + `(("mlton" ,mlton-reduced) > + ("which" ,which))) > + (propagated-inputs > + `(("gmp" ,gmp))) > + (supported-systems '("x86_64-linux")) > + (synopsis "Whole-program, optimizing Standard ML compiler") > + (description "MLton is a whole-program optimizing compiler for Standard ML. > +MLton generates standalone executables with excellent runtime performance, is > +SML '97 compliant, and has a complete basis library. MLton has source-level > +profiling, a fast C FFI, an interface to the GNU multiprecision library, and > +lots of useful libraries.") > + (home-page "http://mlton.org/") > + (license license:hpnd))) > + > +(define-public mlton > + (package (inherit mlton-no-gcc) > + (name "mlton") > + (propagated-inputs > + `(("gcc-toolchain" ,gcc-toolchain) > + ,@(package-propagated-inputs mlton-no-gcc))))) All the best, simon From debbugs-submit-bounces@debbugs.gnu.org Tue Apr 12 06:25:31 2022 Received: (at 38605) by debbugs.gnu.org; 12 Apr 2022 10:25:31 +0000 Received: from localhost ([127.0.0.1]:47671 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1neDiE-0008Fl-Iu for submit@debbugs.gnu.org; Tue, 12 Apr 2022 06:25:31 -0400 Received: from mail-wm1-f44.google.com ([209.85.128.44]:43732) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1neDiC-0008FV-Bs for 38605@debbugs.gnu.org; Tue, 12 Apr 2022 06:25:29 -0400 Received: by mail-wm1-f44.google.com with SMTP id m67-20020a1ca346000000b0038e6a1b218aso1320030wme.2 for <38605@debbugs.gnu.org>; Tue, 12 Apr 2022 03:25:28 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=from:to:cc:subject:references:date:in-reply-to:message-id :user-agent:mime-version; bh=gDUYcKz/tYi1wsYQDkv6emLc4eqzPLSSz0eSgYofbV8=; b=Oe4l666Xa88+iMARydoIrsxgU53l0S0tIPNkwMhzCkeYuh8sezfq4alXXZEnWYqFko VO1wiCBSEzjvlhEo0BbruO09FLgFlk3e4Y9+NCaNA4libWjNUYamf7qi9gvq1yb8454L XV3bfSIKjAkfySnWg9Jg0i6MQN7/I1Lmhen5mYz1PdY3vmbYdJCmjqNEqj5hiVBtLcU8 VvfsmZYeM717lk/jTOwoFhs1smY86lUIeAQTS+ipx09NTPPwBmOe8xQupOcbaNAvpd5/ UcRT+nEXMATWYhu6wrHRd4DpJQIe/5574qTbvx6kqEAHWiHD0q3yepc1QOMsijNpq9Ul CTyQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to :message-id:user-agent:mime-version; bh=gDUYcKz/tYi1wsYQDkv6emLc4eqzPLSSz0eSgYofbV8=; b=3y+wiNWsE6d62AT+QR/3+Nx0rbMo5wi8SIfwnc8u5+28j31VTL8AfJif7Bm/gfWh0u uE7xeQ8G6NJMbFiY0IXmgYk/Zrq//7pgaTZxJ0sGM2UsN9zBv7CmDTm538LTIPiVDNZZ vCAkI4sxiuNj/xNZ9b1XsQKJDoRPb6CptG7MAp7LTAQw64odxCr77I8zi5oZolUZR7u8 8a/QrkTtKjamcmClgZ/LQqUM3h46l3Ydyo0nc2C0V6n9HRL7BwSvQRNvFrvUnWqGS4Tx ANvmHQnusO5fFlTrnDBZMY5tal6MDiY18DjRVbD0Ev8CwCURHmFyefVgU+4IwV0LiZJ/ V8/A== X-Gm-Message-State: AOAM532Wq7IurJOOQbhwQzJ9jlQ15Clko5xU0MivZ7FTOWwGF9N4e5Eh Y2cmeOZMaMMS4M1Ihd5dM1U= X-Google-Smtp-Source: ABdhPJxdPbCbnWYNyiSq9iDXryhn1hM8AXNo+PkmAYAscaqDNZQ+0q5rIXCrIdL5cvlruiXN8Y4fHQ== X-Received: by 2002:a05:600c:4e11:b0:38c:bd19:e72c with SMTP id b17-20020a05600c4e1100b0038cbd19e72cmr3453875wmq.174.1649759122428; Tue, 12 Apr 2022 03:25:22 -0700 (PDT) Received: from lili (roam-nat-fw-prg-194-254-61-42.net.univ-paris-diderot.fr. [194.254.61.42]) by smtp.gmail.com with ESMTPSA id h10-20020a05600c144a00b0038ccc75a6adsm2023149wmi.37.2022.04.12.03.25.21 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 12 Apr 2022 03:25:21 -0700 (PDT) From: zimoun To: Brett Gilio Subject: Re: bug#38605: [WIP MLton 0/1] Add MLton References: <877e2z7e3x.fsf@posteo.net> <874ky37e1n.fsf@posteo.net> <87ft7kqmze.fsf@gmail.com> Date: Tue, 12 Apr 2022 12:21:50 +0200 In-Reply-To: <87ft7kqmze.fsf@gmail.com> (zimoun's message of "Mon, 14 Sep 2020 19:36:37 +0200") Message-ID: <86h76y38ld.fsf_-_@gmail.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: 0.7 (/) X-Debbugs-Envelope-To: 38605 Cc: guix-devel@gnu.org, 38605@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.3 (/) Hi, CC: guix-devel On Mon, 14 Sep 2020 at 19:36, zimoun wrote: > Digging in old unmerged patches, I hit this one. :-) The last interaction of this WIP patch #38605 [1] about MLton is from 1 year, 29 weeks, 6 days ago. Whereas the discussion in this thread about bootstrap strategies is really worth, I am going to close the submission soon. 1: > On Fri, 13 Dec 2019 at 21:59, Brett Gilio wrote: > >> * gnu/packages/sml.scm (mlton-no-gcc): New variable. >> --- >> gnu/packages/sml.scm | 138 +++++++++++++++++++++++++++++++++++++++++++ >> 1 file changed, 138 insertions(+) > > What is the status of the WIP? > Have you make progress? This patch requires a little rebase and could be included in Guix. Any taker? >> diff --git a/gnu/packages/sml.scm b/gnu/packages/sml.scm >> index 30ee58c498..e45ce4c59c 100644 >> --- a/gnu/packages/sml.scm >> +++ b/gnu/packages/sml.scm >> @@ -75,3 +75,141 @@ function interface, and a symbolic debugger.") >> (license >> (list license:lgpl2.1 >> license:lgpl2.1+)))) >> + >> +(define-private mlton-reduced >> + (package >> + (name "mlton") >> + (version "20180207") >> + (source (origin >> + (method url-fetch) >> + (uri (string-append "https://github.com/MLton/" name >> + "/releases/download/on-" version >> + "-release/" name "-" version >> + "-1.amd64-linux.tgz")) >> + (sha256 >> + (base32 >> + "0f4q575yfm5dpg4a2wsnqn4l2zrar96p6rlsk0dw10ggyfwvsjlf")))) >> + (build-system trivial-build-system) >> + ;; TODO: The build arguments can be much more programmatic. >> + (arguments >> + '(#:modules >> + ((guix build utils)) >> + #:builder >> + (begin >> + (use-modules (guix build utils)) >> + (let* >> + ((out (assoc-ref %outputs "out")) >> + (source (assoc-ref %build-inputs "source")) >> + (tar (string-append (assoc-ref %build-inputs "tar") "/bin/tar")) >> + (patchelf (string-append (assoc-ref %build-inputs "patchelf") "/bin/patchelf")) >> + (ld (string-append (assoc-ref %build-inputs "glibc") "/lib/ld-linux-x86-64.so.2")) >> + (gmp (string-append (assoc-ref %build-inputs "gmp") "/lib")) >> + (bash (string-append (assoc-ref %build-inputs "bash") "/bin/bash")) >> + (rm (string-append (assoc-ref %build-inputs "coreutils") "/bin/rm")) >> + (PATH >> + (string-append >> + (assoc-ref %build-inputs "gzip") "/bin" >> + ":" >> + (assoc-ref %build-inputs "tar") "/bin"))) >> + (mkdir-p out) >> + (mkdir-p (string-append out "/bin")) >> + (with-directory-excursion out >> + (setenv "PATH" PATH) >> + (system* tar "xf" source "--strip-components=1") >> + ;; PATCHES FOR /LIB/MLTON/MLTON-COMPILE >> + (system* patchelf >> + "--set-interpreter" >> + ld >> + (string-append out "/lib/mlton/mlton-compile")) >> + (system* patchelf >> + "--set-rpath" >> + gmp >> + (string-append out "/lib/mlton/mlton-compile")) >> + ;; PATCHES FOR /BIN/MLLEX >> + (system* patchelf >> + "--set-interpreter" >> + ld >> + (string-append out "/bin/mllex")) >> + (system* patchelf >> + "--set-rpath" >> + gmp >> + (string-append out "/bin/mllex")) >> + ;; PATCHES FOR /BIN/MLYACC >> + (system* patchelf >> + "--set-interpreter" >> + ld >> + (string-append out "/bin/mlyacc")) >> + (system* patchelf >> + "--set-rpath" >> + gmp >> + (string-append out "/bin/mlyacc")) >> + ;; DELETE ALL UNNEEDED COMPONENTS >> + (system* rm "-rf" >> + "bin/mlprof" >> + "bin/mlnlffigen" >> + "LICENSE" >> + "Makefile" >> + "CHANGELOG.adoc" >> + "README.adoc" >> + "share") >> + ;; PATCH SHEBANG FOR BIN/MLTON >> + (substitute* "bin/mlton" >> + (("/usr/bin/env bash") >> + bash))))))) >> + (native-inputs `(("glibc" ,glibc) >> + ("patchelf" ,patchelf) >> + ("tar" ,tar) >> + ("bash" ,bash) >> + ("coreutils" ,coreutils) >> + ("gzip" ,gzip) >> + ("gmp" ,gmp))) >> + (supported-systems '("x86_64-linux")) >> + (synopsis #f) >> + (description #f) >> + (home-page #f) >> + (license #f))) >> + >> +(define-public mlton-no-gcc >> + (package >> + (name "mlton-no-gcc") >> + (version "20180207") >> + (source (origin >> + (method url-fetch) >> + (uri (string-append "https://github.com/MLton/" name >> + "/archive/on-" version >> + "-release.tar.gz")) >> + (sha256 >> + (base32 >> + "1l1flhxx8hr4n3mf87m02231r3m2f3sh28zfxma3g41jscmj21zi")))) >> + (build-system gnu-build-system) >> + (arguments >> + `(#:parallel-build? #f ; See: https://github.com/MLton/mlton/issues/348 >> + #:phases >> + (modify-phases %standard-phases >> + (delete 'configure) >> + (replace 'install >> + (lambda _ >> + (invoke "make" >> + (string-append "PREFIX=" (assoc-ref %outputs "out")) >> + "install")))))) >> + (native-inputs >> + `(("mlton" ,mlton-reduced) >> + ("which" ,which))) >> + (propagated-inputs >> + `(("gmp" ,gmp))) >> + (supported-systems '("x86_64-linux")) >> + (synopsis "Whole-program, optimizing Standard ML compiler") >> + (description "MLton is a whole-program optimizing compiler for Standard ML. >> +MLton generates standalone executables with excellent runtime performance, is >> +SML '97 compliant, and has a complete basis library. MLton has source-level >> +profiling, a fast C FFI, an interface to the GNU multiprecision library, and >> +lots of useful libraries.") >> + (home-page "http://mlton.org/") >> + (license license:hpnd))) >> + >> +(define-public mlton >> + (package (inherit mlton-no-gcc) >> + (name "mlton") >> + (propagated-inputs >> + `(("gcc-toolchain" ,gcc-toolchain) >> + ,@(package-propagated-inputs mlton-no-gcc))))) Cheers, simon From debbugs-submit-bounces@debbugs.gnu.org Wed May 04 07:58:43 2022 Received: (at 38605-done) by debbugs.gnu.org; 4 May 2022 11:58:43 +0000 Received: from localhost ([127.0.0.1]:41986 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1nmDeV-0001Ce-Ll for submit@debbugs.gnu.org; Wed, 04 May 2022 07:58:43 -0400 Received: from mail-wr1-f52.google.com ([209.85.221.52]:46677) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1nmDeT-0001CO-Kg for 38605-done@debbugs.gnu.org; Wed, 04 May 2022 07:58:42 -0400 Received: by mail-wr1-f52.google.com with SMTP id i5so1666940wrc.13 for <38605-done@debbugs.gnu.org>; Wed, 04 May 2022 04:58:41 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=from:to:cc:subject:references:date:in-reply-to:message-id :user-agent:mime-version; bh=I3Ehxi18xUkmkHAUyJCSAOrBcQ8knfpz4PNSY6KOOOQ=; b=d3AKfRCIWbfXBb0coOJEEBl/oTsLOv2HyIAT1nQoQDGioMq85RpOdIvz/gmrbGNQi3 9ErIZCAnTtdti2OD/QzLiawOzR4y3IrUkqUS41tKLJ1EF7h263bWYb7Bjy/lghCEo2WQ jA5OfgJ3289wWOCzvXuF7I5TutsGsbDgQao/+Apl4PMx5sefo9a+4zxJvEh/x3I/N2iY 5m1KLtyPAnHNcZTHfqG+an5mbffEdLHzUSAh7Ja/QalAK1YwMeH9MerK4ExgRCP7lpmc 7tGDYCUtInX4obGLPAnD5sVnVpZ+W0/cx5XzcYmQX93jByemFEZthVAnKLt9VETbWhep Ll2A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to :message-id:user-agent:mime-version; bh=I3Ehxi18xUkmkHAUyJCSAOrBcQ8knfpz4PNSY6KOOOQ=; b=dwlV3VLwXgOFEBtjYpFKZFjkAmv6jp/zp8UkgNgfMcFtUJ82HqRE1sNK+DiQyVEJAU O7GkyvjL2qWxHFwnFKKlFK23I+VEek5r5Nd18EiqdLW6aeIRH5TReF3cbgfudVl8fJbC wCS7AdCcAV/WwLVS9BDLxOhVl+wmLiYBSphnZGhanDarXlrnPR7ogN318aBLFI4yuAnW 4nCrvKEAagIEn3ox0hYr1yf/K1tbIQcnw4Ww0q4hyAFlAx0/pFvGpyBkC58YFfxh/gt3 EznhczZgsQmIYeg296UIkz2wDFYGMs3tZxB2djjv060HyKFG2QfL9oEQKIUL5iaJ2BGH 33rA== X-Gm-Message-State: AOAM531nSVqBbvw3R+lD6+TaT5aO7T8eFSowRa4C/TZpq/dBCCK4KtMn 7qaNJ15AZKkbOW+qk89y9/25s3VO7nY= X-Google-Smtp-Source: ABdhPJzK2fTnASaLbIfOv9J+jMFfChjPaGcvoT7zZtPdLixJibbYyNiY7be+PDRud6CCGY0Wrz4FUQ== X-Received: by 2002:a5d:528b:0:b0:203:d928:834c with SMTP id c11-20020a5d528b000000b00203d928834cmr16633336wrv.500.1651665515468; Wed, 04 May 2022 04:58:35 -0700 (PDT) Received: from pfiuh07 ([193.48.40.241]) by smtp.gmail.com with ESMTPSA id w6-20020adf8bc6000000b0020c5253d8bdsm13968145wra.9.2022.05.04.04.58.34 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 04 May 2022 04:58:35 -0700 (PDT) From: zimoun To: Brett Gilio Subject: Re: bug#38605: [WIP MLton 0/1] Add MLton References: <877e2z7e3x.fsf@posteo.net> <874ky37e1n.fsf@posteo.net> <87ft7kqmze.fsf@gmail.com> <86h76y38ld.fsf_-_@gmail.com> Date: Wed, 04 May 2022 13:58:11 +0200 In-Reply-To: <86h76y38ld.fsf_-_@gmail.com> (zimoun's message of "Tue, 12 Apr 2022 12:21:50 +0200") Message-ID: <87h7657bn0.fsf_-_@gmail.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 38605-done Cc: 38605-done@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) Hi, On Tue, 12 Apr 2022 at 12:21, zimoun wrote: > On Mon, 14 Sep 2020 at 19:36, zimoun wrote: > >> Digging in old unmerged patches, I hit this one. :-) > > The last interaction of this WIP patch #38605 [1] about MLton is from 1 > year, 29 weeks, 6 days ago. Whereas the discussion in this thread about > bootstrap strategies is really worth, I am going to close the submission > soon. > > 1: > Well, after 3 weeks, 1 day, 1 hour ago. I am closing. Cheers, simon From unknown Tue Jun 24 22:40:06 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Thu, 02 Jun 2022 11:24:04 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator