ports/109958: Update port: math/isabelle for Poly/ML 5.0
Timothy Bourke
timbob at bigpond.com
Tue Mar 6 01:10:04 UTC 2007
>Number: 109958
>Category: ports
>Synopsis: Update port: math/isabelle for Poly/ML 5.0
>Confidential: no
>Severity: non-critical
>Priority: low
>Responsible: freebsd-ports-bugs
>State: open
>Quarter:
>Keywords:
>Date-Required:
>Class: maintainer-update
>Submitter-Id: current-users
>Arrival-Date: Tue Mar 06 01:10:03 GMT 2007
>Closed-Date:
>Last-Modified:
>Originator: Timothy Bourke
>Release: FreeBSD 6.1-RELEASE-p6 i386 (uname -s -r -m)
>Organization:
n/a
>Environment:
>Description:
Update the Isabelle port to work with newly submitted
lang/polyml port (ports/109951).
Includes Makarius' patch files.
>How-To-Repeat:
>Fix:
--- isabelle.diff begins here ---
Index: Makefile
===================================================================
RCS file: /home/ncvs/ports/math/isabelle/Makefile,v
retrieving revision 1.3
diff -u -r1.3 Makefile
--- Makefile 10 Aug 2006 12:04:59 -0000 1.3
+++ Makefile 6 Mar 2007 00:40:00 -0000
@@ -2,7 +2,7 @@
# Date created: 08 August 2005
# Whom: Timothy Bourke <timbob at bigpond.com>
#
-# $FreeBSD: ports/math/isabelle/Makefile,v 1.3 2006/08/10 12:04:59 rafan Exp $
+# $FreeBSD$
#
PORTNAME= isabelle
@@ -22,7 +22,6 @@
COMMENT= A generic proof assistant
OPTIONS= SMLNJ "Use SML/NJ (devel) instead of the faster Poly/ML" Off
-NO_PACKAGE= Requires non-standard kernel setting.
.include <bsd.port.pre.mk>
@@ -30,11 +29,13 @@
ML_SYSTEM= smlnj-110
ML_HOME= ${LOCALBASE}/smlnj/bin
ML_OPTIONS= @SMLdebug=/dev/null
+ML_PLATFORM= x86-bsd
.else
-ML_SYSTEM= polyml-4.2.0
-ML_HOME= ${LOCALBASE}/lib/polyml/
-ML_OPTIONS= -H 80
+ML_SYSTEM= polyml-5.0
+ML_HOME= ${LOCALBASE}/bin
+ML_OPTIONS= -H 500
ML_DBASE= ""
+ML_PLATFORM= ""
.endif
USE_PERL5= yes
@@ -43,12 +44,12 @@
DOCFILES= Contents *.pdf *.eps *.ps *.dvi
-PLIST_SUB= HEAPSUBDIR=${ML_SYSTEM}_x86-bsd
-
.if defined(WITH_SMLNJ)
+PLIST_SUB= HEAPSUBDIR=${ML_SYSTEM}_${ML_PLATFORM}
BUILD_DEPENDS+= sml:${PORTSDIR}/lang/sml-nj-devel
RUN_DEPENDS+= sml:${PORTSDIR}/lang/sml-nj-devel
.else
+PLIST_SUB= HEAPSUBDIR=${ML_SYSTEM}
BUILD_DEPENDS+= poly:${PORTSDIR}/lang/polyml
RUN_DEPENDS+= poly:${PORTSDIR}/lang/polyml
.endif
@@ -57,8 +58,12 @@
post-extract:
@${CP} ${FILESDIR}/Makefile ${WRKSRC}
- @${CP} ${FILESDIR}/polyml-4.1.4-patch.ML ${WRKSRC}/src/Pure/ML-Systems/
- @${CP} ${FILESDIR}/polyml-4.2.0.ML ${WRKSRC}/src/Pure/ML-Systems/
+ @${CP} ${FILESDIR}/run-polyml-5.0 ${WRKSRC}/lib/scripts/
+ @${CHMOD} ugo+x ${WRKSRC}/lib/scripts/run-polyml-5.0
+ @${CP} ${FILESDIR}/polyml-5.0.ML ${WRKSRC}/src/Pure/ML-Systems/
+.if !defined(WITH_SMLNJ)
+ @${CP} ${FILESDIR}/proofgeneral-settings.el ${WRKSRC}/etc/
+.endif
post-patch:
@${MV} ${WRKSRC}/etc/settings ${WRKSRC}/etc/settings.presed
@@ -66,19 +71,12 @@
s|%%ML_HOME%%|${ML_HOME}|; \
s|%%ML_OPTIONS%%|\"${ML_OPTIONS}\"|; \
s|%%ML_DBASE%%|${ML_DBASE}|; \
+ s|%%ML_PLATFORM%%|${ML_PLATFORM}|; \
s|%%PREFIX%%|${PREFIX}|" \
${WRKSRC}/etc/settings.presed > ${WRKSRC}/etc/settings
@${RM} ${WRKSRC}/etc/settings.presed
@${TOUCH} ${WRKSRC}/contrib/.keep
-pre-build:
-.if !defined(WITH_SMLNJ)
- @if ${TEST} `ulimit -Hd` -lt 917504; then \
- ${CAT} ${FILESDIR}/badmaxdsiz; \
- exit 1; \
- fi
-.endif
-
post-install:
${WRKSRC}/bin/isatool ${INSTALL} -d ${PREFIX}/share/isabelle -p ${PREFIX}/bin
.if !defined(NOPORTDOCS)
Index: pkg-install
===================================================================
RCS file: pkg-install
diff -N pkg-install
--- pkg-install 1 Sep 2005 10:03:58 -0000 1.1
+++ /dev/null 1 Jan 1970 00:00:00 -0000
@@ -1,23 +0,0 @@
-#!/bin/sh
-
-if [ "$2" = "POST-INSTALL" ]; then
- if test `ulimit -Hd` -lt 917504; then
- cat <<END
-!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-! The system process data segment value is too low! !
-! !
-! Under these circumstances Isabelle may not function reliably, or !
-! may fail completely. !
-! !
-! The setting may be viewed and modified with the commands: !
-! sh: ulimit -Hd !
-! csh: limit -h datasize !
-! !
-! It may be necessary to lift the maximum limit. One way of doing !
-! this is to add a line to /boot/loader.conf and then to restart the !
-! system: !
-! kern.maxdsiz="896M" !
-!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-END
- fi
-fi
Index: pkg-plist
===================================================================
RCS file: /home/ncvs/ports/math/isabelle/pkg-plist,v
retrieving revision 1.3
diff -u -r1.3 pkg-plist
--- pkg-plist 23 Jun 2006 02:29:06 -0000 1.3
+++ pkg-plist 6 Mar 2007 00:40:01 -0000
@@ -2070,6 +2070,7 @@
%%DATADIR%%/lib/scripts/polyml-version
%%DATADIR%%/lib/scripts/run-mosml
%%DATADIR%%/lib/scripts/run-polyml
+%%DATADIR%%/lib/scripts/run-polyml-5.0
%%DATADIR%%/lib/scripts/run-smlnj
%%DATADIR%%/lib/scripts/showtime
%%DATADIR%%/lib/scripts/unsymbolize.pl
@@ -3341,8 +3342,7 @@
%%DATADIR%%/src/Pure/ML-Systems/cpu-timer-basis.ML
%%DATADIR%%/src/Pure/ML-Systems/cpu-timer-gc.ML
%%DATADIR%%/src/Pure/ML-Systems/mosml.ML
-%%DATADIR%%/src/Pure/ML-Systems/polyml-4.1.4-patch.ML
-%%DATADIR%%/src/Pure/ML-Systems/polyml-4.2.0.ML
+%%DATADIR%%/src/Pure/ML-Systems/polyml-5.0.ML
%%DATADIR%%/src/Pure/ML-Systems/polyml-posix.ML
%%DATADIR%%/src/Pure/ML-Systems/polyml-time-limit.ML
%%DATADIR%%/src/Pure/ML-Systems/polyml.ML
Index: files/badmaxdsiz
===================================================================
RCS file: files/badmaxdsiz
diff -N files/badmaxdsiz
--- files/badmaxdsiz 1 Sep 2005 10:03:58 -0000 1.1
+++ /dev/null 1 Jan 1970 00:00:00 -0000
@@ -1,18 +0,0 @@
-!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-! The system process data segment value is too low! !
-! !
-! Under these circumstances the Isabelle build process for logics !
-! such as HOL will not terminate, or otherwise fail. !
-! !
-! The setting may be viewed and modified with the commands: !
-! sh: ulimit -Hd !
-! csh: limit -h datasize !
-! !
-! It may be necessary to lift the maximum limit. One way of doing !
-! this is to add a line to /boot/loader.conf and then to restart the !
-! system: !
-! kern.maxdsiz="896M" !
-! !
-! This problem only affects Poly/ML. Isabelle may also be configured !
-! to use SML/NJ (build with WITH_SMLNJ=yes). !
-!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
Index: files/patch-etc-settings
===================================================================
RCS file: /home/ncvs/ports/math/isabelle/files/patch-etc-settings,v
retrieving revision 1.2
diff -u -r1.2 patch-etc-settings
--- files/patch-etc-settings 1 May 2006 18:01:58 -0000 1.2
+++ files/patch-etc-settings 6 Mar 2007 00:40:01 -0000
@@ -34,7 +34,7 @@
+ML_SYSTEM=%%ML_SYSTEM%%
+ML_HOME=%%ML_HOME%%
+ML_OPTIONS=%%ML_OPTIONS%%
-+ML_PLATFORM=x86-bsd
++ML_PLATFORM=%%ML_PLATFORM%%
+ML_DBASE=%%ML_DBASE%%
###
Index: files/polyml-4.1.4-patch.ML
===================================================================
RCS file: files/polyml-4.1.4-patch.ML
diff -N files/polyml-4.1.4-patch.ML
--- files/polyml-4.1.4-patch.ML 1 May 2006 18:01:58 -0000 1.1
+++ /dev/null 1 Jan 1970 00:00:00 -0000
@@ -1,31 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-4.1.4-patch.ML
- ID: $Id$
- Author: Makarius
-
-Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit
-this into ML_dbase!
-*)
-
-structure Posix =
-struct
- open Posix;
- structure IO =
- struct
- open IO;
- val mkReader = mkTextReader;
- val mkWriter = mkTextWriter;
- end;
-end;
-
-structure TextIO =
-struct
- open TextIO;
- fun inputLine is = Option.getOpt (TextIO.inputLine is, "");
-end;
-
-structure Substring =
-struct
- open Substring;
- val all = full;
-end;
-
Index: files/polyml-4.2.0.ML
===================================================================
RCS file: files/polyml-4.2.0.ML
diff -N files/polyml-4.2.0.ML
--- files/polyml-4.2.0.ML 1 May 2006 18:01:58 -0000 1.1
+++ /dev/null 1 Jan 1970 00:00:00 -0000
@@ -1,9 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-4.2.0.ML
- ID: $Id: polyml-4.2.0.ML,v 1.1 2005/11/14 13:36:46 wenzelm Exp $
- Author: Makarius
-
-Compatibility wrapper for Poly/ML 4.2.0.
-*)
-
-use "ML-Systems/polyml-4.1.4-patch.ML";
-use "ML-Systems/polyml.ML";
Index: files/polyml-5.0.ML
===================================================================
RCS file: files/polyml-5.0.ML
diff -N files/polyml-5.0.ML
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ files/polyml-5.0.ML 6 Mar 2007 00:40:01 -0000
@@ -0,0 +1,33 @@
+(* Title: Pure/ML-Systems/polyml-5.0.ML
+ ID: $Id: polyml-5.0.ML,v 1.1 2006/12/07 13:11:39 wenzelm Exp $
+
+Compatibility wrapper for Poly/ML 5.0 -- version for Isabelle2005.
+*)
+
+structure Posix =
+struct
+ open Posix;
+ structure IO =
+ struct
+ open IO;
+ val mkReader = mkTextReader;
+ val mkWriter = mkTextWriter;
+ end;
+end;
+
+structure TextIO =
+struct
+ open TextIO;
+ fun inputLine is = Option.getOpt (TextIO.inputLine is, "");
+end;
+
+structure Substring =
+struct
+ open Substring;
+ val all = full;
+end;
+
+
+use "ML-Systems/polyml.ML";
+
+val pointer_eq = PolyML.pointerEq;
Index: files/proofgeneral-settings.el
===================================================================
RCS file: files/proofgeneral-settings.el
diff -N files/proofgeneral-settings.el
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ files/proofgeneral-settings.el 6 Mar 2007 00:40:01 -0000
@@ -0,0 +1,17 @@
+;;;
+;;; $Id: proofgeneral-settings.el,v 1.2 2001/09/28 18:08:05 wenzelm Exp $
+;;;
+;;; Options for Proof General
+
+;; Examples for sensible settings:
+
+;(custom-set-variables '(isar-eta-contract nil))
+
+;(custom-set-faces
+; '(proof-locked-face
+; ((((type x) (class color) (background light)) (:background "lightsteelblue2")))))
+
+; Makarius' Poly/ML 5.0 patches
+(custom-set-variables
+ '(proof-shell-pre-interrupt-hook (lambda () t)))
+
Index: files/run-polyml-5.0
===================================================================
RCS file: files/run-polyml-5.0
diff -N files/run-polyml-5.0
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ files/run-polyml-5.0 6 Mar 2007 00:40:01 -0000
@@ -0,0 +1,93 @@
+#!/usr/bin/env bash
+#
+# $Id: run-polyml-5.0,v 1.2 2006/12/08 21:18:35 wenzelm Exp $
+# Author: Makarius
+#
+# Poly/ML startup script (for 5.0)
+
+export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+
+
+## diagnostics
+
+function fail_out()
+{
+ echo "Unable to create output heap file: \"$OUTFILE\"" >&2
+ exit 2
+}
+
+function check_file()
+{
+ if [ ! -f "$1" ]; then
+ echo "Unable to locate $1" >&2
+ echo "Please check your ML system settings!" >&2
+ exit 2
+ fi
+}
+
+
+## compiler executables and libraries
+
+POLY="$ML_HOME/poly"
+check_file "$POLY"
+
+if [ "$(basename "$ML_HOME")" = bin ]; then
+ POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)"
+else
+ POLYLIB="$ML_HOME"
+fi
+
+export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH"
+export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH"
+
+
+## prepare databases
+
+if [ -z "$INFILE" ]; then
+ EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
+else
+ check_file "$INFILE"
+ POLY="$INFILE"
+ EXIT=""
+fi
+
+ROOT_FUNCTION="fn () => (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.rootFunction ())"
+
+if [ -z "$OUTFILE" ]; then
+ COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
+else
+ if [ -z "$COMPRESS" ]; then
+ COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
+ else
+ COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
+ fi
+ [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+ rm -f "${OUTFILE}.o" || fail_out
+fi
+
+
+## run it!
+
+MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $EXIT $COMMIT $MLTEXT"
+MLEXIT="commit();"
+
+if [ -z "$TERMINATE" ]; then
+ FEEDER_OPTS=""
+else
+ FEEDER_OPTS="-q"
+fi
+
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+ { read FPID; "$POLY" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+RC="$?"
+
+if [ -n "$OUTFILE" ]; then
+ if [ -e "${OUTFILE}.o" ]; then
+ cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml -lstdc++ || fail_out
+ rm -f "${OUTFILE}.o"
+ [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
+ fi
+ [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+fi
+
+exit "$RC"
--- isabelle.diff ends here ---
>Release-Note:
>Audit-Trail:
>Unformatted:
More information about the freebsd-ports-bugs
mailing list