Remove expired port:

2015-02-28 math/isabelle: Broken for more than 6 months
svn path=/head/; revision=380228
2015-03-01 21:24:40 +00:00 · 2015-03-01 21:24:40 +00:00 · f47967987e · 2021-03-31 03:12:20 +00:00
commit f47967987e
parent 92a699e645
8 changed files with 1 additions and 5866 deletions
--- a/1
+++ b/1
@ -7436,3 +7436,4 @@ net/xrdesktop||2015-03-01|Has expired: Unmaintained upstream - please use net/xr
 www/mediawiki122||2015-03-01|Has expired: Deprecated by upstream, use www/mediawiki12{3,4} instead
 www/mod_cplusplus||2015-03-01|Has expired: written for apache 2.0, no longer maintained upstream
 www/py-django15||2015-03-01|Has expired: not supported by upstream
+math/isabelle||2015-03-01|Has expired: Broken for more than 6 months
--- a/math/Makefile
+++ b/math/Makefile
@ -185,7 +185,6 @@
    SUBDIR += hs-vector-space
    SUBDIR += igraph
    SUBDIR += ipopt
-    SUBDIR += isabelle
    SUBDIR += ised
    SUBDIR += jacal
    SUBDIR += jags
--- a/math/isabelle/Makefile
+++ b/math/isabelle/Makefile
@ -1,177 +0,0 @@
-# Created by: Timothy Bourke <timbob@bigpond.com>
-# $FreeBSD$
-
-PORTNAME=	isabelle
-PORTVERSION=	2009.2
-CATEGORIES=	math
-MASTER_SITES=	http://isabelle.in.tum.de/dist/ \
-		http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ \
-		http://mirror.cse.unsw.edu.au/pub/isabelle/dist/
-DISTNAME=	Isabelle2009-2
-
-MAINTAINER=	ports@FreeBSD.org
-COMMENT=	Generic proof assistant
-
-LICENSE=	BSD3CLAUSE
-LICENSE_FILE=	${WRKSRC}/COPYRIGHT
-
-BROKEN=		Build seems to hang on the package builders
-DEPRECATED=	Broken for more than 6 months
-EXPIRATION_DATE=	2015-02-28
-
-OPTIONS_DEFINE=	POLYML RLWRAP LEDIT HOL_ALGEBRA HOL_NOMINAL HOL_NSA HOL_WORD \
-		HOL_TLA HOL_HOL4 EMACS_PKG
-OPTIONS_DEFAULT=	RLWRAP
-POLYML_DESC=		Use Poly/ML (fast but broken) instead of SML/NJ
-RLWRAP_DESC=		Use rlwrap as line editor
-LEDIT_DESC=		Use ledit as line editor
-HOL_ALGEBRA_DESC=	Build optional heap: HOL-Algebra
-HOL_NOMINAL_DESC=	Build optional heap: HOL-Nominal
-HOL_NSA_DESC=		Build optional heap: HOL-NSA
-HOL_WORD_DESC=		Build optional heap: HOL-Word
-HOL_TLA_DESC=		Build optional heap: TLA
-HOL_HOL4_DESC=		Build optional heap: HOL4
-EMACS_PKG_DESC=		Build with Emacs Packages
-
-USES=		perl5
-MAKE_JOBS_UNSAFE=	yes
-
-.include <bsd.port.options.mk>
-
-.if ${PORT_OPTIONS:MDOCS}
-DISTFILES=	${DISTNAME}.tar.gz \
-		${DISTNAME}_library.tar.gz
-.endif
-
-.if ${PORT_OPTIONS:MEMACS_PKG}
-USE_EMACS=	yes # for EMACS_SITE_LISPDIR
-EMACS_NO_BUILD_DEPENDS=yes
-EMACS_NO_RUN_DEPENDS=yes
-RUN_DEPENDS+=	proofgeneral:${PORTSDIR}/math/proofgeneral
-.else
-.endif
-
-BUILD_DEPENDS+=	bash:${PORTSDIR}/shells/bash
-RUN_DEPENDS+=	bash:${PORTSDIR}/shells/bash
-
-DOCFILES=	Contents *.pdf *.eps *.ps *.dvi
-
-.include <bsd.port.pre.mk>
-
-.if ${PORT_OPTIONS:MRLWRAP}
-RUN_DEPENDS+=	rlwrap:${PORTSDIR}/devel/rlwrap
-LINE_EDIT=	"${PREFIX}/bin/rlwrap"
-.else
-.if ${PORT_OPTIONS:MLEDIT}
-RUN_DEPENDS+=	ledit:${PORTSDIR}/sysutils/ledit
-LINE_EDIT=	"${PREFIX}/bin/ledit"
-.else
-LINE_EDIT=	""
-.endif
-.endif
-
-.if ${PORT_OPTIONS:MHOL_ALGEBRA}
-HEAP_HOL_ALGEBRA=""
-EXTRA_HOL+=-m HOL-Algebra
-.else
-HEAP_HOL_ALGEBRA="@comment "
-.endif
-.if ${PORT_OPTIONS:MHOL_NOMINAL}
-HEAP_HOL_NOMINAL=""
-EXTRA_HOL+=-m HOL-Nominal
-.else
-HEAP_HOL_NOMINAL="@comment "
-.endif
-.if ${PORT_OPTIONS:MHOL_NSA}
-HEAP_HOL_NSA=""
-EXTRA_HOL+=-m HOL-NSA
-.else
-HEAP_HOL_NSA="@comment "
-.endif
-.if ${PORT_OPTIONS:MHOL_WORD}
-HEAP_HOL_WORD=""
-EXTRA_HOL+=-m HOL-Word
-.else
-HEAP_HOL_WORD="@comment "
-.endif
-.if ${PORT_OPTIONS:MHOL_TLA}
-HEAP_HOL_TLA=""
-EXTRA_HOL+=-m TLA
-.else
-HEAP_HOL_TLA="@comment "
-.endif
-.if ${PORT_OPTIONS:MHOL_HOL4}
-HEAP_HOL_HOL4=""
-EXTRA_HOL+=-m HOL4
-.else
-HEAP_HOL_HOL4="@comment "
-.endif
-
-.if ! ${PORT_OPTIONS:MPOLYML}
-ML_SYSTEM=	smlnj-110
-ML_HOME=	${LOCALBASE}/smlnj/bin
-ML_OPTIONS=	-Ccontrol.poly-eq-warn=false @SMLdebug=/dev/null
-.else
-ML_SYSTEM=	polyml-5.3
-ML_HOME=	${LOCALBASE}/bin
-ML_OPTIONS=	-H 500
-ML_DBASE=	""
-.endif
-ML_PLATFORM=	x86-bsd
-
-PLIST_SUB+=	HEAPSUBDIR=${ML_SYSTEM}_${ML_PLATFORM} \
-		HEAP_HOL_ALGEBRA=${HEAP_HOL_ALGEBRA} \
-		HEAP_HOL_NOMINAL=${HEAP_HOL_NOMINAL} \
-		HEAP_HOL_NSA=${HEAP_HOL_NSA} \
-		HEAP_HOL_WORD=${HEAP_HOL_WORD} \
-		HEAP_HOL_TLA=${HEAP_HOL_TLA} \
-		HEAP_HOL_HOL4=${HEAP_HOL_HOL4}
-.if ! ${PORT_OPTIONS:MPOLYML}
-BUILD_DEPENDS+=	smlnj>=110.71:${PORTSDIR}/lang/smlnj
-MAKE_ENV+=	SMLNJ_DEVEL=yes
-.else
-BUILD_DEPENDS+=	polyml>=5.2.1:${PORTSDIR}/lang/polyml
-RUN_DEPENDS+=	polyml>=5.2.1:${PORTSDIR}/lang/polyml
-.endif
-
-post-extract:
-	@${CP} ${FILESDIR}/Makefile ${WRKSRC}
-
-post-patch:
-	@${MV} ${WRKSRC}/etc/settings ${WRKSRC}/etc/settings.presed
-	@${SED} "s|%%ML_SYSTEM%%|${ML_SYSTEM}|;		\
-		 s|%%ML_HOME%%|${ML_HOME}|;		\
-		 s|%%ML_OPTIONS%%|\"${ML_OPTIONS}\"|;	\
-		 s|%%ML_DBASE%%|${ML_DBASE}|;		\
-		 s|%%ML_PLATFORM%%|${ML_PLATFORM}|;	\
-		 s|%%PREFIX%%|${PREFIX}|;		\
-		 s|%%LINE_EDIT%%|${LINE_EDIT}|;		\
-		 s|%%SYSTMPDIR%%|/tmp|;			\
-		 s|%%JAVASHAREDIR%%|${PREFIX}/share/java|;	\
-		 s|%%EMACS_SITE_LISPDIR%%|${EMACS_SITE_LISPDIR}|" \
-		${WRKSRC}/etc/settings.presed > ${WRKSRC}/etc/settings
-	@${RM} ${WRKSRC}/etc/settings.presed
-	@${TOUCH} ${WRKSRC}/contrib/.keep
-	@${REINPLACE_CMD} -e 's|%%SMLNJ_VERSION%%|SMLNJ_DEVEL=yes|' \
-			${WRKSRC}/lib/scripts/run-smlnj
-
-post-build:
-.if defined(EXTRA_HOL)
-	${WRKSRC}/build -b ${EXTRA_HOL} HOL
-.endif
-
-post-install:
-	${WRKSRC}/bin/isabelle install \
-		-d ${STAGEDIR}${PREFIX}/share/isabelle \
-		-p ${STAGEDIR}${PREFIX}/bin
-.if ${PORT_OPTIONS:MDOCS}
-	${MKDIR} ${STAGEDIR}${DOCSDIR}
-.for file in ${DOCFILES}
-	${INSTALL_DATA} ${WRKSRC}/doc/${file} ${STAGEDIR}${DOCSDIR}
-.endfor
-	(cd ${WRKSRC}; \
-	 ${FIND} -d browser_info -type d -exec ${MKDIR} ${STAGEDIR}${DOCSDIR}/{} \; ; \
-	 ${FIND} -d browser_info -type f -exec ${INSTALL_DATA} {} ${STAGEDIR}${DOCSDIR}/{} \;)
-.endif
-
-.include <bsd.port.post.mk>
--- a/math/isabelle/distinfo
+++ b/math/isabelle/distinfo
@ -1,4 +0,0 @@
-SHA256 (Isabelle2009-2.tar.gz) = f92a275b78bd8844de47a5902e339b58f3b768c07a7fb19d8e606b68499d5ac4
-SIZE (Isabelle2009-2.tar.gz) = 25193255
-SHA256 (Isabelle2009-2_library.tar.gz) = 1cf4cc438185146367938308e01be2f29b793d6c343299aa697def9a098e63aa
-SIZE (Isabelle2009-2_library.tar.gz) = 54438382
--- a/math/isabelle/files/Makefile
+++ b/math/isabelle/files/Makefile
@ -1,30 +0,0 @@
-# 20050609 T.Bourke
-# $FreeBSD$
-# Install Isabelle from within FreeBSD ports.
-
-DESTDIR=${PREFIX}/share/isabelle
-SRCDIRS=bin contrib etc heaps lib src
-
-all:
-	./build -a -b
-
-install:
-	mkdir -p ${DESTDIR}
-	${BSD_INSTALL_DATA} ANNOUNCE ${DESTDIR}/
-	${BSD_INSTALL_DATA} CONTRIBUTORS ${DESTDIR}/
-	${BSD_INSTALL_DATA} COPYRIGHT ${DESTDIR}/
-	${BSD_INSTALL_DATA} NEWS ${DESTDIR}/
-	${BSD_INSTALL_DATA} README ${DESTDIR}/
-	${BSD_INSTALL_SCRIPT} build ${DESTDIR}/
-	for f in ${SRCDIRS}; \
-		do for g in `find -d $$f -type d`; \
-		   do mkdir -p ${DESTDIR}/$$g; \
-  files=`find -E $$g -depth 1 -type f -not -regex '.*\.(bak|orig)$$' -not -perm +u+x`; \
-			    if [ "$$files" != "" ]; then ${BSD_INSTALL_DATA} \
-			$$files ${DESTDIR}/$$g; fi; \
-  scripts=`find -E $$g -depth 1 -type f -not -regex '.*\.(bak|orig)$$' -perm +u+x`; \
-		     if [ "$$scripts" != "" ]; then ${BSD_INSTALL_SCRIPT} \
-			$$scripts ${DESTDIR}/$$g; fi; \
-		   done; \
-		done
-
--- a/math/isabelle/files/patch-etc-settings
+++ b/math/isabelle/files/patch-etc-settings
@ -1,119 +0,0 @@
--- etc/settings.orig	2010-06-21 02:24:19.000000000 -0700
-+++ etc/settings	2010-08-16 14:53:16.000000000 -0700
-@@ -15,19 +15,7 @@
- # not invent new ML system names unless you know what you are doing.
- # Only one of the sections below should be activated.
- 
-# Poly/ML 5.x (automated settings)
-POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")"
-ML_PLATFORM="$ISABELLE_PLATFORM"
-ML_HOME=$(choosefrom \
-  "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
-  "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
-  "/usr/local/polyml/$ML_PLATFORM" \
-  "/usr/share/polyml/$ML_PLATFORM" \
-  "/opt/polyml/$ML_PLATFORM" \
-  $POLY_HOME)
-ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
-ML_OPTIONS="-H 200"
-ML_SOURCES="$ML_HOME/../src"
-+
- 
- # Poly/ML 5.3.0
- #ML_PLATFORM=x86-linux
-@@ -50,6 +38,13 @@
- #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
- #SMLNJ_CYGWIN_RUNTIME=1
- 
-+# FreeBSD PolyML Settings
-+ML_SYSTEM=%%ML_SYSTEM%%
-+ML_HOME=%%ML_HOME%%
-+ML_OPTIONS=%%ML_OPTIONS%%
-+ML_PLATFORM=%%ML_PLATFORM%%
-+ML_DBASE=%%ML_DBASE%%
-+
- 
- ###
- ### JVM components (Scala or Java)
-@@ -64,7 +59,7 @@
- ### Interactive sessions (cf. isabelle tty)
- ###
- 
-ISABELLE_LINE_EDITOR=""
-+ISABELLE_LINE_EDITOR="%%LINE_EDIT%%"
- [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
- [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)"
- 
-@@ -109,7 +104,7 @@
- ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
- 
- # Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-+ISABELLE_TMP_PREFIX="%%SYSTMPDIR%%/isabelle-$USER"
- 
- # Heap input locations. ML system identifier is included in lookup.
- ISABELLE_PATH="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER:$ISABELLE_HOME/heaps"
-@@ -136,7 +131,7 @@
- ###
- 
- # Where to look for docs (multiple dirs separated by ':').
-ISABELLE_DOCS="$ISABELLE_HOME/doc"
-+ISABELLE_DOCS="%%PREFIX%%/share/doc/isabelle"
- 
- # Preferred document format
- ISABELLE_DOC_FORMAT=pdf
-@@ -173,9 +168,7 @@
- PROOFGENERAL_HOME=$(choosefrom \
-   "$ISABELLE_HOME/contrib/ProofGeneral" \
-   "$ISABELLE_HOME/../ProofGeneral" \
-  "/usr/local/ProofGeneral" \
-  "/usr/share/ProofGeneral" \
-  "/opt/ProofGeneral" \
-+  "%%PREFIX%%/%%EMACS_SITE_LISPDIR%%/ProofGeneral" \
-   "")
- 
- PROOFGENERAL_OPTIONS=""
-@@ -201,9 +194,9 @@
- ## Set HOME only for tools you have installed!
- 
- # External provers
-#E_HOME=/usr/local/bin
-#SPASS_HOME=/usr/local/bin
-#VAMPIRE_HOME=/usr/local/bin
-+#E_HOME=%%PREFIX%%/bin
-+#SPASS_HOME=%%PREFIX%%/bin
-+#VAMPIRE_HOME=%%PREFIX%%/bin
- 
- # HOL4 proof objects (cf. Isabelle/src/HOL/Import)
- #HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
-@@ -214,24 +207,24 @@
- #SVC_MACHINE=sparc-sun-solaris
- 
- # Mucke (mu-calculus model checker)
-#MUCKE_HOME=/usr/local/bin
-+#MUCKE_HOME=%%PREFIX%%/bin
- 
- # Einhoven model checker
-#EINDHOVEN_HOME=/usr/local/bin
-+#EINDHOVEN_HOME=%%PREFIX%%/bin
- 
- # MiniSat 1.14 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
-#MINISAT_HOME=/usr/local/bin
-+#MINISAT_HOME=%%PREFIX%%/bin
- 
- # zChaff (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
-#ZCHAFF_HOME=/usr/local/bin
-+#ZCHAFF_HOME=%%PREFIX%%/bin
- 
- # BerkMin561 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
-#BERKMIN_HOME=/usr/local/bin
-+#BERKMIN_HOME=%%PREFIX%%/bin
- #BERKMIN_EXE=BerkMin561-linux
- #BERKMIN_EXE=BerkMin561-solaris
- 
- # Jerusat 1.3 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
-#JERUSAT_HOME=/usr/local/bin
-+#JERUSAT_HOME=%%PREFIX%%/bin
- 
- # CSDP (SDP Solver, cf. Isabelle/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML)
- #CSDP_EXE=csdp
--- a/math/isabelle/pkg-descr
+++ b/math/isabelle/pkg-descr
@ -1,20 +0,0 @@
-Isabelle is a generic proof assistant. It allows mathematical
-formulas to be expressed in a formal language and provides tools
-for proving those formulas in a logical calculus. The main application
-is the formalization of mathematical proofs and in particular formal
-verification, which includes proving the correctness of computer
-hardware or software and proving properties of computer languages
-and protocols.
-
-Compared with similar tools, Isabelle's distinguishing feature is
-its flexibility. Most proof assistants are built around a single
-formal calculus, typically higher-order logic. Isabelle has the
-capacity to accept a variety of formal calculi. The distributed
-version supports higher-order logic but also axiomatic set theory
-and several other formalisms. See logics for more details.
-
-Isabelle is a joint project between Lawrence C. Paulson (University
-of Cambridge, UK) and Tobias Nipkow (Technical University of Munich,
-Germany).
-
-WWW: http://isabelle.in.tum.de
--- a/math/isabelle/pkg-plist
+++ b/math/isabelle/pkg-plist