[WIP MLton 0/1] Add MLton

DoneSubmitted by Brett Gilio.
Details
4 participants
  • Brett Gilio
  • Brett Gilio
  • Ludovic Courtès
  • zimoun
Owner
unassigned
Severity
normal
B
B
Brett Gilio wrote on 14 Dec 2019 04:58
(address . guix-patches@gnu.org)
877e2z7e3x.fsf@posteo.net
From d6e94b0a04bf71e51d29b7228bd4233bf763eaaa Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@posteo.net>
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
B
B
Brett Gilio wrote on 14 Dec 2019 04:59
[WIP MLton 1/1] gnu: Add mlton.
(address . 38605@debbugs.gnu.org)
874ky37e1n.fsf@posteo.net
From d6e94b0a04bf71e51d29b7228bd4233bf763eaaa Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@posteo.net>
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(+)

Toggle diff (148 lines)
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
L
L
Ludovic Courtès wrote on 14 Dec 2019 18:58
Re: [bug#38605] [WIP MLton 0/1] Add MLton
(name . Brett Gilio)(address . brettg@posteo.net)(address . 38605@debbugs.gnu.org)
87v9qix001.fsf@gnu.org
Hi Brett,

Brett Gilio <brettg@posteo.net> skribis:

Toggle quote (6 lines)
> 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.

“Not permissible” is strong (in the sense that Guix doesn’t have such a
strong policy because there are cases where there’s no known way to
bootstrap from source), but clearly, if there’s a documented way to
build MLton from source, this is what we should be aiming for.

Thanks!

Ludo’.
B
B
Brett Gilio wrote on 15 Dec 2019 23:32
(name . Ludovic Courtès)(address . ludo@gnu.org)(address . 38605@debbugs.gnu.org)
87y2vd43uo.fsf@posteo.net
Ludovic Courtès <ludo@gnu.org> writes:

Toggle quote (19 lines)
> Hi Brett,
>
> Brett Gilio <brettg@posteo.net> skribis:
>
>> 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.
>
> “Not permissible” is strong (in the sense that Guix doesn’t have such a
> strong policy because there are cases where there’s no known way to
> bootstrap from source), but clearly, if there’s a documented way to
> build MLton from source, this is what we should be aiming for.
>
> Thanks!
>
> Ludo’.

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
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/mrustcdoing 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!

--
Brett M. Gilio
Homepage -- https://scm.pw/
L
L
Ludovic Courtès wrote on 16 Dec 2019 11:02
(name . Brett Gilio)(address . brettg@posteo.net)(address . 38605@debbugs.gnu.org)
87tv60k2pw.fsf@gnu.org
Hi Brett,

Brett Gilio <brettg@posteo.net> skribis:

Toggle quote (4 lines)
> 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
“best practices” pretty well: for Rust, for Guile (which contains an
interpreter in C), for Common Lisp (GNU clisp is written in C), for C
(MesCC), etc.

Toggle quote (4 lines)
> 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

Toggle quote (10 lines)
> 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 “nothing”, 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’.
Z
Z
zimoun wrote on 15 Dec 2019 02:59
(name . Ludovic Courtès)(address . ludo@gnu.org)
CAJ3okZ3+6rVQuG9hGr6PRiQmsMMBoFA3PjuRLN22oMuNDVsktA@mail.gmail.com
Hi,

I am -- for sure -- not in topic. :-)

On Mon, 16 Dec 2019 at 11:03, Ludovic Courtès <ludo@gnu.org> wrote:

Toggle quote (3 lines)
> 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.)



All the best,
simon
L
L
Ludovic Courtès wrote on 16 Dec 2019 22:23
(name . zimoun)(address . zimon.toutoune@gmail.com)
87k16wdkx0.fsf@gnu.org
Hi Simon,

zimoun <zimon.toutoune@gmail.com> skribis:

Toggle quote (8 lines)
> 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’s also
nice to see how the tiny diagram to the right of the web page clearly
and succinctly describes its compiler/language tower.

Ludo’.
B
B
Brett Gilio wrote on 17 Dec 2019 03:20
(name . Ludovic Courtès)(address . ludo@gnu.org)
878snbzo8y.fsf@posteo.net
Ludovic Courtès <ludo@gnu.org> writes:

Toggle quote (18 lines)
> Hi Simon,
>
> zimoun <zimon.toutoune@gmail.com> 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’s also
> nice to see how the tiny diagram to the right of the web page clearly
> and succinctly describes its compiler/language tower.
>
> Ludo’.

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.

--
Brett M. Gilio <brettg@posteo.net>
GNU Guix, Contributor https://guix.gnu.org/
Z
Z
zimoun wrote on 17 Dec 2019 17:42
(name . Brett Gilio)(address . brettg@posteo.net)
CAJ3okZ2MW3swvwLjZOJxRp8dFcjNEHvBVGwWdQaFeZT84250CA@mail.gmail.com
Hi Brett,

Thank you for the explanations.

On Tue, 17 Dec 2019 at 03:21, Brett Gilio <brettg@posteo.net> wrote:

Toggle quote (4 lines)
> 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". :-)




Toggle quote (4 lines)
> 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
L
L
Ludovic Courtès wrote on 18 Dec 2019 15:48
(name . zimoun)(address . zimon.toutoune@gmail.com)
87zhfpofja.fsf@gnu.org
Hi,

zimoun <zimon.toutoune@gmail.com> skribis:

Toggle quote (13 lines)
> On Tue, 17 Dec 2019 at 03:21, Brett Gilio <brettg@posteo.net> 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. […] 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’ve been doing so
far. In essence, we’ve 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’t 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’.
B
B
Brett Gilio wrote on 21 Dec 2019 05:56
(name . Ludovic Courtès)(address . ludo@gnu.org)
87a77mqnt3.fsf@gnu.org
Ludovic Courtès <ludo@gnu.org> writes:

Toggle quote (46 lines)
> Hi,
>
> zimoun <zimon.toutoune@gmail.com> skribis:
>
>> On Tue, 17 Dec 2019 at 03:21, Brett Gilio <brettg@posteo.net> 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. […] 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’ve been doing so
> far. In essence, we’ve 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’t 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’.
>
>
>
>

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?

--
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg@gnu.org> <brettg@posteo.net>
Z
Z
zimoun wrote on 14 Sep 2020 19:36
Re: [bug#38605] [WIP MLton 1/1] gnu: Add mlton.
(name . Brett Gilio)(address . brettg@posteo.net)(address . 38605@debbugs.gnu.org)
87ft7kqmze.fsf@gmail.com
Hi Brett,

Digging in old unmerged patches, I hit this one. :-)

On Fri, 13 Dec 2019 at 21:59, Brett Gilio <brettg@posteo.net> wrote:
Toggle quote (10 lines)
>>From d6e94b0a04bf71e51d29b7228bd4233bf763eaaa Mon Sep 17 00:00:00 2001
> From: Brett Gilio <brettg@posteo.net>
> 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?


Toggle quote (148 lines)
> 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
Z
Z
zimoun wrote on 12 Apr 12:21 +0200
Re: bug#38605: [WIP MLton 0/1] Add MLton
(name . Brett Gilio)(address . brettg@posteo.net)
86h76y38ld.fsf_-_@gmail.com
Hi,

CC: guix-devel

On Mon, 14 Sep 2020 at 19:36, zimoun <zimon.toutoune@gmail.com> wrote:

Toggle quote (2 lines)
> 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.



Toggle quote (10 lines)
> On Fri, 13 Dec 2019 at 21:59, Brett Gilio <brettg@posteo.net> 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?


Toggle quote (148 lines)
>> 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
Z
Z
zimoun wrote on 4 May 13:58 +0200
(name . Brett Gilio)(address . brettg@posteo.net)(address . 38605-done@debbugs.gnu.org)
87h7657bn0.fsf_-_@gmail.com
Hi,

On Tue, 12 Apr 2022 at 12:21, zimoun <zimon.toutoune@gmail.com> wrote:
Toggle quote (12 lines)
> On Mon, 14 Sep 2020 at 19:36, zimoun <zimon.toutoune@gmail.com> 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: <http://issues.guix.gnu.org/issue/38605>
>

Well, after 3 weeks, 1 day, 1 hour ago. I am closing.


Cheers,
simon
Closed
?
Your comment

This issue is archived.

To comment on this conversation send email to 38605@debbugs.gnu.org