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
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 ---
Responsible Changed From-To: freebsd-ports-bugs->makc I'll take it.
State Changed From-To: open->feedback It fails on tinderbox http://people.freebsd.org/~makc/tb/isabelle-2009.2.log. Any idea?
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"
State Changed From-To: feedback->closed Committed.