0002baf188
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>
146 lines
4.6 KiB
Text
146 lines
4.6 KiB
Text
--- 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.
|
|
|
|
-# Poly/ML 4.x/5.x (automated settings)
|
|
-POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")"
|
|
-ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform")
|
|
-ML_HOME=$(choosefrom \
|
|
- "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
|
|
- "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
|
|
- "/usr/local/polyml/$ML_PLATFORM" \
|
|
- "/usr/share/polyml/$ML_PLATFORM" \
|
|
- "/opt/polyml/$ML_PLATFORM" \
|
|
- $POLY_HOME)
|
|
-ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
|
|
-ML_OPTIONS="-H 200"
|
|
-ML_DBASE=""
|
|
-
|
|
-# Poly/ML 5.1
|
|
-#ML_PLATFORM=x86-linux
|
|
-#ML_HOME=/usr/local/polyml/x86-linux
|
|
-#ML_SYSTEM=polyml-5.1
|
|
-#ML_OPTIONS="-H 500"
|
|
-
|
|
-# Poly/ML 5.1 (64 bit)
|
|
-#ML_PLATFORM=x86_64-linux
|
|
-#ML_HOME=/usr/local/polyml/x86_64-linux
|
|
-#ML_SYSTEM=polyml-5.1
|
|
-#ML_OPTIONS="-H 1000"
|
|
-
|
|
-# Poly/ML 4.2.0
|
|
-#ML_PLATFORM=x86-linux
|
|
-#ML_HOME=/usr/local/polyml/x86-linux
|
|
-#ML_SYSTEM=polyml-4.2.0
|
|
-#ML_OPTIONS="-H 80"
|
|
-
|
|
-# Standard ML of New Jersey (slow!)
|
|
-#ML_SYSTEM=smlnj-110
|
|
-#ML_HOME="/usr/local/smlnj/bin"
|
|
-#ML_OPTIONS="@SMLdebug=/dev/null"
|
|
-#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
|
|
-#SMLNJ_CYGWIN_RUNTIME=1
|
|
+ML_SYSTEM=%%ML_SYSTEM%%
|
|
+ML_HOME=%%ML_HOME%%
|
|
+ML_OPTIONS=%%ML_OPTIONS%%
|
|
+ML_PLATFORM=%%ML_PLATFORM%%
|
|
+ML_DBASE=%%ML_DBASE%%
|
|
|
|
# Moscow ML 2.00 (experimental!)
|
|
#ML_SYSTEM=mosml
|
|
-#ML_HOME="/usr/local/mosml/bin"
|
|
+#ML_HOME="%%PREFIX%%/bin"
|
|
#ML_OPTIONS=""
|
|
#ML_PLATFORM=""
|
|
|
|
# Alice 1.4 (experimental!)
|
|
#ML_SYSTEM=alice
|
|
-#ML_HOME="/usr/local/alice/bin"
|
|
+#ML_HOME="%%PREFIX%%/bin"
|
|
#ML_OPTIONS=""
|
|
#ML_PLATFORM=""
|
|
|
|
# Poplog/PML version 15.6/2.1 (experimental!)
|
|
#ML_SYSTEM=poplogml
|
|
-#ML_HOME="/usr/local/poplog/current-poplog/bin"
|
|
+#ML_HOME="%%PREFIX%%/bin"
|
|
#ML_OPTIONS="-noinit"
|
|
#ML_SUFFIX=".psv"
|
|
#ML_PLATFORM=""
|
|
|
|
-
|
|
###
|
|
### 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 ':').
|
|
-ISABELLE_DOCS="$ISABELLE_HOME/doc"
|
|
+ISABELLE_DOCS="%%PREFIX%%/share/doc/isabelle"
|
|
|
|
# Preferred document format
|
|
ISABELLE_DOC_FORMAT=pdf
|
|
@@ -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" \
|
|
@@ -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)
|
|
-#MUCKE_HOME=/usr/local/bin
|
|
+#MUCKE_HOME=%%PREFIX%%/bin
|
|
|
|
# Einhoven model checker
|
|
-#EINDHOVEN_HOME=/usr/local/bin
|
|
+#EINDHOVEN_HOME=%%PREFIX%%/bin
|
|
|
|
# MiniSat 1.14 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
|
|
-#MINISAT_HOME=/usr/local/bin
|
|
+#MINISAT_HOME=%%PREFIX%%/bin
|
|
|
|
# zChaff (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
|
|
-#ZCHAFF_HOME=/usr/local/bin
|
|
+#ZCHAFF_HOME=%%PREFIX%%/bin
|
|
#ZCHAFF_VERSION=2004.5.13
|
|
#ZCHAFF_VERSION=2004.11.15
|
|
|
|
# BerkMin561 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
|
|
-#BERKMIN_HOME=/usr/local/bin
|
|
+#BERKMIN_HOME=%%PREFIX%%/bin
|
|
#BERKMIN_EXE=BerkMin561-linux
|
|
#BERKMIN_EXE=BerkMin561-solaris
|
|
|
|
# Jerusat 1.3 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
|
|
-#JERUSAT_HOME=/usr/local/bin
|
|
+#JERUSAT_HOME=%%PREFIX%%/bin
|
|
|
|
# For configuring HOL/Matrix/cplex
|
|
# LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
|