ports/149736: update port: math/isabelle to version 2009.2

Timothy Beyer beyert at cs.ucr.edu
Tue Aug 17 13:00:14 UTC 2010


The following reply was made to PR ports/149736; it has been noted by GNATS.

From: Timothy Beyer <beyert at cs.ucr.edu>
To: bug-followup at FreeBSD.org
Cc: Timothy Beyer <beyert at cs.ucr.edu>
Subject: Re: ports/149736: update port: math/isabelle to version 2009.2
Date: Tue, 17 Aug 2010 05:56:39 -0700

 Upon building the port again a second time, it seems that it doesn't like the
 value of ML_HOME as /usr/local/bin, and now demands /usr/local/smlnj/bin/ for
 some reason.  I don't know why it matters now, but here is an alternative
 Makefile that will probably build on more machines (only one line is different
 than the initial Makefile that I submitted).
 
 Tim
 
 --- Makefile.diff begins here ---
 --- Makefile.orig	2010-03-27 23:39:25.000000000 -0700
 +++ Makefile	2010-08-17 05:32:55.000000000 -0700
 @@ -6,38 +6,45 @@
  #
  
  PORTNAME=	isabelle
 -PORTVERSION=	2009
 -PORTREVISION=	2
 +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
 +DISTNAME=	Isabelle2009-2
  .if !defined(NOPORTDOCS)
 -DISTFILES=	Isabelle2009.tar.gz \
 -		Isabelle2009_library.tar.gz \
 -		Isabelle2009_pdf.tar.gz
 +DISTFILES=	${DISTNAME}.tar.gz \
 +		${DISTNAME}_library.tar.gz
  .endif
  
  MAINTAINER=	beyert at cs.ucr.edu
  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
 +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
 -USE_EMACS=	yes # for EMACS_SITE_LISPDIR
 -EMACS_NO_BUILD_DEPENDS=yes
 -EMACS_NO_RUN_DEPENDS=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
 @@ -93,12 +100,12 @@
  HEAP_HOL_HOL4="@comment "
  .endif
  
 -.if defined(WITH_SMLNJ)
 +.if !defined(WITH_POLYML)
  ML_SYSTEM=	smlnj-110
 -ML_HOME=	${LOCALBASE}/bin
 +ML_HOME=	${LOCALBASE}/smlnj/bin
  ML_OPTIONS=	@SMLdebug=/dev/null
  .else
 -ML_SYSTEM=	polyml-5.2
 +ML_SYSTEM=	polyml-5.3
  ML_HOME=	${LOCALBASE}/bin
  ML_OPTIONS=	-H 500
  ML_DBASE=	""
 @@ -112,7 +119,7 @@
  		HEAP_HOL_WORD=${HEAP_HOL_WORD} \
  		HEAP_HOL_TLA=${HEAP_HOL_TLA} \
  		HEAP_HOL_HOL4=${HEAP_HOL_HOL4}
 -.if defined(WITH_SMLNJ)
 +.if !defined(WITH_POLYML)
  BUILD_DEPENDS+=	smlnj-devel>=110.71:${PORTSDIR}/lang/sml-nj-devel
  MAKE_ENV+=	SMLNJ_DEVEL=yes
  .else
 --- Makefile.diff ends here ---



More information about the freebsd-ports-bugs mailing list