Attachment 76258 Details for Bug 109958 – isabelle.diff

[patch] isabelle.diff

isabelle.diff (text/plain), 12.72 KB, created by Timothy Bourke on 2007-03-06 01:10:03 UTC

(hide)

Description:

Filename:

MIME Type:

Creator: Timothy Bourke

Created: 2007-03-06 01:10:03 UTC

Size: 12.72 KB

patch

obsolete

>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@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"

Actions: View | Diff

Attachments on bug 109958: 76258