mirror of
https://git.FreeBSD.org/ports.git
synced 2024-12-25 04:43:33 +00:00
- Fix crash with lang/polyml.
PR: 109958 Submitted by: Timothy Bourke <timbob@bigpond.com> (maintainer)
This commit is contained in:
Martin Wilke
parent
df0f59df76
commit
6c11582094
Notes:
svn2git
2021-03-31 03:12:20 +00:00
svn path=/head/; revision=188004
@ -22,7 +22,6 @@ MAINTAINER= timbob@bigpond.com
|
||||
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 @@ NO_PACKAGE= Requires non-standard kernel setting.
|
||||
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 @@ RUN_DEPENDS+= proofgeneral:${PORTSDIR}/math/proofgeneral
|
||||
|
||||
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 @@ NO_INSTALL_MANPAGES=yes
|
||||
|
||||
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 @@ post-patch:
|
||||
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)
|
||||
|
||||
@ -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). !
|
||||
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
||||
@ -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%%
|
||||
|
||||
###
|
||||
|
||||
@ -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";
|
||||
@ -1,9 +1,7 @@
|
||||
(* Title: Pure/ML-Systems/polyml-4.1.4-patch.ML
|
||||
ID: $Id$
|
||||
Author: Makarius
|
||||
(* 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 $
|
||||
|
||||
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit
|
||||
this into ML_dbase!
|
||||
Compatibility wrapper for Poly/ML 5.0 -- version for Isabelle2005.
|
||||
*)
|
||||
|
||||
structure Posix =
|
||||
@ -29,3 +27,7 @@ struct
|
||||
val all = full;
|
||||
end;
|
||||
|
||||
|
||||
use "ML-Systems/polyml.ML";
|
||||
|
||||
val pointer_eq = PolyML.pointerEq;
|
||||
17
math/isabelle/files/proofgeneral-settings.el
Normal file
17
math/isabelle/files/proofgeneral-settings.el
Normal file
@ -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)))
|
||||
|
||||
93
math/isabelle/files/run-polyml-5.0
Normal file
93
math/isabelle/files/run-polyml-5.0
Normal file
@ -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"
|
||||
@ -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
|
||||
@ -2070,6 +2070,7 @@ bin/isatool
|
||||
%%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 @@ bin/isatool
|
||||
%%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
|
||||
|
||||
Loading…
Reference in New Issue
Block a user