Attachment #108820 for bug #149736

View | Details | Raw Unified | Return to bug 149736 | Differences between
Collapse All | Expand All




#

PORTNAME=	isabelle
PORTVERSION=	2009.2
PORTREVISION=	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
.if !defined(NOPORTDOCS)
DISTFILES=	${DISTNAME}.tar.gz \
		${DISTNAME}_library.tar.gz
		Isabelle2009_pdf.tar.gz
.endif

MAINTAINER=	beyert@cs.ucr.edu
COMMENT=	A generic proof assistant

LICENSE=	BSD
LICENSE_FILE=	${WRKSRC}/COPYRIGHT

OPTIONS=	POLYML  "Use Poly/ML (fast but broken) instead of SML/NJ" 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_NOMINAL  "Build optional heap: HOL-Nominal"           off
OPTIONS+=	HOL_NSA      "Build optional heap: HOL-NSA"               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+=	EMACS_PKG    "Build with Emacs Packages"                  off

USE_PERL5=	yes

.if defined(WITH_EMACS_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+=	proofgeneral:${PORTSDIR}/math/proofgeneral
RUN_DEPENDS+=	bash:${PORTSDIR}/shells/bash

DOCFILES=	Contents *.pdf *.eps *.ps *.dvi

HEAP_HOL_HOL4="@comment "
.endif

.if !defined(WITH_POLYML)
ML_SYSTEM=	smlnj-110
ML_HOME=	${LOCALBASE}/bin
ML_OPTIONS=	@SMLdebug=/dev/null
.else
ML_SYSTEM=	polyml-5.3
ML_HOME=	${LOCALBASE}/bin
ML_OPTIONS=	-H 500
ML_DBASE=	""

		HEAP_HOL_WORD=${HEAP_HOL_WORD} \
		HEAP_HOL_TLA=${HEAP_HOL_TLA} \
		HEAP_HOL_HOL4=${HEAP_HOL_HOL4}
.if !defined(WITH_POLYML)
BUILD_DEPENDS+=	smlnj-devel>=110.71:${PORTSDIR}/lang/sml-nj-devel
MAKE_ENV+=	SMLNJ_DEVEL=yes
.else

Return to bug 149736

Lines 6-43 Link Here

(-)Makefile (-16 / +23 lines)
6	#	6	#
7		7
8	PORTNAME= isabelle	8	PORTNAME= isabelle
9	PORTVERSION= 2009	9	PORTVERSION= 2009.2
10	PORTREVISION= 2
11	CATEGORIES= math	10	CATEGORIES= math
12	MASTER_SITES= http://isabelle.in.tum.de/dist/ \	11	MASTER_SITES= http://isabelle.in.tum.de/dist/ \
13	http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ \	12	http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ \
14	http://mirror.cse.unsw.edu.au/pub/isabelle/dist/	13	http://mirror.cse.unsw.edu.au/pub/isabelle/dist/
15	DISTNAME= Isabelle2009	14	DISTNAME= Isabelle2009-2
16	.if !defined(NOPORTDOCS)	15	.if !defined(NOPORTDOCS)
17	DISTFILES= Isabelle2009.tar.gz \	16	DISTFILES= ${DISTNAME}.tar.gz \
18	Isabelle2009_library.tar.gz \	17	${DISTNAME}_library.tar.gz
19	Isabelle2009_pdf.tar.gz
20	.endif	18	.endif
21		19
22	MAINTAINER= beyert@cs.ucr.edu	20	MAINTAINER= beyert@cs.ucr.edu
23	COMMENT= A generic proof assistant	21	COMMENT= A generic proof assistant
24		22
25	OPTIONS= SMLNJ "Use SML/NJ (devel) instead of faster Poly/ML" off	23	LICENSE= BSD
26	OPTIONS+= RLWRAP "Use rlwrap as line editor" on	24	LICENSE_FILE= ${WRKSRC}/COPYRIGHT
27	OPTIONS+= LEDIT "Use ledit as line editor" off	25
		26	OPTIONS= POLYML "Use Poly/ML (fast but broken) instead of SML/NJ" off
		27	OPTIONS+= RLWRAP "Use rlwrap as line editor" on
		28	OPTIONS+= LEDIT "Use ledit as line editor" off
28	OPTIONS+= HOL_ALGEBRA "Build optional heap: HOL-Algebra" off	29	OPTIONS+= HOL_ALGEBRA "Build optional heap: HOL-Algebra" off
29	OPTIONS+= HOL_NOMINAL "Build optional heap: HOL-Nominal" off	30	OPTIONS+= HOL_NOMINAL "Build optional heap: HOL-Nominal" off
30	OPTIONS+= HOL_NSA "Build optional heap: HOL-NSA" off	31	OPTIONS+= HOL_NSA "Build optional heap: HOL-NSA" off
31	OPTIONS+= HOL_WORD "Build optional heap: HOL-Word" off	32	OPTIONS+= HOL_WORD "Build optional heap: HOL-Word" off
32	OPTIONS+= HOL_TLA "Build optional heap: TLA" off	33	OPTIONS+= HOL_TLA "Build optional heap: TLA" off
33	OPTIONS+= HOL_HOL4 "Build optional heap: HOL4" off	34	OPTIONS+= HOL_HOL4 "Build optional heap: HOL4" off
		35	OPTIONS+= EMACS_PKG "Build with Emacs Packages" off
34		36
35	USE_PERL5= yes	37	USE_PERL5= yes
36	USE_EMACS= yes # for EMACS_SITE_LISPDIR	38
37	EMACS_NO_BUILD_DEPENDS=yes	39	.if defined(WITH_EMACS_PKG)
38	EMACS_NO_RUN_DEPENDS=yes	40	USE_EMACS= yes # for EMACS_SITE_LISPDIR
		41	EMACS_NO_BUILD_DEPENDS=yes
		42	EMACS_NO_RUN_DEPENDS=yes
		43	RUN_DEPENDS+= proofgeneral:${PORTSDIR}/math/proofgeneral
		44	.else
		45	.endif
		46
39	BUILD_DEPENDS+= bash:${PORTSDIR}/shells/bash	47	BUILD_DEPENDS+= bash:${PORTSDIR}/shells/bash
40	RUN_DEPENDS+= proofgeneral:${PORTSDIR}/math/proofgeneral
41	RUN_DEPENDS+= bash:${PORTSDIR}/shells/bash	48	RUN_DEPENDS+= bash:${PORTSDIR}/shells/bash
42		49
43	DOCFILES= Contents .pdf .eps .ps .dvi	50	DOCFILES= Contents .pdf .eps .ps .dvi
Lines 93-104 Link Here
93	HEAP_HOL_HOL4="@comment "	100	HEAP_HOL_HOL4="@comment "
94	.endif	101	.endif
95		102
96	.if defined(WITH_SMLNJ)	103	.if !defined(WITH_POLYML)
97	ML_SYSTEM= smlnj-110	104	ML_SYSTEM= smlnj-110
98	ML_HOME= ${LOCALBASE}/bin	105	ML_HOME= ${LOCALBASE}/bin
99	ML_OPTIONS= @SMLdebug=/dev/null	106	ML_OPTIONS= @SMLdebug=/dev/null
100	.else	107	.else
101	ML_SYSTEM= polyml-5.2	108	ML_SYSTEM= polyml-5.3
102	ML_HOME= ${LOCALBASE}/bin	109	ML_HOME= ${LOCALBASE}/bin
103	ML_OPTIONS= -H 500	110	ML_OPTIONS= -H 500
104	ML_DBASE= ""	111	ML_DBASE= ""
Lines 112-118 Link Here
112	HEAP_HOL_WORD=${HEAP_HOL_WORD} \	119	HEAP_HOL_WORD=${HEAP_HOL_WORD} \
113	HEAP_HOL_TLA=${HEAP_HOL_TLA} \	120	HEAP_HOL_TLA=${HEAP_HOL_TLA} \
114	HEAP_HOL_HOL4=${HEAP_HOL_HOL4}	121	HEAP_HOL_HOL4=${HEAP_HOL_HOL4}
115	.if defined(WITH_SMLNJ)	122	.if !defined(WITH_POLYML)
116	BUILD_DEPENDS+= smlnj-devel>=110.71:${PORTSDIR}/lang/sml-nj-devel	123	BUILD_DEPENDS+= smlnj-devel>=110.71:${PORTSDIR}/lang/sml-nj-devel
117	MAKE_ENV+= SMLNJ_DEVEL=yes	124	MAKE_ENV+= SMLNJ_DEVEL=yes
118	.else	125	.else