[MLton-devel] Re: Twelf benchmark

Stephen Weeks MLton@mlton.org
Sat, 14 Dec 2002 13:30:02 -0800


> P.S.: It would help if you could send me the diffs, or MLton specific
> files so I do not replicate the work that you already did.

Here's where I currently am.  It might be easier for you to just use
mlton-server.cm rather than figure out how to install cmcat, which
requires older versions of SML/NJ.

For int-inf, I commented out your implementation, since MLton,
Poly/ML, and SML/NJ all have it (and with wildly different
performance).

For the signals stuff, MLton has replacements for the SML/NJ stuff,
but conts/threads/signals are not super-well tested in MLton.  Please
let us know about problems.  Also, MLton's basis library will raise
SysErr with EINTR when a system call like read is interrupted by a
signal, rather than restart the call.  So, I needed to patch your
getLine function.  MLton's library will hopefully someday
automatically restart the call.

In any case, for the benchmark, I plan to make a single file that
works on all compilers, so I'll cut out the signals stuff anyways.

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

% diff -N -u -r twelf twelf-new
diff -N -u -r twelf/Makefile twelf-new/Makefile
--- twelf/Makefile	Mon Oct 16 07:28:12 2000
+++ twelf-new/Makefile	Sat Dec 14 13:16:20 2002
@@ -17,6 +17,33 @@
 
 version = "1.3"
 
+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: clean-mlton
+clean-mlton:
+	rm -f $(NAME) $(NAME).sml
+	find . -type d | grep '/CM$$' | xargs rm -rf
+	find . -type f | grep '~$$' | xargs rm -rf
+
+.PHONY:	cm
+cm: 
+	(								\
+		echo 'Group is' &&					\
+		echo 'src/mlton-stubs.sml' &&				\
+		cmcat -DMLton server.cm &&				\
+		echo 'src/mlton-main.sml';				\
+	) >$(NAME).cm
+
 default : twelf-server twelf-emacs
 
 all : twelf-server twelf-sml twelf-emacs
diff -N -u -r twelf/mlton-server.cm twelf-new/mlton-server.cm
--- twelf/mlton-server.cm	Wed Dec 31 16:00:00 1969
+++ twelf-new/mlton-server.cm	Thu Dec 12 22:40:19 2002
@@ -0,0 +1,279 @@
+Group is
+src/mlton-stubs.sml
+src/lambda/intsyn.sig
+src/lambda/whnf.sig
+src/names/names.sig
+src/print/traverse.sig
+src/print/traverse.fun
+src/meta/funsyn.sig
+src/meta/interpret.sig
+src/timing/timing.sml
+src/timing/timers.sig
+src/timing/timers.fun
+src/timing/timers.sml
+src/stream/stream.sml
+src/paths/paths.sig
+src/frontend/lexer.sig
+src/frontend/twelf.sig
+src/global/global.sig
+src/global/global.sml
+src/trail/trail.sig
+src/trail/notrail.sml
+src/trail/trail.sml
+src/lambda/intsyn.fun
+src/lambda/whnf.fun
+src/lambda/conv.sig
+src/lambda/conv.fun
+src/lambda/constraints.sig
+src/lambda/constraints.fun
+src/lambda/unify.sig
+src/lambda/unify.fun
+src/lambda/abstract.sig
+src/lambda/abstract.fun
+src/lambda/approx.sig
+src/lambda/approx.fun
+src/lambda/lambda.sml
+src/table/table.sig
+src/table/hash-table.sml
+src/table/string-hash.sig
+src/table/string-hash.sml
+src/table/red-black-tree.fun
+src/table/sparse-array.sig
+src/table/sparse-array.fun
+src/table/sparse-array2.sig
+src/table/sparse-array2.fun
+src/table/table.sml
+src/names/names.fun
+src/names/names.sml
+src/paths/paths.fun
+src/paths/origins.sig
+src/paths/origins.fun
+src/paths/paths.sml
+src/formatter/formatter.sig
+src/formatter/formatter.fun
+src/formatter/formatter.sml
+src/print/print-twega.sig
+src/print/print-twega.fun
+src/print/symbol.sig
+src/print/symbol.fun
+src/print/print.sig
+src/print/print.fun
+src/print/clause-print.sig
+src/print/clause-print.fun
+src/print/print.sml
+src/typecheck/strict.sig
+src/typecheck/strict.fun
+src/typecheck/typecheck.sig
+src/typecheck/typecheck.fun
+src/typecheck/typecheck.sml
+src/table/queue.sig
+src/table/queue.sml
+src/index/index.sig
+src/index/index.fun
+src/index/index-skolem.fun
+src/index/index.sml
+src/modes/modesyn.sig
+src/modes/modesyn.fun
+src/modes/modedec.sig
+src/modes/modedec.fun
+src/modes/modecheck.sig
+src/modes/modecheck.fun
+src/modes/modeprint.sig
+src/modes/modeprint.fun
+src/modes/modes.sml
+src/tabling/tabledsyn.sig
+src/tabling/tabledsyn.fun
+src/tabling/tabled.sml
+src/subordinate/subordinate.sig
+src/subordinate/subordinate.fun
+src/subordinate/subordinate.sml
+src/domains/integers.sig
+src/domains/integers.fun
+src/domains/field.sig
+src/domains/ordered-field.sig
+src/domains/rationals.sig
+src/domains/rationals.fun
+src/domains/integers-mod.fun
+src/domains/domains.sml
+src/solvers/cs-manager.sig
+src/solvers/cs-manager.fun
+src/solvers/cs.sig
+src/solvers/cs-eq-field.sig
+src/solvers/cs-eq-field.fun
+src/solvers/cs-ineq-field.fun
+src/solvers/cs-eq-strings.fun
+src/solvers/cs-eq-bools.fun
+src/solvers/cs-eq-integers.sig
+src/solvers/cs-eq-integers.fun
+src/solvers/cs-ineq-integers.fun
+src/solvers/cs-integers-word.fun
+src/solvers/solvers.sml
+src/order/order.sig
+src/order/order.fun
+src/order/order.sml
+src/terminate/checking.sig
+src/terminate/checking.fun
+src/terminate/reduces.sig
+src/terminate/reduces.fun
+src/terminate/terminate.sml
+src/thm/thmsyn.sig
+src/thm/thmsyn.fun
+src/thm/thmprint.sig
+src/thm/thmprint.fun
+src/thm/thm.sig
+src/thm/thm.fun
+src/thm/thm.sml
+src/compile/compsyn.sig
+src/compile/compsyn.fun
+src/compile/cprint.sig
+src/compile/cprint.fun
+src/compile/compile.sig
+src/compile/compile.fun
+src/compile/assign.sig
+src/compile/assign.fun
+src/compile/compile.sml
+src/opsem/absmachine.sig
+src/opsem/absmachine.fun
+src/opsem/ptrecon.sig
+src/opsem/ptrecon.fun
+src/opsem/abstract.sig
+src/opsem/abstract.fun
+src/opsem/index.sig
+src/opsem/index.fun
+src/opsem/tabled.sig
+src/opsem/tabled.fun
+src/opsem/trace.sig
+src/opsem/trace.fun
+src/opsem/tmachine.fun
+src/opsem/swmachine.fun
+src/opsem/opsem.sml
+src/m2/meta-global.sig
+src/m2/meta-global.sml
+src/table/ring.sig
+src/table/ring.sml
+src/m2/metasyn.sig
+src/m2/metasyn.fun
+src/m2/meta-abstract.sig
+src/m2/meta-abstract.fun
+src/m2/meta-print.sig
+src/m2/meta-print.fun
+src/m2/init.sig
+src/m2/init.fun
+src/m2/search.sig
+src/m2/search.fun
+src/m2/lemma.sig
+src/m2/lemma.fun
+src/m2/splitting.sig
+src/m2/splitting.fun
+src/m2/filling.sig
+src/m2/filling.fun
+src/m2/recursion.sig
+src/m2/recursion.fun
+src/m2/qed.sig
+src/m2/qed.fun
+src/m2/strategy.sig
+src/m2/strategy.fun
+src/m2/prover.sig
+src/m2/prover.fun
+src/m2/mpi.sig
+src/m2/mpi.fun
+src/m2/skolem.sig
+src/m2/skolem.fun
+src/m2/m2.sml
+src/modules/modsyn.sig
+src/modules/modsyn.fun
+src/modules/modules.sml
+src/heuristic/heuristic.sig
+src/heuristic/heuristic.sum.fun
+src/meta/global.sig
+src/meta/statesyn.sig
+src/meta/init.sig
+src/meta/strategy.sig
+src/meta/relfun.sig
+src/meta/prover.fun
+src/meta/funprint.sig
+src/meta/print.sig
+src/meta/print.fun
+src/meta/filling.sig
+src/meta/data.sig
+src/meta/splitting.sig
+src/meta/recursion.sig
+src/meta/inference.sig
+src/meta/strategy.fun
+src/meta/statesyn.fun
+src/meta/funtypecheck.sig
+src/meta/uniquesearch.sig
+src/meta/inference.fun
+src/meta/abstract.sig
+src/meta/splitting.fun
+src/meta/uniquesearch.fun
+src/meta/search.sig
+src/meta/search.fun
+src/meta/recursion.fun
+src/meta/mpi.sig
+src/meta/mpi.fun
+src/meta/data.fun
+src/meta/global.fun
+src/meta/filling.fun
+src/meta/init.fun
+src/meta/abstract.fun
+src/meta/funsyn.fun
+src/meta/funnames.sig
+src/meta/funnames.fun
+src/meta/funprint.fun
+src/meta/weaken.sig
+src/meta/weaken.fun
+src/meta/funweaken.sig
+src/meta/funweaken.fun
+src/meta/funtypecheck.fun
+src/meta/relfun.fun
+src/meta/meta.sml
+src/worldcheck/worldsyn.sig
+src/worldcheck/worldsyn.fun
+src/worldcheck/worldprint.sig
+src/worldcheck/worldprint.fun
+src/worldcheck/worldcheck.sml
+src/cover/cover.sig
+src/cover/cover.fun
+src/cover/total.sig
+src/cover/total.fun
+src/cover/cover.sml
+src/frontend/lexer.fun
+src/frontend/parsing.sig
+src/frontend/parsing.fun
+src/frontend/recon-term.sig
+src/frontend/recon-term.fun
+src/frontend/recon-condec.sig
+src/frontend/recon-condec.fun
+src/frontend/recon-query.sig
+src/frontend/recon-query.fun
+src/frontend/recon-mode.sig
+src/frontend/recon-mode.fun
+src/frontend/recon-thm.sig
+src/frontend/recon-thm.fun
+src/frontend/recon-module.sig
+src/frontend/recon-module.fun
+src/frontend/parse-term.sig
+src/frontend/parse-term.fun
+src/frontend/parse-condec.sig
+src/frontend/parse-condec.fun
+src/frontend/parse-query.sig
+src/frontend/parse-query.fun
+src/frontend/parse-fixity.sig
+src/frontend/parse-fixity.fun
+src/frontend/parse-mode.sig
+src/frontend/parse-mode.fun
+src/frontend/parse-thm.sig
+src/frontend/parse-thm.fun
+src/frontend/parse-module.sig
+src/frontend/parse-module.fun
+src/frontend/parser.sig
+src/frontend/parser.fun
+src/frontend/solve.sig
+src/frontend/solve.fun
+src/frontend/twelf.fun
+src/frontend/frontend.sml
+src/server/sigint.sig
+src/server/sigint-any.sml
+src/server/server.sml
+src/mlton-main.sml
diff -N -u -r twelf/src/int-inf/sources.cm twelf-new/src/int-inf/sources.cm
--- twelf/src/int-inf/sources.cm	Sun Sep 24 08:01:31 2000
+++ twelf-new/src/int-inf/sources.cm	Tue Dec 10 17:31:19 2002
@@ -1,3 +1,3 @@
 Group is
-  int-inf-sig.sml
-  int-inf.sml
+(* int-inf-sig.sml *)
+(*  int-inf.sml *)
diff -N -u -r twelf/src/mlton-main.sml twelf-new/src/mlton-main.sml
--- twelf/src/mlton-main.sml	Wed Dec 31 16:00:00 1969
+++ twelf-new/src/mlton-main.sml	Tue Dec 10 17:57:11 2002
@@ -0,0 +1,4 @@
+val _ =
+   OS.Process.exit
+   (Server.server (CommandLine.name (),
+		   CommandLine.arguments ()))
diff -N -u -r twelf/src/mlton-stubs.sml twelf-new/src/mlton-stubs.sml
--- twelf/src/mlton-stubs.sml	Wed Dec 31 16:00:00 1969
+++ twelf-new/src/mlton-stubs.sml	Tue Dec 10 17:53:44 2002
@@ -0,0 +1,12 @@
+structure OS =
+   struct
+      open OS
+
+      structure Path =
+	 struct
+	    open Path
+
+	    fun mkAbsolute (p, d) =
+	       Path.mkAbsolute {path = p, relativeTo = d}
+	 end
+   end
diff -N -u -r twelf/src/server/server.sml twelf-new/src/server/server.sml
--- twelf/src/server/server.sml	Wed Apr 17 23:13:28 2002
+++ twelf-new/src/server/server.sml	Tue Dec 10 18:15:17 2002
@@ -20,7 +20,10 @@
   *)
   fun readLine () =
       let
-        val line = TextIO.inputLine (TextIO.stdIn)
+	 fun getLine () =
+	    TextIO.inputLine (TextIO.stdIn)
+	    handle OS.SysErr (_, SOME _) => getLine ()
+        val line = getLine ()
         fun triml ss = Substring.dropl Char.isSpace ss
         fun trimr ss = Substring.dropr Char.isSpace ss
         val line' = triml (trimr (Substring.all line))
diff -N -u -r twelf/src/server/sigint-any.sml twelf-new/src/server/sigint-any.sml
--- twelf/src/server/sigint-any.sml	Wed Dec 31 16:00:00 1969
+++ twelf-new/src/server/sigint-any.sml	Thu Dec 12 22:39:53 2002
@@ -0,0 +1,6 @@
+structure SigINT:> SIGINT =
+struct
+
+fun interruptLoop (loop:unit -> unit) = loop ()
+   
+end
diff -N -u -r twelf/src/server/sigint-mlton.sml twelf-new/src/server/sigint-mlton.sml
--- twelf/src/server/sigint-mlton.sml	Wed Dec 31 16:00:00 1969
+++ twelf-new/src/server/sigint-mlton.sml	Sat Dec 14 13:17:20 2002
@@ -0,0 +1,17 @@
+structure SigINT :> SIGINT =
+struct
+
+  fun interruptLoop (loop:unit -> unit) =
+     let
+	open MLton
+	val _ =
+	   Cont.callcc
+	   (fn k =>
+	    Signal.handleWith'
+	    (Signal.int, fn _ =>
+	     Thread.new (fn () => Cont.throw (k, ()))))
+     in
+	loop ()
+     end
+
+end;  (* structure SigINT *)
diff -N -u -r twelf/src/server/sources.cm twelf-new/src/server/sources.cm
--- twelf/src/server/sources.cm	Sat Sep  5 15:59:40 1998
+++ twelf-new/src/server/sources.cm	Fri Dec 13 18:03:19 2002
@@ -1,5 +1,10 @@
 Group is
   ../frontend/sources.cm
   sigint.sig
+  sigint-any.sml
+  #if (defined (MLton))
+  sigint-mlton.sml
+  #else
   sigint-smlnj.sml
+  #endif
   server.sml
diff -N -u -r twelf/src/solvers/solvers.sml twelf-new/src/solvers/solvers.sml
--- twelf/src/solvers/solvers.sml	Wed Feb 13 16:03:46 2002
+++ twelf-new/src/solvers/solvers.sml	Tue Dec 10 17:32:32 2002
@@ -51,6 +51,7 @@
                                    structure Unify = UnifyTrail
                                    structure CSManager = CSManager);
 
+val _ = (
 CSManager.installSolver (CSEqQ.solver);
 CSManager.installSolver (CSIneqQ.solver);
 CSManager.installSolver (CSEqStrings.solver);
@@ -58,3 +59,5 @@
 CSManager.installSolver (CSEqZ.solver);
 CSManager.installSolver (CSIneqZ.solver);
 CSManager.installSolver (CSIntWord32.solver);
+()
+)


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