[MLton-devel] Re: Twelf benchmark

[Stephen Weeks]

> It depends on which verson of Twelf you are using.

I grabbed 1.3R4 from twelf.org.

> We now have large developments in Twelf.  Andrew Appel has about
> 100K lines of Twelf source formalizating foundational PCC, and test
> suites that run between minutes and hours.
> 
> Karl Crary has a formalization of Typed Assembly Language in Twelf
> that runs about a minute.
>
> Both of these require relatively recent features of Twelf.

Either of those would be great.  Will they run with 1.3R4?  Do you
have them handy?

> By the way, I would be interested in maintaining the Twelf source
> in a manner so that it can be compiled under MLton as well as
> SML/NJ.  Do you have a suggestion for the best way to do this?

Yes.  It's not too hard, since that's how we develop MLton itself.
Once I get the twelf benchmark built I'll send a patch file for the
1.3R4 tgz to show you exactly what I had to do to make it work.  In
the meantime, here's a rough overview.

You can use cmcat, a tool that comes with MLton, to turn your CM file 
into an ordered list of all the files in your project, which can then
be fed as a simple CM file to MLton.  For the places where there are
differences (e.g. int-inf and signals), you can use a CM #if statement
to get the right code for each compiler.  For example, I changed
src/server/sources.cm to the following.

----------------------------------------
Group is
  ../frontend/sources.cm
  sigint.sig
  sigint-any.sml
  #if (defined (MLton))
  sigint-mlton.sml
  #else
  sigint-smlnj.sml
  #endif
  server.sml
----------------------------------------

Then, the following lines in the Makefile were enough so I could do
"make cm mlton-server' to build the project.

----------------------------------------

MLTON=mlton
NAME=mlton-server
FLAGS=-v

$(NAME): $(NAME).cm $(shell $(MLTON) -stop f $(NAME).cm)
	@echo 'Compiling $(NAME)'
	time $(MLTON) $(FLAGS) $(NAME).cm
	size $(NAME)

$(NAME).sml: $(NAME).cm $(shell $(MLTON) -stop f $(NAME).cm)
	mlton -stop sml $(NAME).cm

.PHONY:	cm
cm: 
	(								\
		echo 'Group is' &&					\
		echo 'src/mlton-stubs.sml' &&				\
		cmcat -DMLton server.cm &&				\
		echo 'src/mlton-main.sml';				\
	) >$(NAME).cm

----------------------------------------


-------------------------------------------------------
This sf.net email is sponsored by:
With Great Power, Comes Great Responsibility 
Learn to use your power at OSDN's High Performance Computing Channel
http://hpc.devchannel.org/
_______________________________________________
MLton-devel mailing list
MLton-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/mlton-devel