Bug 149736 - update port: math/isabelle to version 2009.2
Summary: update port: math/isabelle to version 2009.2
Status: Closed FIXED
Alias: None
Product: Ports & Packages
Classification: Unclassified
Component: Individual Port(s) (show other bugs)
Version: Latest
Hardware: Any Any
: Normal Affects Only Me
Assignee: Max Brazhnikov
URL:
Keywords:
Depends on:
Blocks:
 
Reported: 2010-08-17 13:20 UTC by Timothy Beyer
Modified: 2010-10-30 19:40 UTC (History)
1 user (show)

See Also:


Attachments
Makefile.diff (2.72 KB, patch)
2010-08-17 13:20 UTC, Timothy Beyer
no flags Details | Diff
files.diff (16.16 KB, patch)
2010-08-17 13:20 UTC, Timothy Beyer
no flags Details | Diff
file.diff (384.57 KB, patch)
2010-08-17 13:20 UTC, Timothy Beyer
no flags Details | Diff

Note You need to log in before you can comment on or make changes to this bug.
Description Timothy Beyer 2010-08-17 13:20:01 UTC
This patch makes the following changes:

-Updates math/isabelle to the latest version (in Makefile)

-Makes according changes to distinfo

-Makes according changes to pkg-plist (sorry it is a huge file)

-Makes according changes to files/ (removes a lot of outdated patches and adds new patches)

-Adds copyright information to Makefile

-Changes default compiler to SML/NJ: even though it was a slow build, (~ 8
hours on my machine) it was easy to build.  I will bring back Poly/ML again in
the future, but it needs a lot of patches to build, whereas SML/NJ needed no
patches to build at all.

-Emacs packages (eg. Proof General) are now optionally turned off, which is the
default

Fix: The included patches

--- distinfo.orig	2009-10-29 15:23:27.000000000 -0700
+++ distinfo	2010-08-16 14:23:09.000000000 -0700
@@ -1,9 +1,6 @@
-MD5 (Isabelle2009.tar.gz) = 2b7a8d49bfba64aac7227d692c15c27b
-SHA256 (Isabelle2009.tar.gz) = 49f8708962a89102cd25d9b5b7bf1298017c0689f9ced7741c124351b58f8e71
-SIZE (Isabelle2009.tar.gz) = 9073615
-MD5 (Isabelle2009_library.tar.gz) = 8ffcb7a25a4d110dd9060d7fbb582fc6
-SHA256 (Isabelle2009_library.tar.gz) = db605638e4c66ed74069a4370cb6be776901e6ada6dfdd5104536379dbd0beef
-SIZE (Isabelle2009_library.tar.gz) = 44856488
-MD5 (Isabelle2009_pdf.tar.gz) = 3e964988a4cb70d1589a8c89f1e3eac7
-SHA256 (Isabelle2009_pdf.tar.gz) = 0e451cabf1ece51cd989531dce14136b62c4138ace9bc618a1bd71d1c984ed70
-SIZE (Isabelle2009_pdf.tar.gz) = 5757069
+MD5 (Isabelle2009-2.tar.gz) = c3a5a87ac0026befc90693bc96a63c57
+SHA256 (Isabelle2009-2.tar.gz) = f92a275b78bd8844de47a5902e339b58f3b768c07a7fb19d8e606b68499d5ac4
+SIZE (Isabelle2009-2.tar.gz) = 25193255
+MD5 (Isabelle2009-2_library.tar.gz) = f46a014a1b2efc97716d388cd22a1555
+SHA256 (Isabelle2009-2_library.tar.gz) = 1cf4cc438185146367938308e01be2f29b793d6c343299aa697def9a098e63aa
+SIZE (Isabelle2009-2_library.tar.gz) = 54438382
--- distinfo.diff ends here ---
How-To-Repeat:     Apply the patches
Comment 1 Timothy Beyer 2010-08-17 13:43:16 UTC
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@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 ---
Comment 2 Timothy Beyer 2010-08-17 13:56:39 UTC
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@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 ---
Comment 3 Max Brazhnikov freebsd_committer 2010-09-24 20:55:28 UTC
Responsible Changed
From-To: freebsd-ports-bugs->makc

I'll take it.
Comment 4 Max Brazhnikov freebsd_committer 2010-09-25 21:20:12 UTC
State Changed
From-To: open->feedback

It fails on tinderbox 
http://people.freebsd.org/~makc/tb/isabelle-2009.2.log. Any idea?
Comment 5 dfilter service freebsd_committer 2010-10-30 19:34:31 UTC
makc        2010-10-30 18:34:26 UTC

  FreeBSD ports repository

  Modified files:
    math/isabelle        Makefile distinfo pkg-plist 
    math/isabelle/files  patch-etc-settings 
  Removed files:
    math/isabelle/files  patch-lib-scripts-run_smlnj 
                         patch-src-HOL-Tools-atp_manager.ML 
                         patch-src-HOL-Tools-atp_wrapper.ML 
                         patch-src-HOL-Tools-int_arith.ML 
                         patch-src-HOL-Tools-int_factor_simprocs.ML 
                         patch-src-HOL-Tools-nat_simprocs.ML 
  Log:
  Update to 2009.2
  
  PR:             ports/149736
  Submitted by:   Timothy Beyer (maintainer)
  
  Revision  Changes      Path
  1.16      +24 -19      ports/math/isabelle/Makefile
  1.7       +4 -9        ports/math/isabelle/distinfo
  1.7       +35 -80      ports/math/isabelle/files/patch-etc-settings
  1.5       +0 -25       ports/math/isabelle/files/patch-lib-scripts-run_smlnj (dead)
  1.2       +0 -15       ports/math/isabelle/files/patch-src-HOL-Tools-atp_manager.ML (dead)
  1.2       +0 -18       ports/math/isabelle/files/patch-src-HOL-Tools-atp_wrapper.ML (dead)
  1.2       +0 -29       ports/math/isabelle/files/patch-src-HOL-Tools-int_arith.ML (dead)
  1.2       +0 -65       ports/math/isabelle/files/patch-src-HOL-Tools-int_factor_simprocs.ML (dead)
  1.2       +0 -83       ports/math/isabelle/files/patch-src-HOL-Tools-nat_simprocs.ML (dead)
  1.9       +3832 -2836  ports/math/isabelle/pkg-plist
_______________________________________________
cvs-all@freebsd.org mailing list
http://lists.freebsd.org/mailman/listinfo/cvs-all
To unsubscribe, send any mail to "cvs-all-unsubscribe@freebsd.org"
Comment 6 Max Brazhnikov freebsd_committer 2010-10-30 19:38:02 UTC
State Changed
From-To: feedback->closed

Committed.