mirror of
https://git.FreeBSD.org/ports.git
synced 2024-12-26 05:02:18 +00:00
0002baf188
Updates the port to the latest Isabelle release. It does not seem worth the effort to continually patch the bash script files to make them work under sh, hence the large number of removed files. PR: ports/126067 Submitted by: Timothy Bourke <timbob@bigpond.com>
186 lines
4.9 KiB
Makefile
186 lines
4.9 KiB
Makefile
# New ports collection makefile for: isabelle
|
|
# Date created: 08 August 2005
|
|
# Whom: Timothy Bourke <timbob@bigpond.com>
|
|
#
|
|
# $FreeBSD$
|
|
#
|
|
|
|
PORTNAME= isabelle
|
|
PORTVERSION= 2008
|
|
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= Isabelle2008
|
|
.if !defined(NOPORTDOCS)
|
|
DISTFILES= Isabelle2008.tar.gz \
|
|
Isabelle2008_library.tar.gz \
|
|
Isabelle2008_pdf.tar.gz
|
|
.endif
|
|
|
|
MAINTAINER= timbob@bigpond.com
|
|
COMMENT= A generic proof assistant
|
|
|
|
OPTIONS= SMLNJ "Use SML/NJ (devel) instead of faster Poly/ML" off
|
|
OPTIONS+= RLWRAP "Use rlwrap as line editor" on
|
|
OPTIONS+= LEDIT "Use ledit as line editor" off
|
|
OPTIONS+= HOL_ALGEBRA "Build optional heap: HOL-Algebra" off
|
|
OPTIONS+= HOL_COMPLEX "Build optional heap: HOL-Complex" off
|
|
OPTIONS+= HOL_MATRIX "Build optional heap: HOL-Complex-Matrix" off
|
|
OPTIONS+= HOL_NOMINAL "Build optional heap: HOL-Nominal" off
|
|
OPTIONS+= HOL_WORD "Build optional heap: HOL-Word" off
|
|
OPTIONS+= HOL_TLA "Build optional heap: TLA" off
|
|
OPTIONS+= HOL_HOL4 "Build optional heap: HOL4" off
|
|
OPTIONS+= HOLCF_IOA "Build optional heap: IOA" off
|
|
|
|
USE_PERL5= yes
|
|
BUILD_DEPENDS+= bash:${PORTSDIR}/shells/bash
|
|
RUN_DEPENDS+= proofgeneral:${PORTSDIR}/math/proofgeneral
|
|
RUN_DEPENDS+= bash:${PORTSDIR}/shells/bash
|
|
|
|
DOCFILES= Contents *.pdf *.eps *.ps *.dvi
|
|
|
|
.include <bsd.port.pre.mk>
|
|
|
|
.if defined(WITH_RLWRAP)
|
|
RUN_DEPENDS+= rlwrap:${PORTSDIR}/devel/rlwrap
|
|
LINE_EDIT= "${PREFIX}/bin/rlwrap"
|
|
.else
|
|
.if defined(WITH_LEDIT)
|
|
RUN_DEPENDS+= ledit:${PORTSDIR}/sysutils/ledit
|
|
LINE_EDIT= "${PREFIX}/bin/ledit"
|
|
.else
|
|
LINE_EDIT= ""
|
|
.endif
|
|
.endif
|
|
|
|
.if defined(WITH_HOL_ALGEBRA)
|
|
HEAP_HOL_ALGEBRA=""
|
|
.else
|
|
HEAP_HOL_ALGEBRA="@comment "
|
|
.endif
|
|
.if defined(WITH_HOL_COMPLEX)
|
|
HEAP_HOL_COMPLEX=""
|
|
.else
|
|
HEAP_HOL_COMPLEX="@comment "
|
|
.endif
|
|
.if defined(WITH_HOL_MATRIX)
|
|
HEAP_HOL_COMPLEX_MATRIX=""
|
|
.else
|
|
HEAP_HOL_COMPLEX_MATRIX="@comment "
|
|
.endif
|
|
.if defined(WITH_HOL_NOMINAL)
|
|
HEAP_HOL_NOMINAL=""
|
|
.else
|
|
HEAP_HOL_NOMINAL="@comment "
|
|
.endif
|
|
.if defined(WITH_HOL_WORD)
|
|
HEAP_HOL_WORD=""
|
|
.else
|
|
HEAP_HOL_WORD="@comment "
|
|
.endif
|
|
.if defined(WITH_HOL_TLA)
|
|
HEAP_HOL_TLA=""
|
|
.else
|
|
HEAP_HOL_TLA="@comment "
|
|
.endif
|
|
.if defined(WITH_HOL_HOL4)
|
|
HEAP_HOL_HOL4=""
|
|
.else
|
|
HEAP_HOL_HOL4="@comment "
|
|
.endif
|
|
.if defined(WITH_HOLCF_IOA)
|
|
HEAP_HOLCF_IOA=""
|
|
.else
|
|
HEAP_HOLCF_IOA="@comment "
|
|
.endif
|
|
|
|
.if defined(WITH_SMLNJ)
|
|
ML_SYSTEM= smlnj-110
|
|
ML_HOME= ${LOCALBASE}/bin
|
|
ML_OPTIONS= @SMLdebug=/dev/null
|
|
.else
|
|
ML_SYSTEM= polyml-5.2
|
|
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_COMPLEX=${HEAP_HOL_COMPLEX} \
|
|
HEAP_HOL_COMPLEX_MATRIX=${HEAP_HOL_COMPLEX_MATRIX} \
|
|
HEAP_HOL_NOMINAL=${HEAP_HOL_NOMINAL} \
|
|
HEAP_HOL_WORD=${HEAP_HOL_WORD} \
|
|
HEAP_HOL_TLA=${HEAP_HOL_TLA} \
|
|
HEAP_HOL_HOL4=${HEAP_HOL_HOL4} \
|
|
HEAP_HOLCF_IOA=${HEAP_HOLCF_IOA}
|
|
.if defined(WITH_SMLNJ)
|
|
BUILD_DEPENDS+= smlnj-devel>=110.65:${PORTSDIR}/lang/sml-nj-devel
|
|
MAKE_ENV+= SMLNJ_DEVEL=yes
|
|
.else
|
|
BUILD_DEPENDS+= polyml>=5.2:${PORTSDIR}/lang/polyml
|
|
RUN_DEPENDS+= polyml>=5.2:${PORTSDIR}/lang/polyml
|
|
.endif
|
|
|
|
NO_INSTALL_MANPAGES=yes
|
|
|
|
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}|" \
|
|
${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(WITH_HOL_ALGEBRA)
|
|
${WRKSRC}/build -b -m HOL-Algebra HOL
|
|
.endif
|
|
.if defined(WITH_HOL_COMPLEX)
|
|
${WRKSRC}/build -b -m HOL-Complex HOL
|
|
.endif
|
|
.if defined(WITH_HOL_MATRIX)
|
|
${WRKSRC}/build -b -m HOL-Complex-Matrix HOL
|
|
.endif
|
|
.if defined(WITH_HOL_NOMINAL)
|
|
${WRKSRC}/build -b -m HOL-Nominal HOL
|
|
.endif
|
|
.if defined(WITH_HOL_WORD)
|
|
${WRKSRC}/build -b -m HOL-Word HOL
|
|
.endif
|
|
.if defined(WITH_HOL_TLA)
|
|
${WRKSRC}/build -b -m TLA HOL
|
|
.endif
|
|
.if defined(WITH_HOL_HOL4)
|
|
${WRKSRC}/build -b -m HOL4 HOL
|
|
.endif
|
|
.if defined(WITH_HOLCF_IOA)
|
|
${WRKSRC}/build -b -m IOA HOLCF
|
|
.endif
|
|
|
|
post-install:
|
|
${WRKSRC}/bin/isatool ${INSTALL} -d ${PREFIX}/share/isabelle -p ${PREFIX}/bin
|
|
.if !defined(NOPORTDOCS)
|
|
${MKDIR} ${DOCSDIR}
|
|
.for file in ${DOCFILES}
|
|
${INSTALL_DATA} ${WRKSRC}/doc/${file} ${DOCSDIR}
|
|
.endfor
|
|
(cd ${WRKSRC}; \
|
|
${FIND} -d browser_info -type d -exec ${MKDIR} ${DOCSDIR}/{} \; ; \
|
|
${FIND} -d browser_info -type f -exec ${INSTALL_DATA} {} ${DOCSDIR}/{} \;)
|
|
.endif
|
|
|
|
.include <bsd.port.post.mk>
|