[bug#38605] [WIP MLton 0/1] Add MLton

[bug#38605] [WIP MLton 0/1] Add MLton

[Brett Gilio]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: [WIP MLton 0/1] Add MLton --]
[-- Type: text/x-patch, Size: 851 bytes --]

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

[bug#38605] [WIP MLton 1/1] gnu: Add mlton.

[Brett Gilio]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: [WIP MLton 1/1] gnu: Add mlton. --]
[-- Type: text/x-patch, Size: 5302 bytes --]

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(+)

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

[bug#38605] [WIP MLton 0/1] Add MLton

[Ludovic Courtès]

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’.

[bug#38605] [WIP MLton 0/1] Add MLton

[zimoun]

Hi,

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

On Mon, 16 Dec 2019 at 11:03, Ludovic Courtès <ludo@gnu.org> 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

[bug#38605] [WIP MLton 0/1] Add MLton

[Brett Gilio]

Ludovic Courtès <ludo@gnu.org> writes:

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

-- 
Brett M. Gilio
Homepage -- https://scm.pw/
GNU Guix -- https://guix.gnu.org/

[bug#38605] [WIP MLton 0/1] Add MLton

[Ludovic Courtès]

Hi Brett,

Brett Gilio <brettg@posteo.net> 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
“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.

> 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
<https://www.macs.hw.ac.uk/ultra/skalpel/html/sml.html>.

> 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’.

[bug#38605] [WIP MLton 0/1] Add MLton

[Ludovic Courtès]

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’.

[bug#38605] [WIP MLton 0/1] Add MLton

[Brett Gilio]

Ludovic Courtès <ludo@gnu.org> writes:

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

[bug#38605] [WIP MLton 0/1] Add MLton

[zimoun]

Hi Brett,

Thank you for the explanations.

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". :-)


[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

[bug#38605] [WIP MLton 0/1] Add MLton

[Ludovic Courtès]

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’.

[bug#38605] [WIP MLton 0/1] Add MLton

[Brett Gilio]

Ludovic Courtès <ludo@gnu.org> writes:

> 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>

[bug#38605] [WIP MLton 1/1] gnu: Add mlton.

[zimoun]

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:
>>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?


> 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

[bug#38605] [WIP MLton 0/1] Add MLton

[zimoun]

Hi,

CC: guix-devel

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>


> 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?


>> 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

bug#38605: [WIP MLton 0/1] Add MLton

[zimoun]

Hi,

On Tue, 12 Apr 2022 at 12:21, zimoun <zimon.toutoune@gmail.com> wrote:
> 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