diff options
Diffstat (limited to 'sci-mathematics/twelf')
| -rw-r--r-- | sci-mathematics/twelf/Manifest | 12 | ||||
| -rw-r--r-- | sci-mathematics/twelf/files/50twelf-gentoo.el | 4 | ||||
| -rw-r--r-- | sci-mathematics/twelf/files/twelf-1.7.1-Makefile.patch | 43 | ||||
| -rw-r--r-- | sci-mathematics/twelf/files/twelf-1.7.1-doc-guide-Makefile.patch | 13 | ||||
| -rw-r--r-- | sci-mathematics/twelf/files/twelf-1.7.1-doc-guide-twelf-dot-texi.patch | 14 | ||||
| -rw-r--r-- | sci-mathematics/twelf/files/twelf-1.7.1-emacs-twelf-init.patch | 22 | ||||
| -rw-r--r-- | sci-mathematics/twelf/files/twelf-1.7.1-emacs-twelf.patch | 11 | ||||
| -rw-r--r-- | sci-mathematics/twelf/files/twelf-1.7.1-mlton-mlb.patch | 409 | ||||
| -rw-r--r-- | sci-mathematics/twelf/metadata.xml | 13 | ||||
| -rw-r--r-- | sci-mathematics/twelf/twelf-1.7.1.ebuild | 111 |
10 files changed, 652 insertions, 0 deletions
diff --git a/sci-mathematics/twelf/Manifest b/sci-mathematics/twelf/Manifest new file mode 100644 index 000000000000..6b56bbe3c831 --- /dev/null +++ b/sci-mathematics/twelf/Manifest @@ -0,0 +1,12 @@ +AUX 50twelf-gentoo.el 104 SHA256 1d3382c18895a3f5a6b4c1aebc5d9fc2d2aa94a7c196d5b5ccc9a7bc27a1498d SHA512 b6bd1f73b2224c37f783d0b2cdb16cd4e5435280c7448fd7600398ab2806edb574ec4e811adf26bfc1fbc9d0c311dbb521022b2a9dacbfecfa1ffef488c764bb WHIRLPOOL dea650f36310f83a8b4d3ac51cebb19054e48279e589b4080fbd145f5678be2c0555f1594a28443eebe118873639abf933e58a5ac7f510b1c06397d8248876b5 +AUX twelf-1.7.1-Makefile.patch 1298 SHA256 77038dabdd5fc990d78cba18ce42f598a2ec5a94c85a38ff6e15b08b2517853a SHA512 ffc7c147790b180c50eb645b896ad86c35b771ad516d2a85998f8edfd0e1ff1db98d1880b6e8b02e4ddcf8f218761ab26ddfee9bd5ab876b3bd1caa6a3e0e78e WHIRLPOOL ef6e408c659284ea647692fd73dfb9512138ec1287364bd59fac255e7ae6fcec1ac94233c5fd2e695bf03ee73a7b2607d1e00437d97815f8fe3c4d6dc0bebcfa +AUX twelf-1.7.1-doc-guide-Makefile.patch 498 SHA256 1a71e3686e1d84afbccb39649b1fdcc44a44bc458fd4ede2f323ee7b12a4dc30 SHA512 240192028c9dd9a953ff9778bc9753a08dffa0f3332b72d4d2cd64a594f32fb183092ce1a4ace9fe9e0123d469be50983e4d081db989165beba33212de74b3d0 WHIRLPOOL 62ffc47f3448b75325f051f62a7b2ef7bf60293927f1d7b16a3d441481c9e18602a5c56e8bbaaa51d5c0a33ec5b574a1887f10ee923b241156ec8f3c1e3c9a52 +AUX twelf-1.7.1-doc-guide-twelf-dot-texi.patch 386 SHA256 a21601d5ee953358fc155a96a0167b3fefae2deea9074f7bd53af287836c6df8 SHA512 60741e8df6e2b200f22c435ccf2d092624b601ad71ffc1a3388e9ae1bca6ef0d92092940075d9786efed6218d82cf1a344d3a433eabbdabe2514ff985a6948b7 WHIRLPOOL 1323969b3f369de40e4f6d73b1832e7e4dc3c022fefecf00a6c90ff5bc17cdbe345e66d530589751f87f823c035e72e55ed05d3beaf58aa742e2866db64c57fa +AUX twelf-1.7.1-emacs-twelf-init.patch 813 SHA256 e3f2ffa9dc7e6c1d05a23ede172199a005411be3061e3d3dab65fcb126db4afe SHA512 b45415b57dee44da7a38ea1f40b58526f0f69d012a16c316ebd6c3c9c856bbffd270f034d172b4ddeb083b7289c87eabf805a96fc9475f501038fb6c85a0f571 WHIRLPOOL c48647209e071b8795fdfb8be44c8397ed814a219dba58801cccb82626025ea1b6132289f63b9d475162df3ab0365b88f38e6b797d557047872e1e9c1e0f6aff +AUX twelf-1.7.1-emacs-twelf.patch 602 SHA256 30a8fca3da1b64d06ecb7572c62f832fba7cb2c329d73f86aa74714eba8527ef SHA512 e5fd550210b7107fdafc27906dcb22318d1b0b6044d2502cfb968fb3b5d4baca5535cd6ae995638f38395d08641e59f5b87c76eac190653a6dad89bf52eb1a97 WHIRLPOOL 647290f3c6a42e5075baa78e6683a496b6e0472e0346e4ad85d91978f09c1d1137864452f7993e2a6bb99a6b24f4615099c4e8d09aa95deb53af483de37a6006 +AUX twelf-1.7.1-mlton-mlb.patch 11244 SHA256 cde36be7fa9c21871926cc772b3b16fcf0a8b842ee55f9d78f3f875a0927491a SHA512 2d0f42399e444cbb736f38ad7bdc54f51322c17c010b273c365d9db9a1e6c045c19b872d4b5c1e50444559a981aa5569764ac859c7702c116c97c935fd959bfd WHIRLPOOL 1ca8368e5b4a96a0e175b496f8958782f1b4ecfcd4e49c024f8e6f2f711ac4e4db6e615431facc6b3d7a09137f0a6ac26de5fa690c4daaa9add8434d1579ad06 +DIST twelf-src-1.7.1.tar.gz 1147610 SHA256 91b0d4d8c2e54452a042da0ff642f3b46b25efb36a84497aa8b96598f49a213a SHA512 1b4baa0f385b6b605583a9da312f23c775aab43e7398c6e151833a6b95c74112492530f44fcb7b14f8288774e9b63e2f9618a5debfbc4d34737bc2588f5850df WHIRLPOOL 231879beb66ff143acd3245c10b5e25a91994e67eb3b12aedd0e5a2378a94a2e1f3b29953b1ea24e98ca0063f27aff662cfdd1cea01163be435a6dbba1f0d2b9 +EBUILD twelf-1.7.1.ebuild 2330 SHA256 df29280fc8002cbfa4a70442b45f1b9920f8350df1272643b1014ff1b54e18b5 SHA512 e8554e14b6f5f87e1a7f810ec62d6e1e3e597944a98ee322fc022ce922331e1d0e39b7d910e1ec7ea8f6a2de079f6940f3e4dc7fc53fe5f4354dda3bba38b170 WHIRLPOOL 3fb36341f6ad2015983c0e6ce3351e0049a129b244b511227fd5c07f6e5ea2cef5aa5cef8edfafaaa3de99b8c9b44e13ad7378abf19d01138b15480f20a5b8ad +MISC ChangeLog 2772 SHA256 335e0af993594354b845f928caa66388c4b0cfce793ecff42edafc56742d7c9d SHA512 199ba29e04cd19a314a7c78c51d5da85d68c25a216ee4a6cde87f7f9427303255e8a1e78fc8439742a0d9ac5839c861f3969fc54d37260e8426756cf37f3a592 WHIRLPOOL 1bc9b5525c1b8d42d55a5d39ac16291c75f1ec2d567353878f9e911c5f5f457b542b44c23e3186be0b75384b8c93327060bbd8fd0cca577ee2f0852b73aad74c +MISC ChangeLog-2015 1479 SHA256 85abc565d663b5e5f26929a0a48db1449bc698a9fa7d4d2a74e0d68e6943b85d SHA512 1de52ef8577cb4bf9e1b8d4b4431aa143643d9008110875a944ecf4a23154e63fa589479f62ea59578880ac66601e00a4b78214d71f0c7b119a1c35ddf7c7a5b WHIRLPOOL 8137d222cfb3d29763d257a5c821a21ec788da579019b3505a60cde24f1c79052994a772541b92f8b6e77228e14d6402928d8a666b0e052a1393ec914a7c3309 +MISC metadata.xml 446 SHA256 2eac2599f3b96078a4a05bee31e00c6187c0270a875362ed515a3b60aa11c0da SHA512 7fcca73104456672c8e262129cdcc232073d6d0a4cd48d6593734646a3611ac6056325cc88be5c3a3585d67bc76fa9fb663a0171df7b84612c56c0ec93bc0e2e WHIRLPOOL 390e4992cc9b66534d410f246dab9cf0f35d49ab2d4fa7886b50803a1a4625345de4bc8d1067cb0e8e51ed7db1a5749e17be1b81f239a0ddd3ac1fc43c862043 diff --git a/sci-mathematics/twelf/files/50twelf-gentoo.el b/sci-mathematics/twelf/files/50twelf-gentoo.el new file mode 100644 index 000000000000..5bda54b2f19a --- /dev/null +++ b/sci-mathematics/twelf/files/50twelf-gentoo.el @@ -0,0 +1,4 @@ +;;; twelf site-lisp configuration + +(setq twelf-root "@SITELISP@") +(add-to-list 'load-path "@SITELISP@") diff --git a/sci-mathematics/twelf/files/twelf-1.7.1-Makefile.patch b/sci-mathematics/twelf/files/twelf-1.7.1-Makefile.patch new file mode 100644 index 000000000000..84631f357d9d --- /dev/null +++ b/sci-mathematics/twelf/files/twelf-1.7.1-Makefile.patch @@ -0,0 +1,43 @@ +--- twelf-orig/Makefile 2011-03-03 09:41:47.000000000 +1100 ++++ twelf/Makefile 2012-12-10 00:19:52.255787064 +1100 +@@ -17,6 +17,18 @@ + twelfdir = `pwd` + twelfserver = twelf-server + ++ifdef CFLAGS ++ccopts=$(foreach cf,$(CFLAGS),-cc-opt $(cf)) ++else ++ccopts= ++endif ++ ++ifdef LDFLAGS ++linkopts=$(foreach lf,$(LDFLAGS),-link-opt $(lf)) ++else ++linkopts= ++endif ++ + # --------------------------------------------------------------- + # You should not need to edit beyond this point + # --------------------------------------------------------------- +@@ -53,12 +65,12 @@ + echo; echo "Error: MLton >= 20041109 required"; echo; \ + exit 1; \ + fi; \ +- $(mlton) -output bin/$(twelfserver) build/$${cmfileid} ++ $(mlton) $(ccopts) $(linkopts) -as-opt -Wa,--noexecstack -output bin/$(twelfserver) build/$${cmfileid} + + .PHONY: twelf-server-smlnj + twelf-server-smlnj: + $(smlnj) < build/twelf-server-smlnj.sml ; +- bin/.mkexec "$(smlnj)" "$(twelfdir)" twelf-server "$(twelfserver)" ; ++ bin/.mkexec "$(smlnj)" "$(twelfdir)" twelf-server "$(twelfserver)" "$(twelfexecdir)" ; + + .PHONY: twelf-emacs + twelf-emacs: ; +@@ -87,4 +99,4 @@ + $(mlton) -output bin/twelf-regression TEST/mlton-regression.cm + + check : twelf-regression +- $(make) -C TEST check +\ No newline at end of file ++ $(make) -C TEST check diff --git a/sci-mathematics/twelf/files/twelf-1.7.1-doc-guide-Makefile.patch b/sci-mathematics/twelf/files/twelf-1.7.1-doc-guide-Makefile.patch new file mode 100644 index 000000000000..092b12b20dc0 --- /dev/null +++ b/sci-mathematics/twelf/files/twelf-1.7.1-doc-guide-Makefile.patch @@ -0,0 +1,13 @@ +--- twelf-orig/doc/guide/Makefile 2002-09-24 13:59:23.000000000 +1000 ++++ twelf/doc/guide/Makefile 2012-12-10 00:51:02.758835185 +1100 +@@ -38,8 +38,8 @@ + + twelf_toc.html : twelf.texi; + @echo "---------- Creating HTML: twelf_*.html" +- $(texi2html) -menu -number -split_chapter twelf.texi; +- $(texi2html) -check *.html; ++ $(texi2html) -menu -number-sections -split_chapter twelf.texi; ++# $(texi2html) -check *.html; + + twelf.pdf : twelf.texi; + @echo "---------- Creating unindexed PDF: twelf.pdf" diff --git a/sci-mathematics/twelf/files/twelf-1.7.1-doc-guide-twelf-dot-texi.patch b/sci-mathematics/twelf/files/twelf-1.7.1-doc-guide-twelf-dot-texi.patch new file mode 100644 index 000000000000..877ecd60b710 --- /dev/null +++ b/sci-mathematics/twelf/files/twelf-1.7.1-doc-guide-twelf-dot-texi.patch @@ -0,0 +1,14 @@ +--- twelf-orig/doc/guide/twelf.texi 2004-04-01 04:26:38.000000000 +1000 ++++ twelf/doc/guide/twelf.texi 2012-12-08 21:14:17.026139996 +1100 +@@ -12,6 +12,11 @@ + @syncodeindex fn cp + @c %**end of header + ++@dircategory Programming ++@direntry ++* Twelf User Guide: (twelf). The Twelf User's Guide. ++@end direntry ++ + @titlepage + @title Twelf User's Guide + @subtitle Version @value{VERSION} diff --git a/sci-mathematics/twelf/files/twelf-1.7.1-emacs-twelf-init.patch b/sci-mathematics/twelf/files/twelf-1.7.1-emacs-twelf-init.patch new file mode 100644 index 000000000000..983c3c2290ed --- /dev/null +++ b/sci-mathematics/twelf/files/twelf-1.7.1-emacs-twelf-init.patch @@ -0,0 +1,22 @@ +--- twelf-orig/emacs/twelf-init.el 2002-12-28 16:15:42.000000000 +1100 ++++ twelf/emacs/twelf-init.el 2012-12-10 00:45:49.363104690 +1100 +@@ -20,16 +20,13 @@ + auto-mode-alist))))) + + ;; Default Twelf server program location +-(setq twelf-server-program +- (concat twelf-root "bin/twelf-server")) ++(setq twelf-server-program "/usr/bin/twelf-server") + + ;; Default Twelf SML program location +-(setq twelf-sml-program +- (concat twelf-root "bin/twelf-sml")) ++(setq twelf-sml-program "/usr/bin/twelf-sml") + + ;; Default documentation location (in info format) +-(setq twelf-info-file +- (concat twelf-root "doc/info/twelf.info")) ++(setq twelf-info-file "/usr/share/info/twelf.info") + + ;; Automatically highlight Twelf sources using font-lock + (add-hook 'twelf-mode-hook 'twelf-font-fontify-buffer) diff --git a/sci-mathematics/twelf/files/twelf-1.7.1-emacs-twelf.patch b/sci-mathematics/twelf/files/twelf-1.7.1-emacs-twelf.patch new file mode 100644 index 000000000000..c6c3a9b1fae1 --- /dev/null +++ b/sci-mathematics/twelf/files/twelf-1.7.1-emacs-twelf.patch @@ -0,0 +1,11 @@ +--- twelf-orig/emacs/twelf.el 2008-07-13 06:06:03.000000000 +1000 ++++ twelf/emacs/twelf.el 2012-12-10 00:39:05.332036491 +1100 +@@ -1815,7 +1815,7 @@ + (twelf-server-process (twelf-server-process twelf-server-buffer)) + (proc-mark (process-mark twelf-server-process)) + (_ (display-buffer twelf-server-buffer)) +- (twelf-server-window (get-buffer-window twelf-server-buffer))) ++ (twelf-server-window (get-buffer-window twelf-server-buffer t))) + (if (not (pos-visible-in-window-p proc-mark twelf-server-window)) + (progn + (push-mark proc-mark) diff --git a/sci-mathematics/twelf/files/twelf-1.7.1-mlton-mlb.patch b/sci-mathematics/twelf/files/twelf-1.7.1-mlton-mlb.patch new file mode 100644 index 000000000000..24d16049c0e5 --- /dev/null +++ b/sci-mathematics/twelf/files/twelf-1.7.1-mlton-mlb.patch @@ -0,0 +1,409 @@ +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 ++ + diff --git a/sci-mathematics/twelf/metadata.xml b/sci-mathematics/twelf/metadata.xml new file mode 100644 index 000000000000..667fd5f61ae1 --- /dev/null +++ b/sci-mathematics/twelf/metadata.xml @@ -0,0 +1,13 @@ +<?xml version="1.0" encoding="UTF-8"?> +<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd"> +<pkgmetadata> + <maintainer type="person"> + <email>gienah@gentoo.org</email> + <name>Mark Wright</name> + </maintainer> + <longdescription lang="en"> +Twelf is an implementation of the logical framework LF. It is used for +logic programming and for the formalization of programming language +theory. +</longdescription> +</pkgmetadata> diff --git a/sci-mathematics/twelf/twelf-1.7.1.ebuild b/sci-mathematics/twelf/twelf-1.7.1.ebuild new file mode 100644 index 000000000000..02712b874f0f --- /dev/null +++ b/sci-mathematics/twelf/twelf-1.7.1.ebuild @@ -0,0 +1,111 @@ +# Copyright 1999-2016 Gentoo Foundation +# Distributed under the terms of the GNU General Public License v2 + +EAPI="5" + +inherit elisp-common eutils multilib + +MY_PN="${PN}-src" +MY_P="${MY_PN}-${PV}" + +DESCRIPTION="Implementation of the logical framework LF" +HOMEPAGE="http://twelf.org/" +SRC_URI="http://twelf.plparty.org/releases/${MY_P}.tar.gz" + +SLOT="0/${PV}" +KEYWORDS="~amd64 ~x86" +LICENSE="BSD-2" +IUSE="doc emacs examples" + +# tests reference non-existing directory TEST +RESTRICT="test" + +RDEPEND=" + dev-lang/mlton + doc? ( + virtual/latex-base + app-text/texi2html + ) + emacs? ( + virtual/emacs + )" +DEPEND="${RDEPEND}" + +S=${WORKDIR}/${PN} + +SITEFILE=50${PN}-gentoo.el + +PATCHES=( + "${FILESDIR}/${PN}-1.7.1-doc-guide-twelf-dot-texi.patch" + "${FILESDIR}/${PN}-1.7.1-doc-guide-Makefile.patch" + "${FILESDIR}/${PN}-1.7.1-emacs-twelf.patch" + "${FILESDIR}/${PN}-1.7.1-emacs-twelf-init.patch" + "${FILESDIR}/${PN}-1.7.1-Makefile.patch" + "${FILESDIR}/${PN}-1.7.1-mlton-mlb.patch" +) + +src_prepare() { + epatch "${PATCHES[@]}" + sed \ + -e "s@/usr/bin@${ROOT}usr/bin@g" \ + -e "s@/usr/share@${ROOT}usr/share@" \ + -i "${S}"/emacs/twelf-init.el \ + || die "Could not set ROOT in ${S}/emacs/twelf-init.el" +} + +src_compile() { + emake mlton CFLAGS="${CFLAGS}" LDFLAGS="${LDFLAGS} -fno-PIE" + if use emacs ; then + pushd "${S}/emacs" || die "Could change directory to emacs" + elisp-compile \ + auc-menu.el \ + twelf-font.el \ + twelf-init.el \ + twelf.el \ + || die "emacs elisp compile failed" + popd + fi + if use doc; then + pushd doc/guide + emake all + popd + fi +} + +ins_example_dir() { + insinto "/usr/share/${PN}/examples/${1}" + pushd "${S}/${1}" + doins -r * + popd +} + +src_install() { + if use emacs ; then + elisp-install ${PN} emacs/*.{el,elc} + cp "${FILESDIR}"/${SITEFILE} "${S}" + elisp-site-file-install ${SITEFILE} + fi + if use examples; then + ins_example_dir examples + ins_example_dir examples-clp + ins_example_dir examples-delphin + fi + dobin bin/twelf-server + dohtml doc/html/index.html + doinfo doc/guide/twelf.info + dodoc doc/guide/twelf.dvi doc/guide/twelf.ps doc/guide/twelf.pdf + dohtml doc/guide/twelf/* +} + +pkg_postinst() { + if use emacs; then + elisp-site-regen + ewarn "For twelf emacs, add this line to ~/.emacs" + ewarn "" + ewarn '(load (concat twelf-root "/twelf-init.el"))' + fi +} + +pkg_postrm() { + use emacs && elisp-site-regen +} |