updated "op +", "op -", "op *". "HOL.divide" in src & test
find . -type f -exec sed -i s/"\"op +\""/"\"Groups.plus_class.plus\""/g {} \;
find . -type f -exec sed -i s/"\"op -\""/"\"Groups.minus_class.minus\""/g {} \;
find . -type f -exec sed -i s/"\"op *\""/"\"Groups.times_class.times\""/g {} \;
find . -type f -exec sed -i s/"\"HOL.divide\""/"\"Rings.inverse_class.divide\""/g {} \;
3 # makebin -- make Isabelle logic images for current platform
8 TMP="/var/tmp/isabelle-makebin$$"
10 export THIS_IS_ISABELLE_MAKEBIN=true
20 echo "Usage: $PRG [OPTIONS] ARCHIVE"
23 echo " -l produce library"
25 echo " Precompile Isabelle for the current platform."
37 ## process command line
43 while getopts "ln" OPT
55 shift $(($OPTIND - 1))
60 [ "$#" -gt 1 ] && usage
67 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
68 ARCHIVE_BASE="$(basename "$ARCHIVE")"
69 ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
70 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
72 ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"
73 ISABELLE_HOME="$TMP/$ISABELLE_NAME"
78 mkdir "$TMP" || fail "Cannot create directory $TMP"
81 tar xzf "$ARCHIVE_FULL"
85 -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \
88 if [ -n "$DO_LIBRARY" ]; then
89 perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -V outline=/proof,/ML":;' \
93 ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
94 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
95 echo "### WARNING! Personal Isabelle settings present. " >&2
97 COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
98 PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
100 if [ -n "$DO_LIBRARY" ]; then
103 ./build -b -m HOL-Nominal HOL
114 chgrp -R isabelle "$TMP"
116 if [ -n "$DO_LIBRARY" ]; then
117 tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
119 tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps"