Adding metadata

15 files changed, 782 insertions, 0 deletions

diff --git a/sci-mathematics/twelf/Manifest b/sci-mathematics/twelf/Manifest
new file mode 100644
index 000000000000..7859cca13c6f
--- /dev/null
+++ b/sci-mathematics/twelf/Manifest
@@ -0,0 +1 @@
+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
new file mode 100644
index 000000000000..784e2b36b0a7
--- /dev/null
+++ b/sci-mathematics/twelf/files/50twelf-gentoo.el
@@ -0,0 +1,2 @@
+(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-fix-old-style-backquotes-p1.patch b/sci-mathematics/twelf/files/twelf-1.7.1-emacs-fix-old-style-backquotes-p1.patch
new file mode 100644
index 000000000000..b8d78d97e04e
--- /dev/null
+++ b/sci-mathematics/twelf/files/twelf-1.7.1-emacs-fix-old-style-backquotes-p1.patch
@@ -0,0 +1,45 @@
+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
new file mode 100644
index 000000000000..aae0ef7b75e3
--- /dev/null
+++ b/sci-mathematics/twelf/files/twelf-1.7.1-emacs-fix-old-style-backquotes-p2.patch
@@ -0,0 +1,36 @@
+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
new file mode 100644
index 000000000000..e15d838942e7
--- /dev/null
+++ b/sci-mathematics/twelf/files/twelf-1.7.1-emacs-fix-old-style-backquotes-p3.patch
@@ -0,0 +1,28 @@
+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
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-20180207.patch b/sci-mathematics/twelf/files/twelf-1.7.1-mlton-20180207.patch
new file mode 100644
index 000000000000..823d3e37a8d8
--- /dev/null
+++ b/sci-mathematics/twelf/files/twelf-1.7.1-mlton-20180207.patch
@@ -0,0 +1,11 @@
+--- 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
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/files/twelf-1.7.1-remove-svnversion.patch b/sci-mathematics/twelf/files/twelf-1.7.1-remove-svnversion.patch
new file mode 100644
index 000000000000..64d29f3cba31
--- /dev/null
+++ b/sci-mathematics/twelf/files/twelf-1.7.1-remove-svnversion.patch
@@ -0,0 +1,13 @@
+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
new file mode 100644
index 000000000000..26c76acfaad5
--- /dev/null
+++ b/sci-mathematics/twelf/metadata.xml
@@ -0,0 +1,10 @@
+<?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
new file mode 100644
index 000000000000..1fc16b00baa4
--- /dev/null
+++ b/sci-mathematics/twelf/twelf-1.7.1-r2.ebuild
@@ -0,0 +1,124 @@
+# 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
+}