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

[Brett Gilio]

Ludovic Courtès <address@hidden> writes:

> Hi Brett,
>
> Brett Gilio <address@hidden> 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/