Adding metadata

15 files changed, 0 insertions, 782 deletions

diff --git a/sci-mathematics/twelf/Manifest b/sci-mathematics/twelf/Manifest
deleted file mode 100644
index 7859cca13c6f..000000000000
--- a/sci-mathematics/twelf/Manifest
+++ /dev/null
@@ -1 +0,0 @@
-DIST twelf-src-1.7.1.tar.gz 1147610 BLAKE2B 9fbb3c5a4823845a0c721112744330658be0e68784ef209a3d17fb72874ef50d7dbb434a7104704a5540f2f0bc30727bfe1ff602f986570f944454e77c24609d SHA512 1b4baa0f385b6b605583a9da312f23c775aab43e7398c6e151833a6b95c74112492530f44fcb7b14f8288774e9b63e2f9618a5debfbc4d34737bc2588f5850df
diff --git a/sci-mathematics/twelf/files/50twelf-gentoo.el b/sci-mathematics/twelf/files/50twelf-gentoo.el
deleted file mode 100644
index 784e2b36b0a7..000000000000
--- a/sci-mathematics/twelf/files/50twelf-gentoo.el
+++ /dev/null
@@ -1,2 +0,0 @@
-(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
deleted file mode 100644
index 84631f357d9d..000000000000
--- a/sci-mathematics/twelf/files/twelf-1.7.1-Makefile.patch
+++ /dev/null
@@ -1,43 +0,0 @@
---- 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
deleted file mode 100644
index 092b12b20dc0..000000000000
--- a/sci-mathematics/twelf/files/twelf-1.7.1-doc-guide-Makefile.patch
+++ /dev/null
@@ -1,13 +0,0 @@
---- 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
deleted file mode 100644
index 877ecd60b710..000000000000
--- a/sci-mathematics/twelf/files/twelf-1.7.1-doc-guide-twelf-dot-texi.patch
+++ /dev/null
@@ -1,14 +0,0 @@
---- 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-fix-old-style-backquotes-p1.patch b/sci-mathematics/twelf/files/twelf-1.7.1-emacs-fix-old-style-backquotes-p1.patch
deleted file mode 100644
index b8d78d97e04e..000000000000
--- a/sci-mathematics/twelf/files/twelf-1.7.1-emacs-fix-old-style-backquotes-p1.patch
+++ /dev/null
@@ -1,45 +0,0 @@
-commit 141018e777eecc064909c6f5429c8a0d0c048b5a
-Author: Kartik Singhal <ks@cs.uchicago.edu>
-Date:   Sat Feb 27 16:13:35 2021 -0600
-
-    Fix old-style backquotes, following https://github.com/ProofGeneral/PG/commit/ca601291ddf22739847c629f2d687ab3f68b4786
-
-diff --git a/emacs/twelf.el b/emacs/twelf.el
-index 1e4d46f..57b9cee 100644
---- a/emacs/twelf.el
-+++ b/emacs/twelf.el
-@@ -2884,7 +2884,7 @@ Mode map
-   (setq twelf-server-display-commands (not twelf-server-display-commands)))
- 
- (defconst twelf-options-menu
--  (` ("Options"
-+    `("Options"
-       (, (toggle "Display Commands" '(twelf-toggle-server-display-commands)
- 		 'twelf-server-display-commands))
-       ("chatter"
-@@ -2922,7 +2922,7 @@ Mode map
-       ("Table."
-        ["strategy" (twelf-set-parm "Table.strategy") t]
-        ["strengthen" (twelf-set-parm "Table.strengthen") t])
--      ["Reset Menubar" twelf-reset-menu t]))
-+      ["Reset Menubar" twelf-reset-menu t])
-   "Menu to change options in Twelf mode.")
- 
- (defconst twelf-timers-menu
-@@ -2939,12 +2939,12 @@ Mode map
-   "Fontify current buffer using font-lock minor mode.")
- 
- (defconst twelf-syntax-menu
--  (` ("Syntax Highlighting"
-+    `("Syntax Highlighting"
-       ["Highlight Declaration" twelf-font-fontify-decl t]
-       ["Highlight Buffer" twelf-font-fontify-buffer t]
--      ;(, (toggle "Immediate Highlighting" 'toggle-twelf-font-immediate
--      ;'font-lock-mode))
--      ))
-+      ;;(, (toggle "Immediate Highlighting" 'toggle-twelf-font-immediate
-+      ;;'font-lock-mode))
-+      )
-   "Menu for syntax highlighting in Twelf mode.")
- 
- (easy-menu-define twelf-menu (list twelf-mode-map)
diff --git a/sci-mathematics/twelf/files/twelf-1.7.1-emacs-fix-old-style-backquotes-p2.patch b/sci-mathematics/twelf/files/twelf-1.7.1-emacs-fix-old-style-backquotes-p2.patch
deleted file mode 100644
index aae0ef7b75e3..000000000000
--- a/sci-mathematics/twelf/files/twelf-1.7.1-emacs-fix-old-style-backquotes-p2.patch
+++ /dev/null
@@ -1,36 +0,0 @@
-commit c1bec0d0b9fa506e36bb364b1765191b159e6c4c
-Author: Kartik Singhal <ks@cs.uchicago.edu>
-Date:   Sat Feb 27 16:24:24 2021 -0600
-
-    Argh, two more places
-
-diff --git a/emacs/twelf.el b/emacs/twelf.el
-index 57b9cee..0a04a35 100644
---- a/emacs/twelf.el
-+++ b/emacs/twelf.el
-@@ -2833,13 +2833,13 @@ Mode map
-   "Menu for printing commands.")
- 
- (defconst twelf-recon-menu
--  (` ("Reconstruction"
-+    `("Reconstruction"
-       (, (toggle "trace" '(twelf-toggle-recon-trace)
- 		 '(string-equal twelf-recon-trace "true")))
--      ["traceMode" (twelf-set-parm "Recon.traceMode") t])))
-+      ["traceMode" (twelf-set-parm "Recon.traceMode") t]))
- 
- (defconst twelf-trace-menu
--  (` ("Trace"
-+    `("Trace"
-       ("trace"
-        ["All" twelf-trace-trace-all t]
-        ["None" twelf-trace-untrace t]
-@@ -2852,7 +2852,7 @@ Mode map
-       ("detail"
-        (, (radio "0" '(twelf-set "Trace.detail" "0") '(equal twelf-trace-detail "0")))
-        (, (radio "1*" '(twelf-set "Trace.detail" "1") '(equal twelf-trace-detail "1")))
--       (, (radio "2" '(twelf-set "Trace.detail" "2") '(equal twelf-trace-detail "2")))))))
-+       (, (radio "2" '(twelf-set "Trace.detail" "2") '(equal twelf-trace-detail "2"))))))
- 
- (defconst twelf-server-state-menu
-   '("Server State"
diff --git a/sci-mathematics/twelf/files/twelf-1.7.1-emacs-fix-old-style-backquotes-p3.patch b/sci-mathematics/twelf/files/twelf-1.7.1-emacs-fix-old-style-backquotes-p3.patch
deleted file mode 100644
index e15d838942e7..000000000000
--- a/sci-mathematics/twelf/files/twelf-1.7.1-emacs-fix-old-style-backquotes-p3.patch
+++ /dev/null
@@ -1,28 +0,0 @@
-diff --git a/emacs/auc-menu.el b/emacs/auc-menu.el
-index f6483b0..80fe660 100644
---- a/emacs/auc-menu.el
-+++ b/emacs/auc-menu.el
-@@ -92,10 +92,10 @@
- (defmacro easy-menu-define (symbol maps doc menu)
-   "Define SYMBOL to be a menu for keymaps MAPS.
- DOC is the documentation string, and MENU is a Lucid style menu."
--  (` (progn
-+    `(progn
-        (require 'auc-menu)		;For `easy-menu-do-define'.
-        (defvar (, symbol) nil (, doc))
--       (easy-menu-do-define (quote (, symbol)) (, maps) (, doc) (, menu)))))
-+       (easy-menu-do-define (quote (, symbol)) (, maps) (, doc) (, menu))))
- 
- (cond 
- 
-@@ -212,8 +212,8 @@ DOC is the documentation string, and MENU is a Lucid style menu."
- 
- (defun easy-menu-do-define (symbol maps doc menu)
-   (set symbol (easy-menu-create-keymaps (car menu) (cdr menu)))
--  (fset symbol (` (lambda (event) (, doc) (interactive "@e")
--		    (easy-popup-menu event (, symbol)))))
-+  (fset symbol `(lambda (event) (, doc) (interactive "@e")
-+		    (easy-popup-menu event (, symbol))))
-   (mapcar (function (lambda (map) 
- 	    (define-key map (vector 'menu-bar (intern (car menu)))
- 	      (cons (car menu) (symbol-value symbol)))))
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
deleted file mode 100644
index 983c3c2290ed..000000000000
--- a/sci-mathematics/twelf/files/twelf-1.7.1-emacs-twelf-init.patch
+++ /dev/null
@@ -1,22 +0,0 @@
---- 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
deleted file mode 100644
index c6c3a9b1fae1..000000000000
--- a/sci-mathematics/twelf/files/twelf-1.7.1-emacs-twelf.patch
+++ /dev/null
@@ -1,11 +0,0 @@
---- 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-20180207.patch b/sci-mathematics/twelf/files/twelf-1.7.1-mlton-20180207.patch
deleted file mode 100644
index 823d3e37a8d8..000000000000
--- a/sci-mathematics/twelf/files/twelf-1.7.1-mlton-20180207.patch
+++ /dev/null
@@ -1,11 +0,0 @@
---- twelf-orig/Makefile	2018-03-06 23:30:35.055598250 +1100
-+++ twelf/Makefile	2018-03-06 23:24:44.403762472 +1100
-@@ -11,7 +11,7 @@
- polyml = poly
- smlnj = sml
- oldnj = sml
--mlton = mlton -default-ann 'nonexhaustiveMatch ignore'
-+mlton = mlton -disable-ann nonexhaustiveMatch
- make = make
- 
- twelfdir = `pwd`
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
deleted file mode 100644
index 24d16049c0e5..000000000000
--- a/sci-mathematics/twelf/files/twelf-1.7.1-mlton-mlb.patch
+++ /dev/null
@@ -1,409 +0,0 @@
-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/files/twelf-1.7.1-remove-svnversion.patch b/sci-mathematics/twelf/files/twelf-1.7.1-remove-svnversion.patch
deleted file mode 100644
index 64d29f3cba31..000000000000
--- a/sci-mathematics/twelf/files/twelf-1.7.1-remove-svnversion.patch
+++ /dev/null
@@ -1,13 +0,0 @@
-diff --git a/bin/buildid b/bin/buildid
-index bb60cd3..5972ac0 100755
---- a/bin/buildid
-+++ b/bin/buildid
-@@ -5,7 +5,7 @@
- # William Lovas, 08-27-2010
- #
- 
--REV=`svnversion`
-+REV="1813"
- DATE=`date "+%m/%d/%y at %H:%M:%S"`
- HOST=`hostname`
- 
diff --git a/sci-mathematics/twelf/metadata.xml b/sci-mathematics/twelf/metadata.xml
deleted file mode 100644
index 26c76acfaad5..000000000000
--- a/sci-mathematics/twelf/metadata.xml
+++ /dev/null
@@ -1,10 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE pkgmetadata SYSTEM "https://docs.baldeagleos.com/dtd/metadata.dtd">
-<pkgmetadata>
-  <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>
-  <origin>baldeagleos-repo</origin>
-</pkgmetadata>
diff --git a/sci-mathematics/twelf/twelf-1.7.1-r2.ebuild b/sci-mathematics/twelf/twelf-1.7.1-r2.ebuild
deleted file mode 100644
index 1fc16b00baa4..000000000000
--- a/sci-mathematics/twelf/twelf-1.7.1-r2.ebuild
+++ /dev/null
@@ -1,124 +0,0 @@
-# Copyright 1999-2024 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI="8"
-
-inherit elisp-common flag-o-matic
-
-MY_PN="${PN}-src"
-MY_P="${MY_PN}-${PV}"
-
-DESCRIPTION="Implementation of the logical framework LF"
-HOMEPAGE="https://twelf.org/"
-SRC_URI="https://github.com/standardml/twelf/releases/download/v${PV}/${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-20180207
-	doc? (
-		virtual/latex-base
-		app-text/texi2html
-	)
-	emacs? (
-		>=app-editors/emacs-23.1:*
-	)"
-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
-	"${FILESDIR}"/${PN}-1.7.1-mlton-20180207.patch
-	"${FILESDIR}"/${PN}-1.7.1-remove-svnversion.patch                 # 728028
-	"${FILESDIR}"/${PN}-1.7.1-emacs-fix-old-style-backquotes-p1.patch # 803296
-	"${FILESDIR}"/${PN}-1.7.1-emacs-fix-old-style-backquotes-p2.patch
-	"${FILESDIR}"/${PN}-1.7.1-emacs-fix-old-style-backquotes-p3.patch
-)
-
-src_prepare() {
-	default
-	sed \
-		-e "s@/usr/bin@${PREFIX}/usr/bin@g" \
-		-e "s@/usr/share@${PREFIIX}/usr/share@" \
-		-i "${S}"/emacs/twelf-init.el \
-		|| die "Could not set PREFIX in ${S}/emacs/twelf-init.el"
-}
-
-src_compile() {
-	# relocation R_X86_64_32 against hidden symbol `globalCPointer' can not be used when making a PIE object
-	# https://bugs.gentoo.org/863266
-	#
-	# The software is unmaintained and disables bug reports.
-	filter-lto
-
-	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 -j1
-		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
-	if use doc; then
-		local DOCS=( doc/guide/twelf.dvi doc/guide/twelf.ps doc/guide/twelf.pdf )
-		local HTML_DOCS=( doc/html/index.html doc/guide/twelf/. )
-		doinfo doc/guide/twelf.info
-		einstalldocs
-	fi
-}
-
-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
-}