Add isabelle 2004, a generic proof assistant.

PR:		84859
Submitted by:	Timothy Bourke <timbob@bigpond.com>

4 files changed, 181 insertions, 0 deletions

diff --git a/math/isabelle/files/Makefile b/math/isabelle/files/Makefile
new file mode 100644
index 000000000000..10d428934511
--- /dev/null
+++ b/math/isabelle/files/Makefile
@@ -0,0 +1,31 @@
+# 20050609 T.Bourke
+# $FreeBSD$
+# Install Isabelle from within FreeBSD ports.
+
+DESTDIR=${PREFIX}/share/isabelle
+SRCDIRS=bin contrib etc lib src heaps
+
+all:
+	./build -a -b
+
+install:
+	mkdir -p ${DESTDIR}
+	${BSD_INSTALL_DATA} COPYRIGHT ${DESTDIR}/
+	${BSD_INSTALL_DATA} NEWS ${DESTDIR}/
+	${BSD_INSTALL_DATA} README ${DESTDIR}/
+	${BSD_INSTALL_DATA} ANNOUNCE ${DESTDIR}/
+	${BSD_INSTALL_SCRIPT} build ${DESTDIR}/
+	${BSD_INSTALL_SCRIPT} configure ${DESTDIR}/
+	-rm lib/Tools/doc.orig
+	for f in ${SRCDIRS}; \
+		do for g in `find -d $$f -type d`;	\
+		   do mkdir -p ${DESTDIR}/$$g;		\
+		      files=`find $$g -depth 1 -type f \\! -perm +u+x`;	\
+		      if [ "$$files" != "" ]; then ${BSD_INSTALL_DATA}	\
+			$$files ${DESTDIR}/$$g; fi; \
+		      scripts=`find $$g -depth 1 -type f -perm +u+x`;	\
+		     if [ "$$scripts" != "" ]; then ${BSD_INSTALL_SCRIPT}	\
+			$$scripts ${DESTDIR}/$$g; fi; \
+		   done;	\
+		done
+
diff --git a/math/isabelle/files/badmaxdsiz b/math/isabelle/files/badmaxdsiz
new file mode 100644
index 000000000000..578ab37d768f
--- /dev/null
+++ b/math/isabelle/files/badmaxdsiz
@@ -0,0 +1,18 @@
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+! The system process data segment value is too low!                  !
+!                                                                    !
+! Under these circumstances the Isabelle build process for logics    !
+! such as HOL will not terminate, or otherwise fail.                 !
+!                                                                    !
+! The setting may be viewed and modified with the commands:          !
+!   sh:  ulimit -Hd                                                  !
+!   csh: limit -h datasize                                           !
+!                                                                    !
+! It may be necessary to lift the maximum limit. One way of doing    !
+! this is to add a line to /boot/loader.conf and then to restart the !
+! system:                                                            !
+!    kern.maxdsiz="896M"                                             !
+!                                                                    !
+! This problem only affects Poly/ML. Isabelle may also be configured !
+! to use SML/NJ (build with WITH_SMLNJ=yes).                         !
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
diff --git a/math/isabelle/files/patch-etc-settings b/math/isabelle/files/patch-etc-settings
new file mode 100644
index 000000000000..5a16d33a34ff
--- /dev/null
+++ b/math/isabelle/files/patch-etc-settings
@@ -0,0 +1,122 @@
+--- etc/settings.orig	Tue Jun  8 10:29:49 2004
++++ etc/settings	Fri Aug 12 17:22:30 2005
+@@ -13,61 +13,12 @@
+ # binaries.  Do not invent new ML system names unless you know what
+ # you are doing.  Only one of the sections below should be activated.
+ 
+-
+-# try finding the poly packages from the Isabelle site in the usual places
+-POLYML_HOME=$(choosefrom \
+-  "$ISABELLE_HOME/contrib/polyml" \
+-  "$ISABELLE_HOME/../polyml" \
+-  "/usr/share/polyml" \
+-  "/usr/local/polyml" \
+-  "/opt/polyml")
+-
+-if [ -n "$POLYML_HOME" -a -e "$POLYML_HOME/bin/polyml-version" ]; then
+-  # looks like Isabelle poly packages
+-  ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
+-  ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
+-  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+-  ML_OPTIONS="-h 15000"
+-elif [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
+-  # maybe a shrink-wrapped polyml on x86-linux ...
+-
+-  # Poly/ML 4.0, 4.1, 4.1.x
+-  # include version number, needed for choosing right options
+-  ML_SYSTEM=polyml-4.1.3    
+-  # processor/OS type
+-  ML_PLATFORM=x86-linux
+-  # where to find binaries
+-  ML_HOME=/usr/bin
+-  # where to find the standard database
+-  ML_DBASE=/usr/lib/poly/ML_dbase
+-  # options to pass to poly
+-  ML_OPTIONS="-h 15000"
+-fi
+-
+-# Standard ML of New Jersey 110 or later
+-#ML_SYSTEM=smlnj-110
+-#ML_HOME="$ISABELLE_HOME/../smlnj/bin"
+-#ML_OPTIONS="@SMLdebug=/dev/null"
+-#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
+-
+-# MLWorks 2.0
+-#ML_SYSTEM=mlworks
+-#ML_HOME="$ISABELLE_HOME/../mlworks/bin"
+-#ML_OPTIONS=""
+-#ML_PLATFORM=""
+-
+-# Moscow ML 2.00 or later (experimental!)
+-#ML_SYSTEM=mosml
+-#ML_HOME="$ISABELLE_HOME/../mosml/bin"
+-#ML_PLATFORM=""
+-#ML_OPTIONS=""
+-
+-# Standard ML of New Jersey 0.93
+-#ML_SYSTEM=smlnj-0.93
+-#ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
+-#ML_OPTIONS=""
+-#ML_PLATFORM=""
+-
++# %%ML_COMMENT%%
++ML_SYSTEM=%%ML_SYSTEM%%
++ML_HOME=%%ML_HOME%%
++ML_OPTIONS=%%ML_OPTIONS%%
++ML_PLATFORM=x86-bsd
++ML_DBASE=%%ML_DBASE%%
+ 
+ ###
+ ### Compilation options for isatool usedir
+@@ -79,7 +30,6 @@
+ # for overriding proof objects in HOL image
+ HOL_PROOF_OBJECTS=""
+ 
+-
+ ###
+ ### Document preparation
+ ###
+@@ -155,7 +105,7 @@
+ ###
+ 
+ #Where to look for docs (multiple dirs separated by ':').
+-ISABELLE_DOCS="$ISABELLE_HOME/doc"
++ISABELLE_DOCS="%%PREFIX%%/share/doc/isabelle"
+ 
+ #The dvi file viewer
+ DVI_VIEWER=xdvi
+@@ -181,12 +131,7 @@
+ 
+ # Proof General path, look in a variety of places
+ ISABELLE_INTERFACE=$(choosefrom \
+-  "$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \
+-  "$ISABELLE_HOME/../ProofGeneral/isar/interface" \
+-  "/usr/share/ProofGeneral/isar/interface" \
+-  "/usr/local/ProofGeneral/isar/interface" \
+-  "/opt/ProofGeneral/isar/interface" \
+-  "/usr/share/emacs/ProofGeneral/isar/interface" \
++  "%%PREFIX%%/bin/proofgeneral" \
+   "$ISABELLE_INTERFACE")
+ 
+ # Options to pass to Isabelle command when PG is selected as interface
+@@ -196,20 +141,9 @@
+ # try xemacs first, else emacs
+ type -path xemacs >/dev/null || PROOFGENERAL_OPTIONS="-p emacs $PROOFGENERAL_OPTIONS"
+ 
+-
+-# X-Symbol installation location (for Proof General, obsolete for PG >= 3.5)
+-XSYMBOL_HOME=$(choosefrom \
+-  "$ISABELLE_HOME/contrib/x-symbol" \
+-  "$ISABELLE_HOME/../x-symbol" \
+-  "/usr/share/x-symbol" \
+-  "/usr/local/x-symbol" \
+-  "/opt/x-symbol" \
+-  "")
+-
+ # Executed before xemacs with ProofGeneral is called.
+ # Required for remote fonts only.
+ #XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
+-
+ 
+ ###
+ ### External reasoning tools
diff --git a/math/isabelle/files/patch-lib-Tools-doc b/math/isabelle/files/patch-lib-Tools-doc
new file mode 100644
index 000000000000..490f01b47d05
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-doc
@@ -0,0 +1,10 @@
+--- lib/Tools/doc.orig	Tue Jun  8 10:29:49 2004
++++ lib/Tools/doc	Sat Aug 13 10:47:40 2005
+@@ -32,6 +32,7 @@
+ 
+ [ "$#" -ne 0 -o "$DOC" = "-?" ] && usage
+ 
++DOC=`expr "$DOC" : '^[ 	]*\(.*\)'`
+ 
+ ## main
+