upcoming release

Matthew Fluet fluet@CS.Cornell.EDU
Mon, 1 Apr 2002 08:16:53 -0500 (EST)


> * [all] decide what to do about libgmp.  Currently, we do not include
>   libgmp in our binary rpm.  How much pain might this cause users?
>   Should we include it and check at install or compile time?  Should
>   we just put a note in the docs?  Any other ideas?

I would not include it in the binary (or source) rpms.  It's a dependency,
which should be expressible in the rpms.  I would include a note in the
docs.
We might also put a note in the docs that says modifying the /bin/mlton
script to include a -L option to the libgmp directory might be necessary.
When I first tried out the latest GMP, I installed it in /usr/local/lib,
so mlton (or, more accurately, ld) never found it until I hacked the mlton
script to look in the right place.

Another idea is a supplementary binary rpm that just adds libgmp to the
mlton/lib directory.