sync/ports
1
0
Fork 0
mirror of https://git.freebsd.org/ports.git synced 2025-07-18 17:59:20 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

[MAINTAINER] math/isabelle: update from 2007 to 2008

Browse source 
Updates the port to the latest Isabelle release. It does
	not seem worth the effort to continually patch the bash
	script files to make them work under sh, hence the large
	number of removed files.

PR:		ports/126067
Submitted by:	Timothy Bourke <timbob@bigpond.com>
This commit is contained in:
Edwin Groothuis 2008-08-15 04:33:04 +00:00
parent 3baea6f442
commit 0002baf188
Notes: svn2git 2021-03-31 03:12:20 +00:00 
svn path=/head/; revision=218598
52 changed files with 320 additions and 1653 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

123
math/isabelle/Makefile
View file

@ -6,50 +6,122 @@
#
PORTNAME= isabelle
PORTVERSION= 2007
PORTREVISION= 1
PORTVERSION= 2008
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= Isabelle2007
DISTNAME= Isabelle2008
.if !defined(NOPORTDOCS)
DISTFILES= Isabelle2007.tar.gz \
Isabelle2007_library.tar.gz \
Isabelle2007_pdf.tar.gz
DISTFILES= Isabelle2008.tar.gz \
Isabelle2008_library.tar.gz \
Isabelle2008_pdf.tar.gz
.endif
MAINTAINER= timbob@bigpond.com
COMMENT= A generic proof assistant
OPTIONS= SMLNJ "Use SML/NJ (devel) instead of the faster Poly/ML" off
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
OPTIONS+= HOL_ALGEBRA "Build optional heap: HOL-Algebra" off
OPTIONS+= HOL_COMPLEX "Build optional heap: HOL-Complex" off
OPTIONS+= HOL_MATRIX "Build optional heap: HOL-Complex-Matrix" off
OPTIONS+= HOL_NOMINAL "Build optional heap: HOL-Nominal" 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+= HOLCF_IOA "Build optional heap: IOA" off
USE_PERL5= yes
BUILD_DEPENDS+= bash:${PORTSDIR}/shells/bash
RUN_DEPENDS+= proofgeneral:${PORTSDIR}/math/proofgeneral
RUN_DEPENDS+= bash:${PORTSDIR}/shells/bash
DOCFILES= Contents *.pdf *.eps *.ps *.dvi
.include <bsd.port.pre.mk>
.if defined(WITH_RLWRAP)
RUN_DEPENDS+= rlwrap:${PORTSDIR}/devel/rlwrap
LINE_EDIT= "${PREFIX}/bin/rlwrap"
.else
.if defined(WITH_LEDIT)
RUN_DEPENDS+= ledit:${PORTSDIR}/sysutils/ledit
LINE_EDIT= "${PREFIX}/bin/ledit"
.else
LINE_EDIT= ""
.endif
.endif
.if defined(WITH_HOL_ALGEBRA)
HEAP_HOL_ALGEBRA=""
.else
HEAP_HOL_ALGEBRA="@comment "
.endif
.if defined(WITH_HOL_COMPLEX)
HEAP_HOL_COMPLEX=""
.else
HEAP_HOL_COMPLEX="@comment "
.endif
.if defined(WITH_HOL_MATRIX)
HEAP_HOL_COMPLEX_MATRIX=""
.else
HEAP_HOL_COMPLEX_MATRIX="@comment "
.endif
.if defined(WITH_HOL_NOMINAL)
HEAP_HOL_NOMINAL=""
.else
HEAP_HOL_NOMINAL="@comment "
.endif
.if defined(WITH_HOL_WORD)
HEAP_HOL_WORD=""
.else
HEAP_HOL_WORD="@comment "
.endif
.if defined(WITH_HOL_TLA)
HEAP_HOL_TLA=""
.else
HEAP_HOL_TLA="@comment "
.endif
.if defined(WITH_HOL_HOL4)
HEAP_HOL_HOL4=""
.else
HEAP_HOL_HOL4="@comment "
.endif
.if defined(WITH_HOLCF_IOA)
HEAP_HOLCF_IOA=""
.else
HEAP_HOLCF_IOA="@comment "
.endif
.if defined(WITH_SMLNJ)
ML_SYSTEM= smlnj-110
ML_HOME= ${LOCALBASE}/bin
ML_OPTIONS= @SMLdebug=/dev/null
.else
ML_SYSTEM= polyml-5.1
ML_SYSTEM= polyml-5.2
ML_HOME= ${LOCALBASE}/bin
ML_OPTIONS= -H 500
ML_DBASE= ""
.endif
ML_PLATFORM= x86-bsd
PLIST_SUB= HEAPSUBDIR=${ML_SYSTEM}_${ML_PLATFORM}
PLIST_SUB= HEAPSUBDIR=${ML_SYSTEM}_${ML_PLATFORM} \
HEAP_HOL_ALGEBRA=${HEAP_HOL_ALGEBRA} \
HEAP_HOL_COMPLEX=${HEAP_HOL_COMPLEX} \
HEAP_HOL_COMPLEX_MATRIX=${HEAP_HOL_COMPLEX_MATRIX} \
HEAP_HOL_NOMINAL=${HEAP_HOL_NOMINAL} \
HEAP_HOL_WORD=${HEAP_HOL_WORD} \
HEAP_HOL_TLA=${HEAP_HOL_TLA} \
HEAP_HOL_HOL4=${HEAP_HOL_HOL4} \
HEAP_HOLCF_IOA=${HEAP_HOLCF_IOA}
.if defined(WITH_SMLNJ)
BUILD_DEPENDS+= smlnj-devel>=110.65:${PORTSDIR}/lang/sml-nj-devel
MAKE_ENV+= SMLNJ_DEVEL=yes
.else
BUILD_DEPENDS+= poly:${PORTSDIR}/lang/polyml
RUN_DEPENDS+= poly:${PORTSDIR}/lang/polyml
BUILD_DEPENDS+= polyml>=5.2:${PORTSDIR}/lang/polyml
RUN_DEPENDS+= polyml>=5.2:${PORTSDIR}/lang/polyml
.endif
NO_INSTALL_MANPAGES=yes
@ -64,13 +136,40 @@ post-patch:
s|%%ML_OPTIONS%%|\"${ML_OPTIONS}\"|; \
s|%%ML_DBASE%%|${ML_DBASE}|; \
s|%%ML_PLATFORM%%|${ML_PLATFORM}|; \
s|%%PREFIX%%|${PREFIX}|" \
s|%%PREFIX%%|${PREFIX}|; \
s|%%LINE_EDIT%%|${LINE_EDIT}|" \
${WRKSRC}/etc/settings.presed > ${WRKSRC}/etc/settings
@${RM} ${WRKSRC}/etc/settings.presed
@${TOUCH} ${WRKSRC}/contrib/.keep
@${REINPLACE_CMD} -e 's|%%SMLNJ_VERSION%%|SMLNJ_DEVEL=yes|' \
${WRKSRC}/lib/scripts/run-smlnj
post-build:
.if defined(WITH_HOL_ALGEBRA)
${WRKSRC}/build -b -m HOL-Algebra HOL
.endif
.if defined(WITH_HOL_COMPLEX)
${WRKSRC}/build -b -m HOL-Complex HOL
.endif
.if defined(WITH_HOL_MATRIX)
${WRKSRC}/build -b -m HOL-Complex-Matrix HOL
.endif
.if defined(WITH_HOL_NOMINAL)
${WRKSRC}/build -b -m HOL-Nominal HOL
.endif
.if defined(WITH_HOL_WORD)
${WRKSRC}/build -b -m HOL-Word HOL
.endif
.if defined(WITH_HOL_TLA)
${WRKSRC}/build -b -m TLA HOL
.endif
.if defined(WITH_HOL_HOL4)
${WRKSRC}/build -b -m HOL4 HOL
.endif
.if defined(WITH_HOLCF_IOA)
${WRKSRC}/build -b -m IOA HOLCF
.endif
post-install:
${WRKSRC}/bin/isatool ${INSTALL} -d ${PREFIX}/share/isabelle -p ${PREFIX}/bin
.if !defined(NOPORTDOCS)

18
math/isabelle/distinfo
View file

@ -1,9 +1,9 @@
MD5 (Isabelle2007.tar.gz) = 088e56b79a4c8cd3e4de7dad62a35827
SHA256 (Isabelle2007.tar.gz) = eb270bc44ddb8195c6b80eb80894555671119d12b7aa8d2aa31d1b2149604f26
SIZE (Isabelle2007.tar.gz) = 7577495
MD5 (Isabelle2007_library.tar.gz) = a257ee276275619832748c07cf0257b5
SHA256 (Isabelle2007_library.tar.gz) = b0f407e69d6406d0313c5d0c3a030267908e43b134532eb836fc6236ed440647
SIZE (Isabelle2007_library.tar.gz) = 37173555
MD5 (Isabelle2007_pdf.tar.gz) = b7b0f6965dc3e9f2a88c35d2f3c0cad7
SHA256 (Isabelle2007_pdf.tar.gz) = a9d34030f17d28420bdddecd661e2664c7db1171f278fdbf0f10c7daf3fded32
SIZE (Isabelle2007_pdf.tar.gz) = 6024675
MD5 (Isabelle2008.tar.gz) = 4ebd3288458b6a87979b211bf8fe3e15
SHA256 (Isabelle2008.tar.gz) = 27c963524992d88af57184a19ede96325bd8c117bd29d86664d25183dfffc140
SIZE (Isabelle2008.tar.gz) = 7932744
MD5 (Isabelle2008_library.tar.gz) = feff661e1b5e7279f3dedb9924e03973
SHA256 (Isabelle2008_library.tar.gz) = a5b6d8d22b004b14e94ef8fa16de272b669888a4847f512dbb7874b531612aba
SIZE (Isabelle2008_library.tar.gz) = 37598185
MD5 (Isabelle2008_pdf.tar.gz) = e52b6f445b06a4a0b7c90d703196c37d
SHA256 (Isabelle2008_pdf.tar.gz) = 71b98cb7ae0e5a2d9645e16d2f1f274cc5626ffade96d248ac48529329c79bf7
SIZE (Isabelle2008_pdf.tar.gz) = 5214045

8
math/isabelle/files/patch-bin-Isabelle
View file

@ -1,8 +0,0 @@
--- ./bin/Isabelle.orig Sun Sep 2 15:23:58 2007
+++ ./bin/Isabelle Sun Sep 2 16:05:40 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: Isabelle,v 1.30 2005/05/17 07:58:47 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen

8
math/isabelle/files/patch-bin-isabelle
View file

@ -1,8 +0,0 @@
--- ./bin/isabelle.orig Sun Sep 2 15:23:58 2007
+++ ./bin/isabelle Sun Sep 2 16:05:44 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: isabelle,v 1.46 2005/05/17 07:58:47 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen

23
math/isabelle/files/patch-bin-isabelle_interface
View file

@ -1,23 +0,0 @@
--- ./bin/isabelle-interface.orig Sun Sep 2 15:23:58 2007
+++ ./bin/isabelle-interface Sun Sep 2 16:05:48 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: isabelle-interface,v 1.8 2005/05/17 16:10:33 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -16,12 +16,12 @@
PRG="$(basename "$0")"
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
## diagnostics
-function fail()
+fail()
{
echo "$1" >&2
exit 2

32
math/isabelle/files/patch-bin-isabelle_process
View file

@ -1,32 +0,0 @@
--- bin/isabelle-process.orig Sat Jan 12 16:42:22 2008
+++ bin/isabelle-process Sat Jan 12 16:42:58 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: isabelle-process,v 1.17 2006/12/04 20:33:36 aspinall Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -16,12 +16,12 @@
PRG="$(basename "$0")"
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
## diagnostics
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
@@ -49,7 +49,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2

32
math/isabelle/files/patch-bin-isatool
View file

@ -1,32 +0,0 @@
--- ./bin/isatool.orig Sun Sep 2 15:23:58 2007
+++ ./bin/isatool Sun Sep 2 16:05:57 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: isatool,v 1.22 2005/05/17 07:58:47 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -16,12 +16,12 @@
PRG="$(basename "$0")"
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
## diagnostics
-function usage()
+usage()
{
echo
echo "Usage: $PRG TOOL [ARGS ...]"
@@ -49,7 +49,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2

32
math/isabelle/files/patch-build
View file

@ -1,32 +0,0 @@
--- build.orig Sat Jan 12 16:44:25 2008
+++ build Sat Jan 12 16:46:08 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: build,v 1.36 2005/12/01 17:41:46 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -23,12 +23,12 @@
PRG="$(basename "$0")"
ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)"
-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
## diagnostics
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
@@ -46,7 +46,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2

49
math/isabelle/files/patch-etc-settings
View file

@ -1,6 +1,6 @@
--- etc/settings.orig Sat Jan 12 16:47:09 2008
+++ etc/settings Sat Jan 12 16:56:24 2008
@@ -16,60 +16,27 @@
--- etc/settings.orig 2008-07-28 15:10:38.000000000 +1000
+++ etc/settings 2008-07-28 15:22:08.000000000 +1000
@@ -16,70 +16,36 @@
# not invent new ML system names unless you know what you are doing.
# Only one of the sections below should be activated.
@ -15,7 +15,7 @@
- "/opt/polyml/$ML_PLATFORM" \
- $POLY_HOME)
-ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
-ML_OPTIONS="-H 500"
-ML_OPTIONS="-H 200"
-ML_DBASE=""
-
-# Poly/ML 5.1
@ -69,7 +69,18 @@
#ML_OPTIONS="-noinit"
#ML_SUFFIX=".psv"
#ML_PLATFORM=""
@@ -155,7 +122,7 @@
-
###
### Interactive sessions (cf. isatool tty)
###
-ISABELLE_LINE_EDITOR=""
+ISABELLE_LINE_EDITOR="%%LINE_EDIT%%"
[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)"
@@ -154,7 +120,7 @@
###
# Where to look for docs (multiple dirs separated by ':').
@ -78,15 +89,29 @@
# Preferred document format
ISABELLE_DOC_FORMAT=pdf
@@ -190,6 +157,7 @@
@@ -189,6 +155,8 @@
# Proof General path, look in a variety of places
ISABELLE_INTERFACE=$(choosefrom \
+ "%%PREFIX%%/lib/xemacs/site-lisp/ProofGeneral/isar/interface" \
+ "%%PREFIX%%/bin/proofgeneral" \
"$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \
"$ISABELLE_HOME/../ProofGeneral/isar/interface" \
"/usr/local/ProofGeneral/isar/interface" \
@@ -223,26 +191,26 @@
@@ -211,9 +179,9 @@
## Set HOME only for tools you have installed!
# External provers
-E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "/usr/local/E" "")
-VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" "")
-SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "/usr/local/SPASS" "")
+E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "%%PREFIX%%/E" "")
+VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "%%PREFIX%%/Vampire" "")
+SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "%%PREFIX%%/SPASS" "")
# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
#HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
@@ -224,26 +192,26 @@
#SVC_MACHINE=sparc-sun-solaris
# Mucke (mu-calculus model checker)
@ -119,13 +144,3 @@
# For configuring HOL/Matrix/cplex
# LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
@@ -254,6 +222,6 @@
#GLPK_PATH=glpsol
# External provers
-E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "/usr/local/E" "")
-VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" "")
-SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "/usr/local/SPASS" "")
+E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "%%PREFIX%%/E" "")
+VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "%%PREFIX%%/Vampire" "")
+SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "%%PREFIX%%/SPASS" "")

26
math/isabelle/files/patch-lib-Tools-browser
View file

@ -1,26 +0,0 @@
--- lib/Tools/browser.orig Sat Jan 12 16:56:56 2008
+++ lib/Tools/browser Sat Jan 12 16:58:42 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: browser,v 1.17 2006/09/18 17:12:41 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -8,7 +8,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS] [GRAPHFILE]"
@@ -20,7 +20,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2

17
math/isabelle/files/patch-lib-Tools-codegen
View file

@ -1,17 +0,0 @@
--- lib/Tools/codegen.orig Sat Jan 12 17:19:17 2008
+++ lib/Tools/codegen Sat Jan 12 17:19:37 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: codegen,v 1.5 2007/11/21 13:18:23 haftmann Exp $
# Author: Florian Haftmann, TUM
@@ -10,7 +10,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG IMAGE THY SERI"

17
math/isabelle/files/patch-lib-Tools-convert
View file

@ -1,17 +0,0 @@
--- ./lib/Tools/convert.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/convert Sun Sep 2 15:48:00 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: convert,v 1.5 2005/04/26 17:50:57 wenzelm Exp $
# Author: David von Oheimb, TU Muenchen
@@ -10,7 +10,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [FILES|DIRS...]"

17
math/isabelle/files/patch-lib-Tools-dimacs2hol
View file

@ -1,17 +0,0 @@
--- ./lib/Tools/dimacs2hol.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/dimacs2hol Sun Sep 2 15:48:05 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: dimacs2hol,v 1.3 2005/04/26 17:50:57 wenzelm Exp $
# Author: Tjark Weber
@@ -11,7 +11,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG FILES"

26
math/isabelle/files/patch-lib-Tools-display
View file

@ -1,26 +0,0 @@
--- lib/Tools/display.orig Sat Jan 12 16:57:02 2008
+++ lib/Tools/display Sat Jan 12 17:00:11 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: display,v 1.10 2006/11/13 17:19:24 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -8,7 +8,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS] FILE"
@@ -21,7 +21,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2

26
math/isabelle/files/patch-lib-Tools-doc
View file

@ -1,26 +0,0 @@
--- ./lib/Tools/doc.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/doc Sun Sep 2 15:48:14 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: doc,v 1.13 2005/04/13 16:48:06 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -8,7 +8,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [DOC]"
@@ -18,7 +18,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2

44
math/isabelle/files/patch-lib-Tools-document
View file

@ -1,44 +0,0 @@
--- ./lib/Tools/document.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/document Sun Sep 2 15:48:20 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: document,v 1.22 2005/08/16 11:42:15 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -8,7 +8,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS] [DIR]"
@@ -25,7 +25,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2
@@ -88,7 +88,7 @@
# tagged region markup
-function prep_tags ()
+prep_tags ()
{
(
IFS=","
@@ -115,7 +115,7 @@
# prepare document
-function pre_latex ()
+pre_latex ()
{
local FMT="$1"
[ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log

17
math/isabelle/files/patch-lib-Tools-expandshort
View file

@ -1,17 +0,0 @@
--- ./lib/Tools/expandshort.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/expandshort Sun Sep 2 15:48:24 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: expandshort,v 1.15 2005/04/26 17:50:57 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -8,7 +8,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [FILES|DIRS...]"

17
math/isabelle/files/patch-lib-Tools-findlogics
View file

@ -1,17 +0,0 @@
--- lib/Tools/findlogics.orig Sat Jan 12 16:57:07 2008
+++ lib/Tools/findlogics Sat Jan 12 17:00:42 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: findlogics,v 1.9 2005/10/08 18:15:31 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -8,7 +8,7 @@
PRG=$(basename "$0")
-function usage()
+usage()
{
echo
echo "Usage: $PRG"

17
math/isabelle/files/patch-lib-Tools-fixcpure
View file

@ -1,17 +0,0 @@
--- ./lib/Tools/fixcpure.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/fixcpure Sun Sep 2 15:48:31 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: fixcpure,v 1.2 2005/04/26 17:50:57 wenzelm Exp $
# Author: Makarius
@@ -10,7 +10,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [FILES|DIRS...]"

17
math/isabelle/files/patch-lib-Tools-fixgreek
View file

@ -1,17 +0,0 @@
--- ./lib/Tools/fixgreek.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/fixgreek Sun Sep 2 15:48:35 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: fixgreek,v 1.4 2005/04/26 17:50:58 wenzelm Exp $
# Author: Sebastian Skalberg, TU Muenchen
@@ -10,7 +10,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [FILES|DIRS...]"

17
math/isabelle/files/patch-lib-Tools-fixheaders
View file

@ -1,17 +0,0 @@
--- ./lib/Tools/fixheaders.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/fixheaders Sun Sep 2 15:48:38 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: fixheaders,v 1.2 2005/07/06 08:34:07 wenzelm Exp $
# Author: Florian Haftmann, TUM
@@ -10,7 +10,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [FILES|DIRS...]"

17
math/isabelle/files/patch-lib-Tools-fixsome
View file

@ -1,17 +0,0 @@
--- ./lib/Tools/fixsome.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/fixsome Sun Sep 2 15:48:42 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: fixsome,v 1.7 2005/04/26 17:50:58 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -10,7 +10,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [FILES|DIRS...]"

17
math/isabelle/files/patch-lib-Tools-getenv
View file

@ -1,17 +0,0 @@
--- ./lib/Tools/getenv.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/getenv Sun Sep 2 15:48:46 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: getenv,v 1.11 2005/09/01 20:49:18 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -10,7 +10,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS] [VARNAMES ...]"

54
math/isabelle/files/patch-lib-Tools-install
View file

@ -1,54 +0,0 @@
--- ./lib/Tools/install.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/install Sun Sep 2 15:52:30 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: install,v 1.25 2005/07/01 12:41:57 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -8,7 +8,7 @@
PRG=$(basename "$0")
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS]"
@@ -24,7 +24,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2
@@ -71,18 +71,6 @@
# standalone binaries
-#set by configure
-AUTO_BASH=bash
-
-case "$AUTO_BASH" in
- /*)
- BASH="$AUTO_BASH"
- ;;
- *)
- BASH="/usr/bin/env bash"
- ;;
-esac
-
if [ -n "$BINDIR" ]; then
mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
@@ -92,7 +80,7 @@
DIST="$DISTDIR/bin/$NAME"
echo "installing $BIN"
rm -f "$BIN"
- echo "#!$BASH" > "$BIN" || fail "Cannot write file: $BIN"
+ echo "#!/bin/sh" > "$BIN" || fail "Cannot write file: $BIN"
echo >> "$BIN"
echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
chmod +x "$BIN"

17
math/isabelle/files/patch-lib-Tools-keywords
View file

@ -1,17 +0,0 @@
--- lib/Tools/keywords.orig Sat Jan 12 17:16:34 2008
+++ lib/Tools/keywords Sat Jan 12 17:17:21 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: keywords,v 1.3 2007/10/07 11:32:15 wenzelm Exp $
# Author: Makarius
@@ -10,7 +10,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS] [LOGS ...]"

65
math/isabelle/files/patch-lib-Tools-latex
View file

@ -1,65 +0,0 @@
--- ./lib/Tools/latex.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/latex Sun Sep 2 15:48:54 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: latex,v 1.27 2005/07/19 15:21:45 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -8,7 +8,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS] [FILE]"
@@ -23,7 +23,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2
@@ -67,7 +67,7 @@
FILEBASE=$(basename "$FILE" .tex)
[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
-function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
+check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
# operations
@@ -75,13 +75,13 @@
#set by configure
AUTO_PERL=perl
-function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
-function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
-function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
-function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
-function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
-function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
-function copy_styles ()
+run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
+run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
+run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
+run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
+run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
+run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
+copy_styles ()
{
for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
do
@@ -90,7 +90,7 @@
done
}
-function extract_syms ()
+extract_syms ()
{
"$AUTO_PERL" -n \
-e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \

26
math/isabelle/files/patch-lib-Tools-logo
View file

@ -1,26 +0,0 @@
--- ./lib/Tools/logo.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/logo Sun Sep 2 15:49:00 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: logo,v 1.10 2005/04/26 17:50:58 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -8,7 +8,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS] NAME"
@@ -22,7 +22,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2

17
math/isabelle/files/patch-lib-Tools-make
View file

@ -1,17 +0,0 @@
--- ./lib/Tools/make.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/make Sun Sep 2 15:49:08 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: make,v 1.9 2004/06/21 08:25:57 kleing Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -8,7 +8,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [ARGS ...]"

26
math/isabelle/files/patch-lib-Tools-makeall
View file

@ -1,26 +0,0 @@
--- lib/Tools/makeall.orig Sat Jan 12 16:57:16 2008
+++ lib/Tools/makeall Sat Jan 12 17:01:23 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: makeall,v 1.20 2005/12/01 17:41:46 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -14,7 +14,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [ARGS ...]"
@@ -24,7 +24,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2

26
math/isabelle/files/patch-lib-Tools-mkdir
View file

@ -1,26 +0,0 @@
--- lib/Tools/mkdir.orig Sat Jan 12 16:57:23 2008
+++ lib/Tools/mkdir Sat Jan 12 17:02:14 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: mkdir,v 1.45 2007/11/12 10:18:51 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -10,7 +10,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS] [LOGIC] NAME"
@@ -27,7 +27,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2

17
math/isabelle/files/patch-lib-Tools-mkproject
View file

@ -1,17 +0,0 @@
--- lib/Tools/mkproject.orig Sat Jan 12 17:18:15 2008
+++ lib/Tools/mkproject Sat Jan 12 17:18:41 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: mkproject,v 1.2 2007/08/09 17:19:23 wenzelm Exp $
# Author: David Aspinall and Makarius Wenzel
@@ -7,7 +7,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG NAME"

26
math/isabelle/files/patch-lib-Tools-print
View file

@ -1,26 +0,0 @@
--- ./lib/Tools/print.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/print Sun Sep 2 15:49:21 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: print,v 1.2 2004/06/29 09:21:18 kleing Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -8,7 +8,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS] FILE"
@@ -21,7 +21,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2

17
math/isabelle/files/patch-lib-Tools-unsymbolize
View file

@ -1,17 +0,0 @@
--- ./lib/Tools/unsymbolize.orig Sun Sep 2 15:11:55 2007
+++ ./lib/Tools/unsymbolize Sun Sep 2 15:49:24 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: unsymbolize,v 1.6 2005/04/26 17:50:58 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -10,7 +10,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [FILES|DIRS...]"

48
math/isabelle/files/patch-lib-Tools-usedir
View file

@ -1,48 +0,0 @@
--- lib/Tools/usedir.orig Sat Jan 12 16:57:29 2008
+++ lib/Tools/usedir Sat Jan 12 17:03:34 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: usedir,v 1.67 2007/10/30 09:52:26 haftmann Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -10,7 +10,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS] LOGIC NAME"
@@ -43,18 +43,18 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2
}
-function check_bool()
+check_bool()
{
[ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
}
-function check_number()
+check_number()
{
[ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
}
@@ -82,7 +82,7 @@
PROOFS=0
VERBOSE=false
-function getoptions()
+getoptions()
{
OPTIND=1
while getopts "C:D:M:P:T:V:bc:d:f:g:i:m:p:rs:v:" OPT

8
math/isabelle/files/patch-lib-Tools-version
View file

@ -1,8 +0,0 @@
--- lib/Tools/version.orig Sat Jan 12 16:57:34 2008
+++ lib/Tools/version Sat Jan 12 17:03:48 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: version,v 1.2 2004/06/21 08:25:57 kleing Exp $
# Author: Stefan Berghofer, TU Muenchen

15
math/isabelle/files/patch-lib-scripts-configure
View file

@ -1,15 +0,0 @@
--- lib/scripts/configure.orig Fri Sep 14 18:00:10 2007
+++ lib/scripts/configure Fri Sep 14 18:00:21 2007
@@ -8,11 +8,5 @@
## patch scripts
cd "`dirname "$0"`"
+exec sh lib/scripts/patch-scripts.bash
-if bash -c :
-then
- bash lib/scripts/patch-scripts.bash
-else
- echo "FATAL ERROR: bash not found!"
- exit 2
-fi

26
math/isabelle/files/patch-lib-scripts-feeder
View file

@ -1,26 +0,0 @@
--- ./lib/scripts/feeder.orig Sun Sep 2 15:12:50 2007
+++ ./lib/scripts/feeder Sun Sep 2 15:54:12 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: feeder,v 1.10 2005/04/26 17:50:58 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -11,7 +11,7 @@
PRG="$(basename "$0")"
DIR="$(dirname "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS]"
@@ -27,7 +27,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2

8
math/isabelle/files/patch-lib-scripts-fileindent
View file

@ -1,8 +0,0 @@
--- lib/scripts/fileident.orig Sat Jan 12 17:20:26 2008
+++ lib/scripts/fileident Sat Jan 12 17:20:38 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: fileident,v 1.1 2007/07/17 20:51:27 wenzelm Exp $
#

30
math/isabelle/files/patch-lib-scripts-getsettings
View file

@ -1,30 +0,0 @@
--- lib/scripts/getsettings.orig Sat Jan 12 17:08:58 2008
+++ lib/scripts/getsettings Sat Jan 12 17:10:17 2008
@@ -27,10 +27,9 @@
#users tend to put strange things in here ...
unset ENV
-unset BASH_ENV
#support easy settings
-function choosefrom ()
+choosefrom ()
{
local RESULT=""
local FILE=""
@@ -45,13 +44,13 @@
}
#get actual settings
-source "$ISABELLE_HOME/etc/settings" || exit 2
+. "$ISABELLE_HOME/etc/settings" || exit 2
ISABELLE_SITE_SETTINGS_PRESENT=true
[ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
{ echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; }
[ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \
- { source "$ISABELLE_HOME_USER/etc/settings" || exit 2; }
+ { . "$ISABELLE_HOME_USER/etc/settings" || exit 2; }
#ML system identifier
if [ -z "$ML_PLATFORM" ]; then

37
math/isabelle/files/patch-lib-scripts-patch_scripts.bash
View file

@ -1,37 +0,0 @@
--- lib/scripts/patch-scripts.bash.orig Sun Sep 2 15:55:18 2007
+++ lib/scripts/patch-scripts.bash Sun Sep 2 16:06:41 2007
@@ -3,12 +3,12 @@
# Author: Markus Wenzel, TU Muenchen
#
# patch-scripts.bash - relocate interpreter paths of executable scripts and
-# insert AUTO_BASH/AUTO_PERL values
+# insert AUTO_PERL values
#
## find binaries
-function findbin()
+findbin()
{
local BASE="$1"
local BINARY=""
@@ -29,17 +29,14 @@
## main
-[ -z "$BASH_PATH" ] && BASH_PATH=$(findbin bash)
[ -z "$PERL_PATH" ] && PERL_PATH=$(findbin perl)
-[ -z "$AUTO_BASH" ] && AUTO_BASH="$BASH_PATH"
[ -z "$AUTO_PERL" ] && AUTO_PERL="$PERL_PATH"
for FILE in $(find . -type f -print)
do
if [ -x "$FILE" ]; then
- sed -e "s:^#!.*/bash:#!$BASH_PATH:" -e "s:^#!.*/perl:#!$PERL_PATH:" \
- -e "s:^AUTO_BASH=.*bash:AUTO_BASH=$AUTO_BASH:" \
- -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" "$FILE" > "$FILE~~"
+ sed -e "s:^#!.*/perl:#!$PERL_PATH:" \
+ -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" "$FILE" > "$FILE~~"
if cmp -s "$FILE" "$FILE~~"; then
rm "$FILE~~"
else

8
math/isabelle/files/patch-lib-scripts-polyml_platform
View file

@ -1,8 +0,0 @@
--- lib/scripts/polyml-platform.orig Sat Jan 12 17:09:07 2008
+++ lib/scripts/polyml-platform Sat Jan 12 17:11:51 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: polyml-platform,v 1.6 2007/11/08 19:07:58 wenzelm Exp $
#

8
math/isabelle/files/patch-lib-scripts-polyml_version
View file

@ -1,8 +0,0 @@
--- lib/scripts/polyml-version.orig Sat Jan 12 17:09:13 2008
+++ lib/scripts/polyml-version Sat Jan 12 17:15:41 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: polyml-version,v 1.5 2006/12/05 17:32:54 wenzelm Exp $
#

35
math/isabelle/files/patch-lib-scripts-run_mosml
View file

@ -1,35 +0,0 @@
--- lib/scripts/run-mosml.orig Mon Jun 21 18:25:58 2004
+++ lib/scripts/run-mosml Sun Sep 2 17:14:13 2007
@@ -1,16 +1,14 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: run-mosml,v 1.8 2004/06/21 08:25:58 kleing Exp $
# Author: Markus Wenzel, TU Muenchen
#
# Moscow ML 2.00 startup script
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
-
## diagnostics
-function fail_out()
+fail_out()
{
echo "Unable to create output heap file: \"$OUTFILE\"" >&2
exit 2
@@ -37,6 +35,13 @@
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
fi
+SAVE_OUTFILE="$OUTFILE"
+SAVE_MLTEXT="$MLTEXT"
+SAVE_NOWRITE="$NOWRITE"
+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+OUTFILE="$SAVE_OUTFILE"
+MLTEXT="$SAVE_MLTEXT"
+NOWRITE="$SAVE_NOWRITE"
## run it!

45
math/isabelle/files/patch-lib-scripts-run_polyml
View file

@ -1,45 +0,0 @@
--- lib/scripts/run-polyml.orig Sun Oct 21 04:31:50 2007
+++ lib/scripts/run-polyml Sat Jan 12 18:01:17 2008
@@ -5,18 +5,15 @@
#
# Poly/ML startup script.
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
-
-
## diagnostics
-function fail_out()
+fail_out()
{
echo "Unable to create output heap file: \"$OUTFILE\"" >&2
exit 2
}
-function check_file()
+check_file()
{
if [ ! -f "$1" ]; then
echo "Unable to locate $1" >&2
@@ -25,6 +22,21 @@
fi
}
+SAVE_INFILE="$INFILE"
+SAVE_OUTFILE="$OUTFILE"
+SAVE_COPYDB="$COPYDB"
+SAVE_COMPRESS="$COMPRESS"
+SAVE_MLTEXT="$MLTEXT"
+SAVE_TERMINATE="$TERMINATE"
+SAVE_NOWRITE="$NOWRITE"
+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+INFILE="$SAVE_INFILE"
+OUTFILE="$SAVE_OUTFILE"
+COPYDB="$SAVE_COPYDB"
+COMPRESS="$SAVE_COMPRESS"
+MLTEXT="$SAVE_MLTEXT"
+TERMINATE="$SAVE_TERMINATE"
+NOWRITE="$SAVE_NOWRITE"
## Poly/ML executable and database

50
math/isabelle/files/patch-lib-scripts-run_polyml_5.0
View file

@ -1,50 +0,0 @@
--- lib/scripts/run-polyml-5.0.orig Sun Oct 21 04:32:23 2007
+++ lib/scripts/run-polyml-5.0 Sat Jan 12 18:01:28 2008
@@ -1,22 +1,20 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: run-polyml-5.0,v 1.9 2007/10/20 18:32:23 wenzelm Exp $
# Author: Makarius
#
# Poly/ML startup script (for 5.0)
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
-
## diagnostics
-function fail_out()
+fail_out()
{
echo "Unable to create output heap file: \"$OUTFILE\"" >&2
exit 2
}
-function check_file()
+check_file()
{
if [ ! -f "$1" ]; then
echo "Unable to locate $1" >&2
@@ -25,6 +23,21 @@
fi
}
+SAVE_INFILE="$INFILE"
+SAVE_OUTFILE="$OUTFILE"
+SAVE_COPYDB="$COPYDB"
+SAVE_COMPRESS="$COMPRESS"
+SAVE_MLTEXT="$MLTEXT"
+SAVE_TERMINATE="$TERMINATE"
+SAVE_NOWRITE="$NOWRITE"
+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+INFILE="$SAVE_INFILE"
+OUTFILE="$SAVE_OUTFILE"
+COPYDB="$SAVE_COPYDB"
+COMPRESS="$SAVE_COMPRESS"
+MLTEXT="$SAVE_MLTEXT"
+TERMINATE="$SAVE_TERMINATE"
+NOWRITE="$SAVE_NOWRITE"
## compiler executables and libraries

50
math/isabelle/files/patch-lib-scripts-run_polyml_5.1
View file

@ -1,50 +0,0 @@
--- lib/scripts/run-polyml-5.1.orig Tue Nov 20 21:42:15 2007
+++ lib/scripts/run-polyml-5.1 Sat Jan 12 18:01:39 2008
@@ -1,22 +1,20 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: run-polyml-5.1,v 1.7 2007/11/20 10:42:15 wenzelm Exp $
# Author: Makarius
#
# Poly/ML startup script (for 5.1)
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
-
## diagnostics
-function fail_out()
+fail_out()
{
echo "Unable to create output heap file: \"$OUTFILE\"" >&2
exit 2
}
-function check_file()
+check_file()
{
if [ ! -f "$1" ]; then
echo "Unable to locate $1" >&2
@@ -25,6 +23,21 @@
fi
}
+SAVE_INFILE="$INFILE"
+SAVE_OUTFILE="$OUTFILE"
+SAVE_COPYDB="$COPYDB"
+SAVE_COMPRESS="$COMPRESS"
+SAVE_MLTEXT="$MLTEXT"
+SAVE_TERMINATE="$TERMINATE"
+SAVE_NOWRITE="$NOWRITE"
+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+INFILE="$SAVE_INFILE"
+OUTFILE="$SAVE_OUTFILE"
+COPYDB="$SAVE_COPYDB"
+COMPRESS="$SAVE_COMPRESS"
+MLTEXT="$SAVE_MLTEXT"
+TERMINATE="$SAVE_TERMINATE"
+NOWRITE="$SAVE_NOWRITE"
## compiler executables and libraries

59
math/isabelle/files/patch-lib-scripts-run_poplogml
View file

@ -1,59 +0,0 @@
--- lib/scripts/run-poplogml.orig Tue Oct 11 21:28:04 2005
+++ lib/scripts/run-poplogml Sat Jan 12 18:01:54 2008
@@ -1,22 +1,20 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: run-poplogml,v 1.5 2005/10/11 11:28:04 wenzelm Exp $
# Author: Makarius
#
# Poplog/PML startup script (version 15.6/2.1).
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
-
## diagnostics
-function fail_out()
+fail_out()
{
echo "Unable to create output heap file: \"$OUTFILE\"" >&2
exit 2
}
-function check_mlhome_file()
+check_mlhome_file()
{
if [ ! -f "$1" ]; then
echo "Unable to locate $1" >&2
@@ -25,7 +23,7 @@
fi
}
-function check_heap_file()
+check_heap_file()
{
if [ ! -f "$1" ]; then
echo "Expected to find ML heap file $1" >&2
@@ -35,6 +33,21 @@
fi
}
+SAVE_INFILE="$INFILE"
+SAVE_OUTFILE="$OUTFILE"
+SAVE_COPYDB="$COPYDB"
+SAVE_COMPRESS="$COMPRESS"
+SAVE_MLTEXT="$MLTEXT"
+SAVE_TERMINATE="$TERMINATE"
+SAVE_NOWRITE="$NOWRITE"
+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+INFILE="$SAVE_INFILE"
+OUTFILE="$SAVE_OUTFILE"
+COPYDB="$SAVE_COPYDB"
+COMPRESS="$SAVE_COMPRESS"
+MLTEXT="$SAVE_MLTEXT"
+TERMINATE="$SAVE_TERMINATE"
+NOWRITE="$SAVE_NOWRITE"
## prepare databases

58
math/isabelle/files/patch-lib-scripts-run_smlnj
View file

@ -1,43 +1,10 @@
--- lib/scripts/run-smlnj.orig Mon Jun 21 18:25:58 2004
+++ lib/scripts/run-smlnj Fri Sep 14 18:01:25 2007
@@ -1,22 +1,20 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: run-smlnj,v 1.28 2004/06/21 08:25:58 kleing Exp $
# Author: Markus Wenzel, TU Muenchen
#
# SML/NJ startup script (for 110 or later).
--- lib/scripts/run-smlnj.orig 2004-06-21 18:25:58.000000000 +1000
+++ lib/scripts/run-smlnj 2008-07-29 15:49:30.000000000 +1000
@@ -39,11 +39,10 @@
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
-
## diagnostics
-function fail_out()
+fail_out()
{
echo "Unable to create output heap file: \"$OUTFILE\"" >&2
exit 2
}
-function check_mlhome_file()
+check_mlhome_file()
{
if [ ! -f "$1" ]; then
echo "Unable to locate $1" >&2
@@ -25,7 +23,7 @@
fi
}
-function check_heap_file()
+check_heap_file()
{
if [ ! -f "$1" ]; then
echo "Expected to find ML heap file $1" >&2
@@ -40,10 +38,8 @@
## compiler binaries
+export SMLNJ_DEVEL=yes
SML="$ML_HOME/sml"
-ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
@ -46,22 +13,7 @@
@@ -76,6 +72,14 @@
FEEDER_OPTS="-q"
fi
+SAVE_OUTFILE="$OUTFILE"
+SAVE_MLTEXT="$MLTEXT"
+SAVE_NOWRITE="$NOWRITE"
+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+OUTFILE="$SAVE_OUTFILE"
+MLTEXT="$SAVE_MLTEXT"
+NOWRITE="$SAVE_NOWRITE"
+
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
{ read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
RC="$?"
@@ -84,8 +88,7 @@
@@ -84,8 +83,7 @@
## fix heap file name and permissions
if [ -n "$OUTFILE" ]; then

16
math/isabelle/files/patch-lib-scripts-timestart.bash
View file

@ -1,16 +0,0 @@
--- lib/scripts/timestart.bash.orig Thu Dec 8 01:23:22 2005
+++ lib/scripts/timestart.bash Sat Jan 12 17:53:32 2008
@@ -10,9 +10,11 @@
#set by configure
AUTO_PERL=perl
-function get_times () {
- local TMP="/tmp/get_times$$"
+get_times () {
+ local TMP SECONDS
+ TMP="/tmp/get_times$$"
times > "$TMP" # No pipe here!
+ SECONDS=$(( `date +'%j * 86400 + %H * 3600 + %M * 60 + %S'` ))
TIMES_RESULT="$SECONDS $(echo $(cat "$TMP") | "$AUTO_PERL" -pe 's,\d+m\d+\.\d+s \d+m\d+\.\d+s (\d+)m(\d+)\.\d+s +(\d+)m(\d+)\.\d+s, $1 * 60 + $2 + $3 * 60 + $4,e')"
rm -f "$TMP"
}

44
math/isabelle/files/patch-lib-scripts-timestop.bash
View file

@ -1,44 +0,0 @@
--- lib/scripts/timestop.bash.orig Fri Dec 2 04:44:47 2005
+++ lib/scripts/timestop.bash Sat Jan 12 17:54:13 2008
@@ -7,28 +7,29 @@
TIMES_REPORT=""
-function show_times ()
+show_times ()
{
- local TIMES_START="$TIMES_RESULT"
+ local TIMES_START TIMES_STOP KIND START STOP TIME SECS MINUTES HOURS \
+ KIND_NAME RESULT
+
+ TIMES_START="$TIMES_RESULT"
get_times
- local TIMES_STOP="$TIMES_RESULT"
- local KIND
+ TIMES_STOP="$TIMES_RESULT"
for KIND in 1 2
do
- local START=$(echo "$TIMES_START" | cut -d " " -f $KIND)
- local STOP=$(echo "$TIMES_STOP" | cut -d " " -f $KIND)
+ START=$(echo "$TIMES_START" | cut -d " " -f $KIND)
+ STOP=$(echo "$TIMES_STOP" | cut -d " " -f $KIND)
- local TIME=$[ $STOP - $START ]
- local SECS=$[ $TIME % 60 ]
+ TIME=$(( $STOP - $START ))
+ SECS=$(( $TIME % 60 ))
[ $SECS -lt 10 ] && SECS="0$SECS"
- local MINUTES=$[ ($TIME / 60) % 60 ]
+ MINUTES=$(( ($TIME / 60) % 60 ))
[ $MINUTES -lt 10 ] && MINUTES="0$MINUTES"
- local HOURS=$[ $TIME / 3600 ]
+ HOURS=$(( $TIME / 3600 ))
- local KIND_NAME
[ "$KIND" = 1 ] && KIND_NAME="elapsed time"
[ "$KIND" = 2 ] && KIND_NAME="cpu time"
- local RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}"
+ RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}"
if [ -z "$TIMES_REPORT" ]; then
TIMES_REPORT="$RESULT"

26
math/isabelle/files/patch-src-Pure-mk
View file

@ -1,26 +0,0 @@
--- src/Pure/mk.orig Sat Jan 12 17:35:00 2008
+++ src/Pure/mk Sat Jan 12 17:36:05 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: mk,v 1.32 2007/01/04 20:58:46 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -10,7 +10,7 @@
## diagnostics
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS]"
@@ -23,7 +23,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2

494
math/isabelle/pkg-plist
View file

File diff suppressed because it is too large Load diff