You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
410 lines
11 KiB
410 lines
11 KiB
commit 35216e78de99558a39b147bf06fef85e1aabb2c6
|
|
Author: Rob Simmons <robsimmons@gmail.com>
|
|
Date: Mon Aug 19 11:49:04 2013 -0400
|
|
|
|
Transfer Mlton build over to mlb files, as they've been asking us to do for years and now insist on.
|
|
|
|
diff --git a/Makefile b/Makefile
|
|
index 9d7d422..2422f36 100644
|
|
--- a/Makefile
|
|
+++ b/Makefile
|
|
@@ -46,9 +46,9 @@ twelf-server-announce:
|
|
twelf-server-mlton:
|
|
mltonversion=`$(mlton) 2>&1 | awk 'NR==1 { print 0+$$2 }'`; \
|
|
if [ $$mltonversion -ge 20041109 ]; then \
|
|
- cmfileid="twelf-server-mlton.cm"; \
|
|
+ cmfileid="twelf-server-mlton.mlb"; \
|
|
elif [ $$mltonversion="MLTONVERSION" ]; then \
|
|
- cmfileid="twelf-server-mlton.cm"; \
|
|
+ cmfileid="twelf-server-mlton.mlb"; \
|
|
else \
|
|
echo; echo "Error: MLton >= 20041109 required"; echo; \
|
|
exit 1; \
|
|
@@ -84,7 +84,7 @@ mlton : twelf-server-announce buildid twelf-server-mlton twelf-emacs
|
|
|
|
.PHONY: twelf-regression check
|
|
twelf-regression: buildid
|
|
- $(mlton) -output bin/twelf-regression TEST/mlton-regression.cm
|
|
+ $(mlton) -output bin/twelf-regression TEST/mlton-regression.mlb
|
|
|
|
check : twelf-regression
|
|
$(make) -C TEST check
|
|
diff --git a/TEST/mlton-regression.mlb b/TEST/mlton-regression.mlb
|
|
new file mode 100644
|
|
index 0000000..b77a9ee
|
|
--- /dev/null
|
|
+++ b/TEST/mlton-regression.mlb
|
|
@@ -0,0 +1,7 @@
|
|
+(* MLton version *)
|
|
+
|
|
+../build/twelf-core-mlton.mlb
|
|
+
|
|
+regression.sml
|
|
+runquiet.sml
|
|
+
|
|
diff --git a/build/twelf-core-mlton.mlb b/build/twelf-core-mlton.mlb
|
|
new file mode 100644
|
|
index 0000000..26843cd
|
|
--- /dev/null
|
|
+++ b/build/twelf-core-mlton.mlb
|
|
@@ -0,0 +1,348 @@
|
|
+(* Common MLton version *)
|
|
+
|
|
+$(SML_LIB)/basis/basis.mlb
|
|
+$(SML_LIB)/basis/mlton.mlb
|
|
+$(SML_LIB)/basis/sml-nj.mlb
|
|
+
|
|
+../src/compat/array.sig
|
|
+../src/compat/vector.sig
|
|
+../src/compat/path.sig
|
|
+../src/compat/substring.sig
|
|
+../src/compat/text-io.sig
|
|
+../src/compat/timer.sig
|
|
+../src/compat/socket.sig
|
|
+../src/compat/compat.sig
|
|
+../src/compat/socket.sml
|
|
+../src/compat/compat.fun
|
|
+../src/compat/compat.sml
|
|
+../src/timing/timing.sml
|
|
+../src/timing/timers.sig
|
|
+../src/timing/timers.fun
|
|
+../src/timing/timers.sml
|
|
+../src/global/global.sig
|
|
+../src/global/global.sml
|
|
+../src/lambda/fgnopn.sig
|
|
+../src/lambda/fgnopntable.fun
|
|
+../src/lambda/intsyn.sig
|
|
+../src/lambda/intsyn.fun
|
|
+../src/lambda/whnf.sig
|
|
+../src/lambda/whnf.fun
|
|
+../src/lambda/conv.sig
|
|
+../src/lambda/conv.fun
|
|
+
|
|
+../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/order/order.sig
|
|
+../src/order/order.fun
|
|
+../src/order/order.sml
|
|
+
|
|
+../src/lambda/tomega.sig
|
|
+../src/lambda/tomega.fun
|
|
+../src/lambda/tomega.sml
|
|
+../src/paths/paths.sig
|
|
+../src/paths/paths.fun
|
|
+../src/paths/origins.sig
|
|
+../src/paths/origins.fun
|
|
+../src/paths/paths.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/trail/trail.sig
|
|
+../src/trail/notrail.sml
|
|
+../src/trail/trail.sml
|
|
+../src/lambda/constraints.sig
|
|
+../src/lambda/constraints.fun
|
|
+../src/lambda/unify.sig
|
|
+../src/lambda/unify.fun
|
|
+../src/lambda/match.sig
|
|
+../src/lambda/match.fun
|
|
+../src/lambda/abstract.sig
|
|
+../src/lambda/abstract.fun
|
|
+../src/lambda/approx.sig
|
|
+../src/lambda/approx.fun
|
|
+../src/lambda/lambda.sml
|
|
+../src/names/names.sig
|
|
+../src/names/names.fun
|
|
+../src/names/names.sml
|
|
+../src/style/style.sig
|
|
+../src/style/style.fun
|
|
+../src/style/style.sml
|
|
+../src/stream/stream.sml
|
|
+../src/frontend/lexer.sig
|
|
+../src/frontend/lexer.fun
|
|
+../src/frontend/twelf.sig
|
|
+../src/formatter/formatter.sig
|
|
+../src/formatter/formatter.fun
|
|
+../src/formatter/formatter.sml
|
|
+../src/print/print-omdoc.sig
|
|
+../src/print/print-xml.sig
|
|
+../src/print/print-omdoc.fun
|
|
+../src/print/print-xml.fun
|
|
+../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/modes/modesyn.sml
|
|
+../src/modes/modetable.sig
|
|
+../src/modes/modetable.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/intset.sml
|
|
+../src/subordinate/subordinate.sig
|
|
+../src/subordinate/subordinate.fun
|
|
+../src/subordinate/subordinate.sml
|
|
+../src/solvers/cs-manager.sig
|
|
+../src/solvers/cs-manager.fun
|
|
+../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.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/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/table/red-black-set.sig
|
|
+../src/table/red-black-set.sml
|
|
+../src/compile/compsyn.sig
|
|
+../src/compile/compsyn.fun
|
|
+../src/compile/cprint.sig
|
|
+../src/compile/cprint.fun
|
|
+../src/compile/subtree.sig
|
|
+../src/compile/subtree.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/table-param.sig
|
|
+../src/opsem/table-param.fun
|
|
+../src/opsem/table-param.sml
|
|
+../src/opsem/abstract.sig
|
|
+../src/opsem/abstract.fun
|
|
+../src/opsem/sw-subtree.sig
|
|
+../src/opsem/subtree.fun
|
|
+../src/opsem/subtree-inst.fun
|
|
+../src/opsem/sw-subtree.fun
|
|
+../src/opsem/tabled.sig
|
|
+../src/opsem/tabled.fun
|
|
+../src/opsem/ptrecon.sig
|
|
+../src/opsem/ptrecon.fun
|
|
+../src/opsem/trace.sig
|
|
+../src/opsem/trace.fun
|
|
+../src/opsem/absmachine-sbt.sig
|
|
+../src/opsem/absmachine-sbt.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/compat/time-limit.sig
|
|
+../src/compat/time-limit.sml
|
|
+../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/funsyn.sig
|
|
+../src/meta/funsyn.fun
|
|
+../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/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/worldify.sig
|
|
+../src/worldcheck/worldify.fun
|
|
+../src/worldcheck/worldcheck.sml
|
|
+../src/unique/unique.sig
|
|
+../src/unique/unique.fun
|
|
+../src/unique/unique.sml
|
|
+../src/cover/cover.sig
|
|
+../src/cover/cover.fun
|
|
+../src/cover/total.sig
|
|
+../src/cover/total.fun
|
|
+../src/cover/cover.sml
|
|
+../src/tomega/abstract.sig
|
|
+../src/tomega/abstract.fun
|
|
+../src/tomega/tomegaprint.sig
|
|
+../src/tomega/tomegaprint.fun
|
|
+../src/tomega/typecheck.sig
|
|
+../src/tomega/typecheck.fun
|
|
+../src/tomega/opsem.sig
|
|
+../src/tomega/opsem.fun
|
|
+../src/tomega/redundant.sig
|
|
+../src/tomega/redundant.fun
|
|
+../src/tomega/converter.sig
|
|
+../src/tomega/converter.fun
|
|
+../src/tomega/coverage.sig
|
|
+../src/tomega/coverage.fun
|
|
+../src/tomega/tomega.sml
|
|
+../src/msg/msg.sml
|
|
+../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/parsing.sig
|
|
+../src/frontend/parsing.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/fquery.sig
|
|
+../src/frontend/fquery.fun
|
|
+../src/frontend/unknownexn.sig
|
|
+../src/frontend/buildid.sml
|
|
+../src/frontend/version.sml
|
|
+../src/frontend/twelf.fun
|
|
+../src/frontend/unknownexn.fun
|
|
+../src/frontend/unknownexn-smlnj.sml
|
|
+../src/frontend/frontend.sml
|
|
+../src/server/sigint.sig
|
|
+../src/server/sigint-mlton.sml
|
|
+../src/server/server.sml
|
|
diff --git a/build/twelf-server-mlton.mlb b/build/twelf-server-mlton.mlb
|
|
new file mode 100644
|
|
index 0000000..fa4332f
|
|
--- /dev/null
|
|
+++ b/build/twelf-server-mlton.mlb
|
|
@@ -0,0 +1,4 @@
|
|
+
|
|
+twelf-core-mlton.mlb
|
|
+twelf-server-mlton.sml
|
|
+
|
|
|