Compiling caml-light for the Mac

Compiling caml-light for the Mac

[Richard Bornat]

Bernard Sufrin and I have a proof editor - Jape - which was written in
SML/NJ for SunOS and A/UX.  I want to port it to MacOS now, and to
Windows-based PCs as soon as maybe.

I have already translated it into Moscow ML, and am enormously impressed by
the speed of translation, the small size of the bytecodes, and so on.  But
speed of execution is disappointing - about six times slower than NJ.  This
doesn't matter most of the time, when the user is making small proof steps,
because all they see is a slightly longer delay between steps.  But we have
some compute-intensive phases - for example, reading in a file of
previously completed proofs and re-incorporating them into the system -
where speed is essential.

Mosml 1.30 isn't yet available for the Mac, though I know it's coming.
Caml-light is ready, and it has compilation tools, and a profiler, and a
large body of users, and I don't know what other wonderful features. To
move now from Moscow ML to caml-light would be a relatively small step.  I
could even do it mechanically, as a first approximation. But would that
make it possible to compile my program into fast-running C on the Mac? on
Windows PC? or fast-running anything on either?  I note that both camlot
and camloo/bigloo know nothing about the alien environment of the Mac.  Is
the C they produce Mac-friendly, or is it very difficult to make it fit?

So far as I know, nobody has experience of caml-light -> C for the Mac.  (I
should be delighted to be contradicted on this point!).

I have MPW and CodeWarrior for MacOS.  I could run camlot / camloo on a Sun
and, through the miracle of fileserving, compile it with the Mac tools.

Richard Bornat                          Department of Computer Science
richard@dcs.qmw.ac.uk                   Queen Mary and Westfield College
phone (+44) 171 975 5206 direct line    Mile End Road
      (+44) 171 975 5200 department     LONDON E1 4NS
fax   (+44) 181 980 6533 department     UK