--- a/bin/isabelle Tue May 06 15:24:41 1997 +0200
+++ b/bin/isabelle Tue May 06 15:27:35 1997 +0200
@@ -148,8 +148,8 @@
OUTFILE="$OUTPUT"
;;
*)
- mkdir -p "$ISABELLE_OUTPUT_DIR"
- OUTFILE="$ISABELLE_OUTPUT_DIR/$OUTPUT"
+ mkdir -p "$ISABELLE_OUTPUT"
+ OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
;;
esac
--- a/etc/settings Tue May 06 15:24:41 1997 +0200
+++ b/etc/settings Tue May 06 15:27:35 1997 +0200
@@ -56,16 +56,17 @@
ISABELLE_TOOLS=$ISABELLE_HOME/lib/Tools
-# Heap file locations.
+# Heap file locations. ML system identifier appended automatically!
-ISABELLE_PATH=$ISABELLE_HOME_USER/heaps/$ML_SYSTEM:$ISABELLE_HOME/heaps/$ML_SYSTEM
+ISABELLE_PATH=$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps
if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then
- ISABELLE_OUTPUT_DIR=$ISABELLE_HOME/heaps/$ML_SYSTEM
+ ISABELLE_OUTPUT=$ISABELLE_HOME/heaps
else
- ISABELLE_OUTPUT_DIR=$ISABELLE_HOME_USER/heaps/$ML_SYSTEM
+ ISABELLE_OUTPUT=$ISABELLE_HOME_USER/heaps
fi
+
DEFAULT_LOGIC=HOL
--- a/etc/user-settings.sample Tue May 06 15:24:41 1997 +0200
+++ b/etc/user-settings.sample Tue May 06 15:27:35 1997 +0200
@@ -15,7 +15,10 @@
### Heap files
###
+# Note: ML system identifier appended automatically!
+
#ISABELLE_PATH=other-places-where-heaps-may-reside:$ISABELLE_PATH
+#ISABELLE_OUTPUT=somewhere-else
#DEFAULT_LOGIC=ZF
--- a/lib/Tools/makeall Tue May 06 15:24:41 1997 +0200
+++ b/lib/Tools/makeall Tue May 06 15:27:35 1997 +0200
@@ -47,7 +47,7 @@
echo Started at `date`
echo Source=`pwd`
-echo Destination=$ISABELLE_OUTPUT_DIR
+echo Destination=$ISABELLE_OUTPUT
echo force=$FORCE ' ' clean=$CLEAN ' '
echo Compiler=$ML_SYSTEM
echo Running on `hostname`
@@ -57,10 +57,10 @@
echo ' **** Consider the -notest switch ****'
esac
-mkdir -p $ISABELLE_OUTPUT_DIR
+mkdir -p $ISABELLE_OUTPUT
case $FORCE.$EXEC in
- on.on) (cd $ISABELLE_OUTPUT_DIR;
+ on.on) (cd $ISABELLE_OUTPUT;
for f in Pure FOL ZF CCL LCF CTT Sequents HOL HOLCF Cube FOLP
do
rm -f $f
@@ -91,7 +91,7 @@
tail ZF/make$$.log
gzip ZF/make$$.log
case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT_DIR/ZF
+ on.on) rm -f $ISABELLE_OUTPUT/ZF
esac
echo
@@ -101,7 +101,7 @@
tail CCL/make$$.log
gzip CCL/make$$.log
case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT_DIR/CCL
+ on.on) rm -f $ISABELLE_OUTPUT/CCL
esac
echo
@@ -111,7 +111,7 @@
tail LCF/make$$.log
gzip LCF/make$$.log
case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT_DIR/FOL $ISABELLE_OUTPUT_DIR/LCF
+ on.on) rm -f $ISABELLE_OUTPUT/FOL $ISABELLE_OUTPUT/LCF
esac
echo
@@ -121,7 +121,7 @@
tail CTT/make$$.log
gzip CTT/make$$.log
case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT_DIR/CTT
+ on.on) rm -f $ISABELLE_OUTPUT/CTT
esac
echo
@@ -131,7 +131,7 @@
tail Sequents/make$$.log
gzip Sequents/make$$.log
case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT_DIR/Sequents
+ on.on) rm -f $ISABELLE_OUTPUT/Sequents
esac
echo
@@ -149,7 +149,7 @@
tail HOLCF/make$$.log
gzip HOLCF/make$$.log
case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT_DIR/HOL $ISABELLE_OUTPUT_DIR/HOLCF
+ on.on) rm -f $ISABELLE_OUTPUT/HOL $ISABELLE_OUTPUT/HOLCF
esac
echo
@@ -157,7 +157,7 @@
echo '*****The Lambda-Cube (Cube)*****'
(cd Cube; $ISATOOL make $NO $TEST > make$$.log)
case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT_DIR/Cube
+ on.on) rm -f $ISABELLE_OUTPUT/Cube
esac
tail Cube/make$$.log
gzip Cube/make$$.log
@@ -167,7 +167,7 @@
echo '*****First-Order Logic with Proof Terms (FOLP)*****'
(cd FOLP; $ISATOOL make $NO $TEST > make$$.log)
case $CLEAN.$EXEC in
- on.on) rm -f $ISABELLE_OUTPUT_DIR/FOLP
+ on.on) rm -f $ISABELLE_OUTPUT/FOLP
esac
tail FOLP/make$$.log
gzip FOLP/make$$.log
--- a/lib/scripts/getsettings Tue May 06 15:24:41 1997 +0200
+++ b/lib/scripts/getsettings Tue May 06 15:27:35 1997 +0200
@@ -23,4 +23,9 @@
ISABELLE=$ISABELLE_HOME/bin/isabelle
ISATOOL=$ISABELLE_HOME/bin/isatool
+#append ML system to paths
+ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_SYSTEM"
+ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_SYSTEM; done)
+ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :)
+
set +o allexport
--- a/src/CCL/IsaMakefile Tue May 06 15:24:41 1997 +0200
+++ b/src/CCL/IsaMakefile Tue May 06 15:27:35 1997 +0200
@@ -4,7 +4,7 @@
# IsaMakefile for CCL
#
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
SET_FILES = ROOT.ML Set.thy Set.ML subset.ML equalities.ML mono.ML \
Gfp.thy Gfp.ML Lfp.thy Lfp.ML
--- a/src/CTT/IsaMakefile Tue May 06 15:24:41 1997 +0200
+++ b/src/CTT/IsaMakefile Tue May 06 15:27:35 1997 +0200
@@ -4,7 +4,7 @@
# IsaMakefile for CTT
#
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
FILES = ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \
Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML
--- a/src/Cube/IsaMakefile Tue May 06 15:24:41 1997 +0200
+++ b/src/Cube/IsaMakefile Tue May 06 15:27:35 1997 +0200
@@ -4,7 +4,7 @@
# IsaMakefile for Cube
#
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
FILES = ROOT.ML Cube.thy Cube.ML
$(OUT)/Cube: $(OUT)/Pure $(FILES)
--- a/src/FOL/IsaMakefile Tue May 06 15:24:41 1997 +0200
+++ b/src/FOL/IsaMakefile Tue May 06 15:27:35 1997 +0200
@@ -4,7 +4,7 @@
# IsaMakefile for FOL
#
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
FILES = ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
thy_data.ML cladata.ML \
--- a/src/FOLP/IsaMakefile Tue May 06 15:24:41 1997 +0200
+++ b/src/FOLP/IsaMakefile Tue May 06 15:27:35 1997 +0200
@@ -4,7 +4,7 @@
# IsaMakefile for FOLP
#
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
FILES = ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML \
hypsubst.ML classical.ML simp.ML
--- a/src/HOL/IsaMakefile Tue May 06 15:24:41 1997 +0200
+++ b/src/HOL/IsaMakefile Tue May 06 15:27:35 1997 +0200
@@ -6,7 +6,7 @@
#### Base system
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
--- a/src/HOLCF/IsaMakefile Tue May 06 15:24:41 1997 +0200
+++ b/src/HOLCF/IsaMakefile Tue May 06 15:27:35 1997 +0200
@@ -6,7 +6,7 @@
#### Base system
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
THYS = Porder.thy Porder0.thy Pcpo.thy \
Fun1.thy Fun2.thy Fun3.thy \
--- a/src/LCF/IsaMakefile Tue May 06 15:24:41 1997 +0200
+++ b/src/LCF/IsaMakefile Tue May 06 15:27:35 1997 +0200
@@ -4,7 +4,7 @@
# IsaMakefile for LCF
#
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
FILES = ROOT.ML LCF.thy LCF.ML simpdata.ML pair.ML fix.ML
$(OUT)/LCF: $(OUT)/FOL $(FILES)
--- a/src/Pure/IsaMakefile Tue May 06 15:24:41 1997 +0200
+++ b/src/Pure/IsaMakefile Tue May 06 15:27:35 1997 +0200
@@ -7,7 +7,7 @@
# are loaded on top of it.
#
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
FILES = ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML \
ML-Systems/smlnj-1.07.ML ML-Systems/smlnj-1.09.ML ROOT.ML \
--- a/src/Pure/mk Tue May 06 15:24:41 1997 +0200
+++ b/src/Pure/mk Tue May 06 15:27:35 1997 +0200
@@ -32,4 +32,4 @@
-e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
-q RAW_ML_SYSTEM Pure
-chmod -w $ISABELLE_OUTPUT_DIR/Pure
+chmod -w $ISABELLE_OUTPUT/Pure
--- a/src/Sequents/IsaMakefile Tue May 06 15:24:41 1997 +0200
+++ b/src/Sequents/IsaMakefile Tue May 06 15:27:35 1997 +0200
@@ -4,7 +4,7 @@
# IsaMakefile for Sequents
#
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
NAMES = ILL LK S4 S43 T
FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML)
--- a/src/ZF/IsaMakefile Tue May 06 15:24:41 1997 +0200
+++ b/src/ZF/IsaMakefile Tue May 06 15:27:35 1997 +0200
@@ -6,7 +6,7 @@
#### Base system
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
NAMES = ZF upair subset pair domrange \
func AC equalities Bool \