1.1 --- a/Admin/MacOS/App1/README Mon Jul 23 18:52:10 2012 +0200
1.2 +++ b/Admin/MacOS/App1/README Mon Jul 23 19:07:01 2012 +0200
1.3 @@ -5,5 +5,6 @@
1.4
1.5 * CocoaDialog 2.1.1 http://cocoadialog.sourceforge.net/
1.6
1.7 -* Platypus 4.0 http://www.sveinbjorn.org/platypus
1.8 +* Platypus 4.7 http://www.sveinbjorn.org/platypus
1.9 + Preferences: Install command line tool
1.10
2.1 --- a/Admin/MacOS/App1/mk Mon Jul 23 18:52:10 2012 +0200
2.2 +++ b/Admin/MacOS/App1/mk Mon Jul 23 19:07:01 2012 +0200
2.3 @@ -4,15 +4,17 @@
2.4
2.5 THIS="$(cd "$(dirname "$0")"; pwd)"
2.6
2.7 -PLATYPUS_APP="/Applications/Platypus-4.0/Platypus.app"
2.8 COCOADIALOG_APP="/Applications/CocoaDialog.app"
2.9
2.10 -"$PLATYPUS_APP/Contents/Resources/platypus" \
2.11 +/usr/local/bin/platypus \
2.12 -a Isabelle -u Isabelle \
2.13 -I "de.tum.in.isabelle" \
2.14 -i "$THIS/../isabelle.icns" \
2.15 + -D -X thy \
2.16 + -Q "$THIS/../theory.icns" \
2.17 -p /bin/bash \
2.18 - -c "$THIS/script" \
2.19 + -R \
2.20 -o None \
2.21 -f "$COCOADIALOG_APP" \
2.22 + "$THIS/script" \
2.23 "$PWD/Isabelle.app"
3.1 --- a/Admin/init_components Mon Jul 23 18:52:10 2012 +0200
3.2 +++ b/Admin/init_components Mon Jul 23 19:07:01 2012 +0200
3.3 @@ -5,22 +5,11 @@
3.4 # init_components - bash source script to initialize components
3.5 # as specified in the Admin directory
3.6
3.7 -function init_component_liberal
3.8 -{
3.9 - local LOCATION="$1"
3.10 - if [[ -d "${LOCATION}" ]]
3.11 - then
3.12 - init_component "${LOCATION}"
3.13 - else
3.14 - echo "Warning: no component found in ${LOCATION}" >&2
3.15 - fi
3.16 -}
3.17 -
3.18 -while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
3.19 +while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
3.20 do
3.21 - case "${REPLY}" in
3.22 + case "$REPLY" in
3.23 \#* | "") ;;
3.24 - /*) init_component_liberal "${REPLY}" ;;
3.25 - *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
3.26 + /*) init_component "$REPLY" ;;
3.27 + *) init_component "$COMPONENT/$REPLY" ;;
3.28 esac
3.29 -done < "${ISABELLE_HOME}/Admin/components"
3.30 +done < "$ISABELLE_HOME/Admin/components"
4.1 --- a/Admin/isatest/annomaly Mon Jul 23 18:52:10 2012 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,98 +0,0 @@
4.4 -#!/bin/sh
4.5 -
4.6 -# Create AnnoMaLy documentation for Isabelle
4.7 -# See http://martin.von-gagern.net/projects/annomaly/
4.8 -# 2007 Martin von Gagern (martin@von-gagern.net)
4.9 -
4.10 -# Abort on any error
4.11 -set -e -o pipefail
4.12 -
4.13 -BUILD_DIR="$HOME/isabelle.annomaly"
4.14 -ISABELLE_HOME="$BUILD_DIR/Isabelle"
4.15 -ISABELLE_CVS="$HOME/isabelle.cvs"
4.16 -ADMIN_CVS="$ISABELLE_CVS/Admin"
4.17 -# ISABELLE_HOME="$ISABELLE_CVS/Distribution"
4.18 -ISABELLE_SRC="$ISABELLE_HOME/src"
4.19 -HTML_DIR="$HOME/html-data/isabelle-doc"
4.20 -export CVS_RSH=ssh
4.21 -export SMLNJ_HOME="$HOME/annomaly"
4.22 -export PATH="$SMLNJ_HOME/bin:$PATH"
4.23 -export SML_DOC_DIR="$HTML_DIR.tmp"
4.24 -# export SML_DOC_DEBUG="all"
4.25 -TARGET=HOL
4.26 -CVSUP=true
4.27 -
4.28 -# Parse command line
4.29 -for ARG in "$@"; do case "$ARG" in
4.30 - -p) TARGET=Pure ;;
4.31 - -n) CVSUP=false ;;
4.32 - -l) export SML_LOG_DIR="$HOME/logs" ;;
4.33 -esac; done
4.34 -
4.35 -# Update CVS
4.36 -cd "$ADMIN_CVS"
4.37 -if $CVSUP; then
4.38 - echo "Updating CVS"
4.39 - cvs -q up -d
4.40 -fi
4.41 -
4.42 -# Find nightly isabelle tarball
4.43 -ISABELLE_TAR=""
4.44 -for i in /home/html/isatest/Isabelle_[0-9]*-20[0-9][0-9].tar.gz; do
4.45 - if [[ -r "$i" ]]; then ISABELLE_TAR="$i"; fi
4.46 -done
4.47 -if [[ -z $ISABELLE_TAR ]]; then
4.48 - echo "No isabelle tarball found!" >&2
4.49 - exit 1
4.50 -fi
4.51 -
4.52 -# Create build environemnt
4.53 -mkdir -p "$BUILD_DIR"
4.54 -cd "$BUILD_DIR"
4.55 -if [[ -d Isabelle ]]; then
4.56 - rm -rf *
4.57 -fi
4.58 -tar xzf "$ISABELLE_TAR"
4.59 -cd "$ISABELLE_HOME"
4.60 -cp "$ADMIN_CVS"/isatest/annomaly.ML src/Pure/ML-Systems/annomaly.ML
4.61 -ln -s run-smlnj lib/scripts/run-annomaly
4.62 -
4.63 -# Create clean output directory
4.64 -rm -rf "$SML_DOC_DIR"
4.65 -mkdir "$SML_DOC_DIR"
4.66 -cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
4.67 -cat > "$SML_DOC_DIR/.htaccess" <<EOF
4.68 -DirectoryIndex index.html source.html
4.69 -<IfModule mod_deflate>
4.70 -SetOutputFilter DEFLATE
4.71 -</IfModule>
4.72 -AddType text/plain .dot
4.73 -EOF
4.74 -
4.75 -# Build isabelle
4.76 -ISABELLE_HOME="$(cd "$ISABELLE_HOME"; pwd -P)"
4.77 -cd "$ISABELLE_HOME"
4.78 -export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
4.79 -rm -rf heaps
4.80 -./build -b $TARGET
4.81 -cd "$BUILD_DIR"
4.82 -rm -rf *
4.83 -
4.84 -# Postprocess created files
4.85 -cd $SML_DOC_DIR
4.86 -dot -Tsvg depGraph.dot \
4.87 - | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
4.88 - > depGraph.svg
4.89 -dot -Tps2 depGraph.dot > depGraph.ps
4.90 -ps2pdf depGraph.ps depGraph.pdf
4.91 -grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
4.92 -
4.93 -# Install result by renaming, to be almost atomic
4.94 -rm -rf "$HTML_DIR.bac"
4.95 -if [[ -d $HTML_DIR ]]; then mv "$HTML_DIR" "$HTML_DIR.bac"; fi
4.96 -mv "$SML_DOC_DIR" "$HTML_DIR"
4.97 -rm -rf "$HTML_DIR.bac"
4.98 -
4.99 -# Done
4.100 -echo "Completed successfully"
4.101 -exit 0
5.1 --- a/Admin/isatest/annomaly.ML Mon Jul 23 18:52:10 2012 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,69 +0,0 @@
5.4 -(* Title: Admin/isatest/annomaly.ML
5.5 - Author: Martin von Gagern <martin@von-gagern.net>
5.6 -*)
5.7 -
5.8 -use "ML-Systems/smlnj.ML";
5.9 -
5.10 -local
5.11 -
5.12 - val smlnj_use_text = use_text
5.13 -
5.14 - val smlnj_use_file = use_file
5.15 -
5.16 - val smlnj_forget_structure = forget_structure
5.17 -
5.18 - fun mkAbsolute path =
5.19 - OS.Path.mkAbsolute { path = path, relativeTo = OS.FileSys.getDir () }
5.20 -
5.21 - fun toArcs path = #arcs (OS.Path.fromString path)
5.22 -
5.23 - val isabelleHome =
5.24 - case OS.Process.getEnv "ISABELLE_HOME"
5.25 - of NONE => OS.FileSys.getDir ()
5.26 - | SOME home => mkAbsolute home
5.27 -
5.28 - fun noparent [] = []
5.29 - | noparent (n :: ns) =
5.30 - if n = OS.Path.parentArc then noparent ns else n :: noparent ns
5.31 -
5.32 - fun isabellePath [] = []
5.33 - | isabellePath ("src" :: name) = "Isabelle" :: name
5.34 - | isabellePath (name as (n :: ns)) =
5.35 - if n = OS.Path.parentArc then noparent ns else "Isabelle" :: name
5.36 -
5.37 - fun rewrite defPrefix name =
5.38 - let val abs = mkAbsolute name
5.39 - val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
5.40 - val exists = (OS.FileSys.access(abs, nil)
5.41 - handle OS.SysErr _ => false)
5.42 - in if exists andalso rel <> ""
5.43 - then isabellePath (toArcs rel)
5.44 - else defPrefix @ noparent (toArcs name)
5.45 - end handle OS.Path.Path => defPrefix @ noparent (toArcs name)
5.46 -
5.47 -in
5.48 -
5.49 - fun use_text tune str_of_pos name_space (line, name) p v t =
5.50 - let val name = case name of "" => "unnamed" | name => name
5.51 - val arcs = rewrite ["use_text"] name
5.52 - (* should we have different files for different line numbers? *
5.53 - val arcs = if line <= 1 then arcs
5.54 - else arcs @ [ "l." ^ Int.toString line ]
5.55 - *)
5.56 - val arcs = if t = "structure Isabelle =\nstruct\nend;"
5.57 - andalso name = "ML"
5.58 - then ["empty_Isabelle", "empty" ] else arcs
5.59 - val _ = AnnoMaLy.nameNextStream arcs
5.60 - in smlnj_use_text tune str_of_pos name_space (line, name) p v t end;
5.61 -
5.62 - fun use_file tune str_of_pos name_space output verbose name =
5.63 - let val arcs = rewrite ["use_file"] name
5.64 - val _ = AnnoMaLy.nameNextStream arcs
5.65 - in smlnj_use_file tune str_of_pos name_space output verbose name end;
5.66 -
5.67 - fun forget_structure name =
5.68 - let val arcs = [ "forget_structure", name ]
5.69 - val _ = AnnoMaLy.nameNextStream arcs
5.70 - in smlnj_forget_structure name end;
5.71 -
5.72 -end;
6.1 --- a/Admin/isatest/isatest-annomaly Mon Jul 23 18:52:10 2012 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,90 +0,0 @@
6.4 -#!/usr/bin/env bash
6.5 -#
6.6 -# Create AnnoMaLy documentation for Isabelle
6.7 -#
6.8 -# Based on http://martin.von-gagern.net/projects/annomaly/
6.9 -# 2007 Martin von Gagern (martin@von-gagern.net)
6.10 -
6.11 -## global settings
6.12 -. ~/admin/isatest/isatest-settings
6.13 -
6.14 -PRG="$(basename "$0")"
6.15 -
6.16 -export SMLNJ_HOME="/home/gagern/annomaly"
6.17 -export SML_DOC_DIR="$HOME/anno-html"
6.18 -
6.19 -ADMIN="$HOME/admin/isatest"
6.20 -LOGICS="HOL"
6.21 -
6.22 -# Abort on any error
6.23 -set -e -o pipefail
6.24 -
6.25 -function usage()
6.26 -{
6.27 - echo
6.28 - echo "Usage: $PRG"
6.29 - echo
6.30 - echo " Generate html documentation from .ML files"
6.31 - echo
6.32 - exit 1
6.33 -}
6.34 -
6.35 -function fail()
6.36 -{
6.37 - echo "$1" >&2
6.38 - log "FAILED, $1"
6.39 - exit 2
6.40 -}
6.41 -
6.42 -
6.43 -## main
6.44 -
6.45 -ISABELLE_HOME="$DISTPREFIX/Isabelle"
6.46 -ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
6.47 -
6.48 -[ -d $ISABELLE_HOME ] || fail "$ISABELLE_HOME is not a directory."
6.49 -
6.50 -
6.51 -# Create clean output directory
6.52 -rm -rf "$SML_DOC_DIR"
6.53 -mkdir "$SML_DOC_DIR"
6.54 -cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
6.55 -cat > "$SML_DOC_DIR/.htaccess" <<EOF
6.56 -DirectoryIndex index.html source.html
6.57 -<IfModule mod_deflate>
6.58 -SetOutputFilter DEFLATE
6.59 -</IfModule>
6.60 -AddType text/plain .dot
6.61 -EOF
6.62 -
6.63 -# Prepare build environemnt
6.64 -cd "$ISABELLE_HOME"
6.65 -cp "$ADMIN/annomaly.ML" src/Pure/ML-Systems/annomaly.ML
6.66 -ln -fs run-smlnj lib/scripts/run-annomaly
6.67 -
6.68 -cd "$ISABELLE_HOME"
6.69 -export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
6.70 -
6.71 -
6.72 -# Process image(s)
6.73 -for L in $LOGICS
6.74 -do
6.75 - ( cd "$ISABELLE_HOME/src/$L"; \
6.76 - cat ~/settings/annomaly >> $ISABELLE_HOME/etc/settings; \
6.77 - "$ISABELLE_TOOL" make || fail "isabelle make for $L failed." )
6.78 -done
6.79 -
6.80 -
6.81 -# Postprocess created files
6.82 -cd "$SML_DOC_DIR"
6.83 -dot -Tsvg depGraph.dot \
6.84 - | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
6.85 - > depGraph.svg
6.86 -dot -Tps2 depGraph.dot > depGraph.ps
6.87 -ps2pdf depGraph.ps depGraph.pdf
6.88 -
6.89 -# $ISABELLE_HOME does not seem to occur anywhere ??
6.90 -# grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
6.91 -
6.92 -
6.93 -log "annomaly docs generated successfully."
7.1 --- a/Admin/isatest/settings/annomaly Mon Jul 23 18:52:10 2012 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,26 +0,0 @@
7.4 -# -*- shell-script -*- :mode=shellscript:
7.5 -
7.6 -ML_SYSTEM=annomaly
7.7 -ML_HOME="$SMLNJ_HOME/bin"
7.8 -ML_OPTIONS="-m $SMLNJ_HOME/annomaly/annomaly.cm @SMLdebug=/dev/null"
7.9 -ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
7.10 -
7.11 -
7.12 -ISABELLE_HOME_USER="$HOME/isabelle-annomaly"
7.13 -
7.14 -# Where to look for isabelle tools (multiple dirs separated by ':').
7.15 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
7.16 -
7.17 -# Location for temporary files (should be on a local file system).
7.18 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
7.19 -
7.20 -
7.21 -# Heap input locations. ML system identifier is included in lookup.
7.22 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
7.23 -
7.24 -# Heap output location. ML system identifier is appended automatically later on.
7.25 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
7.26 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
7.27 -
7.28 -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
7.29 -
8.1 --- a/Admin/mira.py Mon Jul 23 18:52:10 2012 +0200
8.2 +++ b/Admin/mira.py Mon Jul 23 19:07:01 2012 +0200
8.3 @@ -492,8 +492,8 @@
8.4
8.5 smlnj_settings = '''
8.6 ML_SYSTEM=smlnj
8.7 -ML_HOME="/home/smlnj/110.72/bin"
8.8 -ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
8.9 +ML_HOME="/home/smlnj/110.74/bin"
8.10 +ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
8.11 ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
8.12 '''
8.13
9.1 --- a/etc/settings Mon Jul 23 18:52:10 2012 +0200
9.2 +++ b/etc/settings Mon Jul 23 19:07:01 2012 +0200
9.3 @@ -45,7 +45,7 @@
9.4 # Standard ML of New Jersey (slow!)
9.5 #ML_SYSTEM=smlnj-110
9.6 #ML_HOME="/usr/local/smlnj/bin"
9.7 -#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
9.8 +#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
9.9 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
9.10 #SMLNJ_CYGWIN_RUNTIME=1
9.11
9.12 @@ -93,7 +93,11 @@
9.13 ###
9.14
9.15 # The place for user configuration, heap files, etc.
9.16 -ISABELLE_HOME_USER="$USER_HOME/.isabelle/${ISABELLE_IDENTIFIER:-.}"
9.17 +if [ -z "ISABELLE_IDENTIFIER" ]; then
9.18 + ISABELLE_HOME_USER="$USER_HOME/.isabelle"
9.19 +else
9.20 + ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER"
9.21 +fi
9.22
9.23 # Where to look for isabelle tools (multiple dirs separated by ':').
9.24 ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
10.1 --- a/lib/Tools/build Mon Jul 23 18:52:10 2012 +0200
10.2 +++ b/lib/Tools/build Mon Jul 23 19:07:01 2012 +0200
10.3 @@ -21,6 +21,7 @@
10.4 echo " -j INT maximum number of jobs (default 1)"
10.5 echo " -l list sessions only"
10.6 echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)"
10.7 + echo " -s system build mode: produce output in ISABELLE_HOME"
10.8 echo " -v verbose"
10.9 echo
10.10 echo " Build and manage Isabelle sessions, depending on implicit"
10.11 @@ -52,12 +53,13 @@
10.12 BUILD_IMAGES=false
10.13 MAX_JOBS=1
10.14 LIST_ONLY=false
10.15 +SYSTEM_MODE=false
10.16 VERBOSE=false
10.17
10.18 declare -a MORE_DIRS=()
10.19 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
10.20
10.21 -while getopts "abd:j:lo:v" OPT
10.22 +while getopts "abd:j:lo:sv" OPT
10.23 do
10.24 case "$OPT" in
10.25 a)
10.26 @@ -79,6 +81,9 @@
10.27 o)
10.28 BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
10.29 ;;
10.30 + s)
10.31 + SYSTEM_MODE="true"
10.32 + ;;
10.33 v)
10.34 VERBOSE="true"
10.35 ;;
10.36 @@ -96,5 +101,5 @@
10.37 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
10.38
10.39 exec "$ISABELLE_TOOL" java isabelle.Build \
10.40 - "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$VERBOSE" \
10.41 + "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$SYSTEM_MODE" "$VERBOSE" \
10.42 "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
11.1 --- a/lib/Tools/usedir Mon Jul 23 18:52:10 2012 +0200
11.2 +++ b/lib/Tools/usedir Mon Jul 23 19:07:01 2012 +0200
11.3 @@ -241,7 +241,7 @@
11.4 LOG="$LOGDIR/$ITEM"
11.5
11.6 "$ISABELLE_PROCESS" \
11.7 - -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
11.8 + -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
11.9 -q -w $LOGIC $NAME > "$LOG"
11.10 RC="$?"
11.11 else
11.12 @@ -250,7 +250,7 @@
11.13 LOG="$LOGDIR/$ITEM"
11.14
11.15 "$ISABELLE_PROCESS" \
11.16 - -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
11.17 + -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
11.18 -r -q "$LOGIC" > "$LOG"
11.19 RC="$?"
11.20 cd ..
12.1 --- a/lib/scripts/getsettings Mon Jul 23 18:52:10 2012 +0200
12.2 +++ b/lib/scripts/getsettings Mon Jul 23 19:07:01 2012 +0200
12.3 @@ -163,8 +163,7 @@
12.4 esac
12.5
12.6 if [ ! -d "$COMPONENT" ]; then
12.7 - echo >&2 "Missing Isabelle component directory: \"$COMPONENT\""
12.8 - exit 2
12.9 + echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
12.10 elif [ -z "$ISABELLE_COMPONENTS" ]; then
12.11 ISABELLE_COMPONENTS="$COMPONENT"
12.12 else
13.1 --- a/src/HOL/TPTP/MaSh_Export.thy Mon Jul 23 18:52:10 2012 +0200
13.2 +++ b/src/HOL/TPTP/MaSh_Export.thy Mon Jul 23 19:07:01 2012 +0200
13.3 @@ -11,7 +11,7 @@
13.4
13.5 sledgehammer_params
13.6 [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
13.7 - lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
13.8 + lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize]
13.9
13.10 ML {*
13.11 open MaSh_Export
13.12 @@ -66,5 +66,4 @@
13.13 ()
13.14 *}
13.15
13.16 -
13.17 end
14.1 --- a/src/HOL/TPTP/atp_theory_export.ML Mon Jul 23 18:52:10 2012 +0200
14.2 +++ b/src/HOL/TPTP/atp_theory_export.ML Mon Jul 23 19:07:01 2012 +0200
14.3 @@ -113,10 +113,6 @@
14.4 handle TYPE _ => @{prop True}
14.5 end
14.6
14.7 -fun all_non_tautological_facts_of thy css_table =
14.8 - Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
14.9 - |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd)
14.10 -
14.11 fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
14.12 let
14.13 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
14.14 @@ -126,7 +122,8 @@
14.15 val mono = not (is_type_enc_polymorphic type_enc)
14.16 val path = file_name |> Path.explode
14.17 val _ = File.write path ""
14.18 - val facts = all_non_tautological_facts_of thy css_table
14.19 + val facts =
14.20 + Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
14.21 val atp_problem =
14.22 facts
14.23 |> map (fn ((_, loc), th) =>
15.1 --- a/src/HOL/TPTP/mash_eval.ML Mon Jul 23 18:52:10 2012 +0200
15.2 +++ b/src/HOL/TPTP/mash_eval.ML Mon Jul 23 19:07:01 2012 +0200
15.3 @@ -26,9 +26,7 @@
15.4
15.5 val max_facts_slack = 2
15.6
15.7 -val all_names =
15.8 - filter_out is_likely_tautology_or_too_meta
15.9 - #> map (rpair () o nickname_of) #> Symtab.make
15.10 +val all_names = map (rpair () o nickname_of) #> Symtab.make
15.11
15.12 fun evaluate_mash_suggestions ctxt params thy file_name =
15.13 let
16.1 --- a/src/HOL/TPTP/mash_export.ML Mon Jul 23 18:52:10 2012 +0200
16.2 +++ b/src/HOL/TPTP/mash_export.ML Mon Jul 23 19:07:01 2012 +0200
16.3 @@ -49,9 +49,7 @@
16.4 val thy_name_of_fact = hd o Long_Name.explode
16.5 fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact
16.6
16.7 -val all_names =
16.8 - filter_out is_likely_tautology_or_too_meta
16.9 - #> map (rpair () o nickname_of) #> Symtab.make
16.10 +val all_names = map (rpair () o nickname_of) #> Symtab.make
16.11
16.12 fun generate_accessibility thy include_thy file_name =
16.13 let
17.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Mon Jul 23 18:52:10 2012 +0200
17.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Mon Jul 23 19:07:01 2012 +0200
17.3 @@ -88,11 +88,13 @@
17.4 val isabelle_info : string -> int -> (string, 'a) ho_term list
17.5 val extract_isabelle_status : (string, 'a) ho_term list -> string option
17.6 val extract_isabelle_rank : (string, 'a) ho_term list -> int
17.7 + val inductionN : string
17.8 val introN : string
17.9 val inductiveN : string
17.10 val elimN : string
17.11 val simpN : string
17.12 - val defN : string
17.13 + val non_rec_defN : string
17.14 + val rec_defN : string
17.15 val rankN : string
17.16 val minimum_rank : int
17.17 val default_rank : int
17.18 @@ -222,11 +224,14 @@
17.19
17.20 val isabelle_info_prefix = "isabelle_"
17.21
17.22 +val inductionN = "induction"
17.23 val introN = "intro"
17.24 val inductiveN = "inductive"
17.25 val elimN = "elim"
17.26 val simpN = "simp"
17.27 -val defN = "def"
17.28 +val non_rec_defN = "non_rec_def"
17.29 +val rec_defN = "rec_def"
17.30 +
17.31 val rankN = "rank"
17.32
17.33 val minimum_rank = 0
17.34 @@ -503,9 +508,13 @@
17.35 fun suffix_tag top_level s =
17.36 if top_level then
17.37 case extract_isabelle_status info of
17.38 - SOME s' => if s' = defN then s ^ ":lt"
17.39 - else if s' = simpN andalso gen_simp then s ^ ":lr"
17.40 - else s
17.41 + SOME s' =>
17.42 + if s' = non_rec_defN then
17.43 + s ^ ":lt"
17.44 + else if (s' = simpN orelse s' = rec_defN) andalso gen_simp then
17.45 + s ^ ":lr"
17.46 + else
17.47 + s
17.48 | NONE => s
17.49 else
17.50 s
18.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jul 23 18:52:10 2012 +0200
18.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jul 23 19:07:01 2012 +0200
18.3 @@ -18,7 +18,9 @@
18.4 datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
18.5
18.6 datatype scope = Global | Local | Assum | Chained
18.7 - datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
18.8 + datatype status =
18.9 + General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def |
18.10 + Rec_Def
18.11 type stature = scope * status
18.12
18.13 datatype strictness = Strict | Non_Strict
18.14 @@ -103,6 +105,7 @@
18.15 val helper_table : ((string * bool) * (status * thm) list) list
18.16 val trans_lams_from_string :
18.17 Proof.context -> type_enc -> string -> term list -> term list * term list
18.18 + val string_of_status : status -> string
18.19 val factsN : string
18.20 val prepare_atp_problem :
18.21 Proof.context -> atp_format -> formula_role -> type_enc -> mode -> string
18.22 @@ -123,7 +126,8 @@
18.23 datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
18.24
18.25 datatype scope = Global | Local | Assum | Chained
18.26 -datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
18.27 +datatype status =
18.28 + General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
18.29 type stature = scope * status
18.30
18.31 datatype order =
18.32 @@ -1236,7 +1240,8 @@
18.33 |>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts
18.34 val lam_facts =
18.35 map2 (fn t => fn j =>
18.36 - ((lam_fact_prefix ^ Int.toString j, (Global, Def)), (Axiom, t)))
18.37 + ((lam_fact_prefix ^ Int.toString j,
18.38 + (Global, Non_Rec_Def)), (Axiom, t)))
18.39 lambda_ts (1 upto length lambda_ts)
18.40 in (facts, lam_facts) end
18.41
18.42 @@ -1293,7 +1298,7 @@
18.43 ((name, stature as (_, status)), t) =
18.44 let
18.45 val role =
18.46 - if is_format_with_defs format andalso status = Def andalso
18.47 + if is_format_with_defs format andalso status = Non_Rec_Def andalso
18.48 is_legitimate_tptp_def t then
18.49 Definition
18.50 else
18.51 @@ -1664,18 +1669,18 @@
18.52
18.53 (* The Boolean indicates that a fairly sound type encoding is needed. *)
18.54 val base_helper_table =
18.55 - [(("COMBI", false), [(Def, @{thm Meson.COMBI_def})]),
18.56 - (("COMBK", false), [(Def, @{thm Meson.COMBK_def})]),
18.57 - (("COMBB", false), [(Def, @{thm Meson.COMBB_def})]),
18.58 - (("COMBC", false), [(Def, @{thm Meson.COMBC_def})]),
18.59 - (("COMBS", false), [(Def, @{thm Meson.COMBS_def})]),
18.60 + [(("COMBI", false), [(Non_Rec_Def, @{thm Meson.COMBI_def})]),
18.61 + (("COMBK", false), [(Non_Rec_Def, @{thm Meson.COMBK_def})]),
18.62 + (("COMBB", false), [(Non_Rec_Def, @{thm Meson.COMBB_def})]),
18.63 + (("COMBC", false), [(Non_Rec_Def, @{thm Meson.COMBC_def})]),
18.64 + (("COMBS", false), [(Non_Rec_Def, @{thm Meson.COMBS_def})]),
18.65 ((predicator_name, false), [(General, not_ffalse), (General, ftrue)]),
18.66 (("fFalse", false), [(General, not_ffalse)]),
18.67 (("fFalse", true), [(General, @{thm True_or_False})]),
18.68 (("fTrue", false), [(General, ftrue)]),
18.69 (("fTrue", true), [(General, @{thm True_or_False})]),
18.70 (("If", true),
18.71 - [(Def, @{thm if_True}), (Def, @{thm if_False}),
18.72 + [(Non_Rec_Def, @{thm if_True}), (Non_Rec_Def, @{thm if_False}),
18.73 (General, @{thm True_or_False})])]
18.74
18.75 val helper_table =
18.76 @@ -1683,7 +1688,7 @@
18.77 [(("fNot", false),
18.78 @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
18.79 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
18.80 - |> map (pair Def)),
18.81 + |> map (pair Non_Rec_Def)),
18.82 (("fconj", false),
18.83 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
18.84 by (unfold fconj_def) fast+}
18.85 @@ -1718,19 +1723,19 @@
18.86 ((app_op_name, true),
18.87 [(General, @{lemma "EX x. ~ f x = g x | f = g" by blast})]),
18.88 (("fconj", false),
18.89 - @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Def)),
18.90 + @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
18.91 (("fdisj", false),
18.92 - @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Def)),
18.93 + @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
18.94 (("fimplies", false),
18.95 @{thms fimplies_table fconj_laws fdisj_laws fimplies_laws}
18.96 - |> map (pair Def)),
18.97 + |> map (pair Non_Rec_Def)),
18.98 (("fequal", false),
18.99 - (@{thms fequal_table} |> map (pair Def)) @
18.100 + (@{thms fequal_table} |> map (pair Non_Rec_Def)) @
18.101 (@{thms fequal_laws} |> map (pair General))),
18.102 (("fAll", false),
18.103 - @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Def)),
18.104 + @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def)),
18.105 (("fEx", false),
18.106 - @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
18.107 + @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def))]
18.108 |> map (apsnd (map (apsnd zero_var_indexes)))
18.109
18.110 fun bound_tvars type_enc sorts Ts =
18.111 @@ -2104,28 +2109,29 @@
18.112 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
18.113 in do_formula end
18.114
18.115 +fun string_of_status General = ""
18.116 + | string_of_status Induction = inductionN
18.117 + | string_of_status Intro = introN
18.118 + | string_of_status Inductive = inductiveN
18.119 + | string_of_status Elim = elimN
18.120 + | string_of_status Simp = simpN
18.121 + | string_of_status Non_Rec_Def = non_rec_defN
18.122 + | string_of_status Rec_Def = rec_defN
18.123 +
18.124 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
18.125 of monomorphization). The TPTP explicitly forbids name clashes, and some of
18.126 the remote provers might care. *)
18.127 fun line_for_fact ctxt prefix encode freshen pos mono type_enc rank
18.128 - (j, {name, stature, role, iformula, atomic_types}) =
18.129 - (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, role,
18.130 - iformula
18.131 - |> formula_from_iformula ctxt mono type_enc should_guard_var_in_formula
18.132 - (if pos then SOME true else NONE)
18.133 - |> close_formula_universally
18.134 - |> bound_tvars type_enc true atomic_types,
18.135 - NONE,
18.136 - let val rank = rank j in
18.137 - case snd stature of
18.138 - Intro => isabelle_info introN rank
18.139 - | Inductive => isabelle_info inductiveN rank
18.140 - | Elim => isabelle_info elimN rank
18.141 - | Simp => isabelle_info simpN rank
18.142 - | Def => isabelle_info defN rank
18.143 - | _ => isabelle_info "" rank
18.144 - end)
18.145 - |> Formula
18.146 + (j, {name, stature = (_, status), role, iformula, atomic_types}) =
18.147 + Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
18.148 + encode name,
18.149 + role,
18.150 + iformula
18.151 + |> formula_from_iformula ctxt mono type_enc
18.152 + should_guard_var_in_formula (if pos then SOME true else NONE)
18.153 + |> close_formula_universally
18.154 + |> bound_tvars type_enc true atomic_types,
18.155 + NONE, isabelle_info (string_of_status status) (rank j))
18.156
18.157 fun lines_for_subclass type_enc sub super =
18.158 Formula (subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, Axiom,
18.159 @@ -2355,7 +2361,7 @@
18.160 Axiom,
18.161 eq_formula type_enc (atomic_types_of T) [] false
18.162 (tag_with_type ctxt mono type_enc NONE T x_var) x_var,
18.163 - NONE, isabelle_info defN helper_rank)
18.164 + NONE, isabelle_info non_rec_defN helper_rank)
18.165 end
18.166
18.167 fun lines_for_mono_types ctxt mono type_enc Ts =
18.168 @@ -2438,7 +2444,7 @@
18.169 val tag_with = tag_with_type ctxt mono type_enc NONE
18.170 fun formula c =
18.171 [Formula (ident, role, eq (tag_with res_T c) c, NONE, isabelle_info
18.172 - defN helper_rank)]
18.173 + non_rec_defN helper_rank)]
18.174 in
18.175 if pred_sym orelse not (should_encode_type ctxt mono level res_T) then
18.176 []
18.177 @@ -2538,7 +2544,7 @@
18.178 in
18.179 ([tm1, tm2],
18.180 [Formula (uncurried_alias_eq_prefix ^ s2, role, eq |> maybe_negate,
18.181 - NONE, isabelle_info defN helper_rank)])
18.182 + NONE, isabelle_info non_rec_defN helper_rank)])
18.183 |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
18.184 else pair_append (do_alias (ary - 1)))
18.185 end
18.186 @@ -2878,8 +2884,9 @@
18.187 fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
18.188 val graph =
18.189 Graph.empty
18.190 - |> fold (fold (add_eq_deps (has_status defN)) o snd) problem
18.191 - |> fold (fold (add_eq_deps (has_status simpN orf is_conj)) o snd) problem
18.192 + |> fold (fold (add_eq_deps (has_status non_rec_defN)) o snd) problem
18.193 + |> fold (fold (add_eq_deps (has_status rec_defN orf has_status simpN
18.194 + orf is_conj)) o snd) problem
18.195 |> fold (fold (add_intro_deps (has_status inductiveN)) o snd) problem
18.196 |> fold (fold (add_intro_deps (has_status introN)) o snd) problem
18.197 fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1
19.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jul 23 18:52:10 2012 +0200
19.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jul 23 19:07:01 2012 +0200
19.3 @@ -200,10 +200,11 @@
19.4 else
19.5 isa_ext
19.6
19.7 -fun add_all_defs fact_names accum =
19.8 +fun add_non_rec_defs fact_names accum =
19.9 Vector.foldl
19.10 (fn (facts, facts') =>
19.11 - union (op =) (filter (fn (_, (_, status)) => status = Def) facts)
19.12 + union (op =)
19.13 + (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts)
19.14 facts')
19.15 accum fact_names
19.16
19.17 @@ -214,12 +215,12 @@
19.18 (* LEO 1.3.3 does not record definitions properly, leading to missing
19.19 dependencies in the TSTP proof. Remove the next line once this is
19.20 fixed. *)
19.21 - add_all_defs fact_names
19.22 + add_non_rec_defs fact_names
19.23 else if rule = satallax_unsat_coreN then
19.24 (fn [] =>
19.25 (* Satallax doesn't include definitions in its unsatisfiable cores,
19.26 so we assume the worst and include them all here. *)
19.27 - [(ext_name ctxt, (Global, General))] |> add_all_defs fact_names
19.28 + [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
19.29 | facts => facts)
19.30 else
19.31 I)
20.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jul 23 18:52:10 2012 +0200
20.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jul 23 19:07:01 2012 +0200
20.3 @@ -23,7 +23,6 @@
20.4 val fact_from_ref :
20.5 Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
20.6 -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
20.7 - val is_likely_tautology_or_too_meta : thm -> bool
20.8 val backquote_thm : thm -> string
20.9 val clasimpset_rule_table_of : Proof.context -> status Termtab.table
20.10 val maybe_instantiate_inducts :
20.11 @@ -50,8 +49,6 @@
20.12 del : (Facts.ref * Attrib.src list) list,
20.13 only : bool}
20.14
20.15 -val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
20.16 -
20.17 (* experimental features *)
20.18 val ignore_no_atp =
20.19 Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
20.20 @@ -147,10 +144,11 @@
20.21 fun multi_base_blacklist ctxt ho_atp =
20.22 ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
20.23 "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
20.24 - "weak_case_cong"]
20.25 + "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps",
20.26 + "nibble.distinct"]
20.27 |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
20.28 append ["induct", "inducts"]
20.29 - |> map (prefix ".")
20.30 + |> map (prefix Long_Name.separator)
20.31
20.32 val max_lambda_nesting = 3 (*only applies if not ho_atp*)
20.33
20.34 @@ -162,12 +160,11 @@
20.35
20.36 (* Don't count nested lambdas at the level of formulas, since they are
20.37 quantifiers. *)
20.38 -fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
20.39 - | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
20.40 - formula_has_too_many_lambdas false (T :: Ts) t
20.41 - | formula_has_too_many_lambdas _ Ts t =
20.42 +fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
20.43 + formula_has_too_many_lambdas (T :: Ts) t
20.44 + | formula_has_too_many_lambdas Ts t =
20.45 if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
20.46 - exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t))
20.47 + exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
20.48 else
20.49 term_has_too_many_lambdas max_lambda_nesting t
20.50
20.51 @@ -180,11 +177,17 @@
20.52 | apply_depth _ = 0
20.53
20.54 fun is_formula_too_complex ho_atp t =
20.55 - apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
20.56 + apply_depth t > max_apply_depth orelse
20.57 + (not ho_atp andalso formula_has_too_many_lambdas [] t)
20.58
20.59 -(* FIXME: Extend to "Meson" and "Metis" *)
20.60 +(* These theories contain auxiliary facts that could positively confuse
20.61 + Sledgehammer if they were included. *)
20.62 +val sledgehammer_prefixes =
20.63 + ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator)
20.64 +
20.65 val exists_sledgehammer_const =
20.66 - exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
20.67 + exists_Const (fn (s, _) =>
20.68 + exists (fn pref => String.isPrefix pref s) sledgehammer_prefixes)
20.69
20.70 (* FIXME: make more reliable *)
20.71 val exists_low_level_class_const =
20.72 @@ -192,25 +195,11 @@
20.73 s = @{const_name equal_class.equal} orelse
20.74 String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
20.75
20.76 -fun is_metastrange_theorem th =
20.77 - case head_of (concl_of th) of
20.78 - Const (s, _) => (s <> @{const_name Trueprop} andalso
20.79 - s <> @{const_name "=="})
20.80 - | _ => false
20.81 -
20.82 fun is_that_fact th =
20.83 String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
20.84 andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
20.85 | _ => false) (prop_of th)
20.86
20.87 -fun is_theorem_bad_for_atps ho_atp thm =
20.88 - is_metastrange_theorem thm orelse
20.89 - let val t = prop_of thm in
20.90 - is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
20.91 - exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
20.92 - is_that_fact thm
20.93 - end
20.94 -
20.95 fun is_likely_tautology_or_too_meta th =
20.96 let
20.97 val is_boring_const = member (op =) atp_widely_irrelevant_consts
20.98 @@ -229,6 +218,15 @@
20.99 is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
20.100 end
20.101
20.102 +fun is_theorem_bad_for_atps ho_atp th =
20.103 + is_likely_tautology_or_too_meta th orelse
20.104 + let val t = prop_of th in
20.105 + is_formula_too_complex ho_atp t orelse
20.106 + exists_type type_has_top_sort t orelse
20.107 + exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
20.108 + is_that_fact th
20.109 + end
20.110 +
20.111 fun hackish_string_for_term thy t =
20.112 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
20.113 (print_mode_value ())) (Syntax.string_of_term_global thy) t
20.114 @@ -299,8 +297,8 @@
20.115 |> maps (snd o snd)
20.116 in
20.117 Termtab.empty |> add Simp [atomize] snd simps
20.118 - |> add Simp [] I rec_defs
20.119 - |> add Def [] I nonrec_defs
20.120 + |> add Rec_Def [] I rec_defs
20.121 + |> add Non_Rec_Def [] I nonrec_defs
20.122 (* Add once it is used:
20.123 |> add Elim [] I elims
20.124 *)
20.125 @@ -458,7 +456,6 @@
20.126 else
20.127 let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
20.128 all_facts ctxt ho_atp reserved add chained css
20.129 - |> filter_out (is_likely_tautology_or_too_meta o snd)
20.130 |> filter_out (member Thm.eq_thm_prop del o snd)
20.131 |> maybe_filter_no_atps ctxt
20.132 |> uniquify
21.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jul 23 18:52:10 2012 +0200
21.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jul 23 19:07:01 2012 +0200
21.3 @@ -29,7 +29,7 @@
21.4 open Sledgehammer_MaSh
21.5 open Sledgehammer_Run
21.6
21.7 -val cvc3N = "cvc3"
21.8 +(* val cvc3N = "cvc3" *)
21.9 val yicesN = "yices"
21.10 val z3N = "z3"
21.11
21.12 @@ -226,7 +226,7 @@
21.13 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
21.14 timeout, it makes sense to put E first. *)
21.15 fun default_provers_param_value ctxt =
21.16 - [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN, cvc3N]
21.17 + [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN]
21.18 |> map_filter (remotify_prover_if_not_installed ctxt)
21.19 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
21.20 max_default_remote_threads)
21.21 @@ -404,11 +404,11 @@
21.22 else
21.23 ();
21.24 mash_learn ctxt (get_params Normal ctxt
21.25 - (("timeout",
21.26 - [string_of_real default_learn_atp_timeout]) ::
21.27 + ([("timeout",
21.28 + [string_of_real default_learn_atp_timeout]),
21.29 + ("slice", ["false"])] @
21.30 override_params @
21.31 - [("slice", ["false"]),
21.32 - ("minimize", ["true"]),
21.33 + [("minimize", ["true"]),
21.34 ("preplay_timeout", ["0"])]))
21.35 fact_override (#facts (Proof.goal state))
21.36 (subcommand = learn_atpN orelse subcommand = relearn_atpN))
22.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jul 23 18:52:10 2012 +0200
22.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jul 23 19:07:01 2012 +0200
22.3 @@ -59,7 +59,7 @@
22.4 val mash_can_suggest_facts : Proof.context -> bool
22.5 val mash_suggested_facts :
22.6 Proof.context -> params -> string -> int -> term list -> term
22.7 - -> ('a * thm) list -> (('a * thm) * real) list * ('a * thm) list
22.8 + -> fact list -> (fact * real) list * fact list
22.9 val mash_learn_proof :
22.10 Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
22.11 -> unit
22.12 @@ -106,7 +106,7 @@
22.13 getenv "ISABELLE_HOME_USER" ^ "/mash"
22.14 |> tap (Isabelle_System.mkdir o Path.explode)
22.15 val mash_state_dir = mash_model_dir
22.16 -fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
22.17 +fun mash_state_file () = mash_state_dir () ^ "/state"
22.18
22.19
22.20 (*** Isabelle helpers ***)
22.21 @@ -312,25 +312,44 @@
22.22 |> forall is_lambda_free ts ? cons "no_lams"
22.23 |> forall (not o exists_Const is_exists) ts ? cons "no_skos"
22.24 |> scope <> Global ? cons "local"
22.25 - |> (case status of
22.26 - General => I
22.27 - | Induction => cons "induction"
22.28 - | Intro => cons "intro"
22.29 - | Inductive => cons "inductive"
22.30 - | Elim => cons "elim"
22.31 - | Simp => cons "simp"
22.32 - | Def => cons "def")
22.33 + |> (case string_of_status status of "" => I | s => cons s)
22.34
22.35 (* Too many dependencies is a sign that a decision procedure is at work. There
22.36 isn't much too learn from such proofs. *)
22.37 -val max_dependencies = 10
22.38 +val max_dependencies = 20
22.39 val atp_dependency_default_max_fact = 50
22.40
22.41 -fun trim_dependencies deps =
22.42 - if length deps <= max_dependencies then SOME deps else NONE
22.43 +(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
22.44 +val typedef_deps = [@{thm CollectI} |> nickname_of]
22.45
22.46 -fun isar_dependencies_of all_names =
22.47 - thms_in_proof (SOME all_names) #> trim_dependencies
22.48 +(* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *)
22.49 +val typedef_ths =
22.50 + @{thms type_definition.Abs_inverse type_definition.Rep_inverse
22.51 + type_definition.Rep type_definition.Rep_inject
22.52 + type_definition.Abs_inject type_definition.Rep_cases
22.53 + type_definition.Abs_cases type_definition.Rep_induct
22.54 + type_definition.Abs_induct type_definition.Rep_range
22.55 + type_definition.Abs_image}
22.56 + |> map nickname_of
22.57 +
22.58 +fun is_size_def [dep] th =
22.59 + (case first_field ".recs" dep of
22.60 + SOME (pref, _) =>
22.61 + (case first_field ".size" (nickname_of th) of
22.62 + SOME (pref', _) => pref = pref'
22.63 + | NONE => false)
22.64 + | NONE => false)
22.65 + | is_size_def _ _ = false
22.66 +
22.67 +fun trim_dependencies th deps =
22.68 + if length deps > max_dependencies orelse deps = typedef_deps orelse
22.69 + exists (member (op =) typedef_ths) deps orelse is_size_def deps th then
22.70 + NONE
22.71 + else
22.72 + SOME deps
22.73 +
22.74 +fun isar_dependencies_of all_names th =
22.75 + th |> thms_in_proof (SOME all_names) |> trim_dependencies th
22.76
22.77 fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
22.78 auto_level facts all_names th =
22.79 @@ -376,7 +395,7 @@
22.80 end
22.81 else
22.82 ();
22.83 - used_facts |> map fst |> trim_dependencies)
22.84 + used_facts |> map fst |> trim_dependencies th)
22.85 | _ => NONE
22.86 end
22.87
22.88 @@ -385,11 +404,11 @@
22.89
22.90 (* more friendly than "try o File.rm" for those who keep the files open in their
22.91 text editor *)
22.92 -fun wipe_out file = File.write file ""
22.93 +fun wipe_out_file file = File.write (Path.explode file) ""
22.94
22.95 -fun write_file (xs, f) file =
22.96 +fun write_file heading (xs, f) file =
22.97 let val path = Path.explode file in
22.98 - wipe_out path;
22.99 + File.write path heading;
22.100 xs |> chunk_list 500
22.101 |> List.app (File.append path o space_implode "" o map f)
22.102 end
22.103 @@ -411,8 +430,8 @@
22.104 mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^
22.105 " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file
22.106 in
22.107 - write_file ([], K "") sugg_file;
22.108 - write_file write_cmds cmd_file;
22.109 + write_file "" ([], K "") sugg_file;
22.110 + write_file "" write_cmds cmd_file;
22.111 trace_msg ctxt (fn () => "Running " ^ command);
22.112 Isabelle_System.bash command;
22.113 read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these)
22.114 @@ -422,8 +441,7 @@
22.115 | SOME "" => "Done"
22.116 | SOME s => "Error: " ^ elide_string 1000 s))
22.117 |> not overlord
22.118 - ? tap (fn _ => List.app (wipe_out o Path.explode)
22.119 - [err_file, sugg_file, cmd_file])
22.120 + ? tap (fn _ => List.app wipe_out_file [err_file, sugg_file, cmd_file])
22.121 end
22.122
22.123 fun str_of_add (name, parents, feats, deps) =
22.124 @@ -506,7 +524,7 @@
22.125
22.126 fun load _ (state as (true, _)) = state
22.127 | load ctxt _ =
22.128 - let val path = mash_state_path () in
22.129 + let val path = mash_state_file () |> Path.explode in
22.130 (true,
22.131 case try File.read_lines path of
22.132 SOME (version' :: node_lines) =>
22.133 @@ -531,15 +549,13 @@
22.134
22.135 fun save ctxt {fact_G} =
22.136 let
22.137 - val path = mash_state_path ()
22.138 - fun fact_line_for name parents =
22.139 - escape_meta name ^ ": " ^ escape_metas parents
22.140 - val append_fact = File.append path o suffix "\n" oo fact_line_for
22.141 - fun append_entry (name, ((), (parents, _))) () =
22.142 - append_fact name (Graph.Keys.dest parents)
22.143 + fun str_of_entry (name, parents) =
22.144 + escape_meta name ^ ": " ^ escape_metas parents ^ "\n"
22.145 + fun append_entry (name, ((), (parents, _))) =
22.146 + cons (name, Graph.Keys.dest parents)
22.147 + val entries = [] |> Graph.fold append_entry fact_G
22.148 in
22.149 - File.write path (version ^ "\n");
22.150 - Graph.fold append_entry fact_G ();
22.151 + write_file (version ^ "\n") (entries, str_of_entry) (mash_state_file ());
22.152 trace_msg ctxt (fn () => "Saved fact graph (" ^ graph_info fact_G ^ ")")
22.153 end
22.154
22.155 @@ -551,12 +567,17 @@
22.156 fun mash_map ctxt f =
22.157 Synchronized.change global_state (load ctxt ##> (f #> tap (save ctxt)))
22.158
22.159 +fun mash_peek ctxt f =
22.160 + Synchronized.change_result global_state (load ctxt #> `snd #>> f)
22.161 +
22.162 fun mash_get ctxt =
22.163 Synchronized.change_result global_state (load ctxt #> `snd)
22.164
22.165 fun mash_unlearn ctxt =
22.166 Synchronized.change global_state (fn _ =>
22.167 - (mash_CLEAR ctxt; wipe_out (mash_state_path ()); (true, empty_state)))
22.168 + (mash_CLEAR ctxt;
22.169 + wipe_out_file (mash_state_file ());
22.170 + (true, empty_state)))
22.171
22.172 end
22.173
22.174 @@ -598,28 +619,43 @@
22.175 (* Generate more suggestions than requested, because some might be thrown out
22.176 later for various reasons and "meshing" gives better results with some
22.177 slack. *)
22.178 -fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
22.179 +fun max_suggs_of max_facts = max_facts + Int.min (50, max_facts)
22.180
22.181 fun is_fact_in_graph fact_G (_, th) =
22.182 can (Graph.get_node fact_G) (nickname_of th)
22.183
22.184 +fun interleave 0 _ _ = []
22.185 + | interleave n [] ys = take n ys
22.186 + | interleave n xs [] = take n xs
22.187 + | interleave 1 (x :: _) _ = [x]
22.188 + | interleave n (x :: xs) (y :: ys) = x :: y :: interleave (n - 2) xs ys
22.189 +
22.190 fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
22.191 concl_t facts =
22.192 let
22.193 val thy = Proof_Context.theory_of ctxt
22.194 - val fact_G = #fact_G (mash_get ctxt)
22.195 - val parents = maximal_in_graph fact_G facts
22.196 - val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
22.197 - val suggs =
22.198 - if Graph.is_empty fact_G then []
22.199 - else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
22.200 - val selected =
22.201 + val (fact_G, suggs) =
22.202 + mash_peek ctxt (fn {fact_G} =>
22.203 + if Graph.is_empty fact_G then
22.204 + (fact_G, [])
22.205 + else
22.206 + let
22.207 + val parents = maximal_in_graph fact_G facts
22.208 + val feats =
22.209 + features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
22.210 + in
22.211 + (fact_G, mash_QUERY ctxt overlord (max_suggs_of max_facts)
22.212 + (parents, feats))
22.213 + end)
22.214 + val sels =
22.215 facts |> suggested_facts suggs
22.216 (* The weights currently returned by "mash.py" are too extreme to
22.217 make any sense. *)
22.218 - |> map fst |> weight_mepo_facts
22.219 - val unknown = facts |> filter_out (is_fact_in_graph fact_G)
22.220 - in (selected, unknown) end
22.221 + |> map fst
22.222 + val (unk_global, unk_local) =
22.223 + facts |> filter_out (is_fact_in_graph fact_G)
22.224 + |> List.partition (fn ((_, (scope, _)), _) => scope = Global)
22.225 + in (interleave max_facts unk_local sels |> weight_mepo_facts, unk_global) end
22.226
22.227 fun add_to_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
22.228 let
22.229 @@ -638,7 +674,7 @@
22.230 val hard_timeout = time_mult learn_timeout_slack timeout
22.231 val birth_time = Time.now ()
22.232 val death_time = Time.+ (birth_time, hard_timeout)
22.233 - val desc = ("machine learner for Sledgehammer", "")
22.234 + val desc = ("Machine learner for Sledgehammer", "")
22.235 in Async_Manager.launch MaShN birth_time death_time desc task end
22.236
22.237 fun freshish_name () =
22.238 @@ -656,12 +692,22 @@
22.239 val name = freshish_name ()
22.240 val feats = features_of ctxt prover thy (Local, General) [t]
22.241 val deps = used_ths |> map nickname_of
22.242 - val {fact_G} = mash_get ctxt
22.243 - val parents = maximal_in_graph fact_G facts
22.244 in
22.245 - mash_ADD ctxt overlord [(name, parents, feats, deps)]; (true, "")
22.246 + mash_peek ctxt (fn {fact_G} =>
22.247 + let val parents = maximal_in_graph fact_G facts in
22.248 + mash_ADD ctxt overlord [(name, parents, feats, deps)]
22.249 + end);
22.250 + (true, "")
22.251 end)
22.252
22.253 +val evil_theories =
22.254 + ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick",
22.255 + "New_DSequence", "New_Random_Sequence", "Quickcheck",
22.256 + "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"]
22.257 +
22.258 +fun fact_has_evil_theory (_, th) =
22.259 + member (op =) evil_theories (Context.theory_name (theory_of_thm th))
22.260 +
22.261 fun sendback sub =
22.262 Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
22.263
22.264 @@ -676,7 +722,8 @@
22.265 Time.+ (Timer.checkRealTimer timer, commit_timeout)
22.266 val {fact_G} = mash_get ctxt
22.267 val (old_facts, new_facts) =
22.268 - facts |> List.partition (is_fact_in_graph fact_G)
22.269 + facts |> filter_out fact_has_evil_theory
22.270 + |> List.partition (is_fact_in_graph fact_G)
22.271 ||> sort (thm_ord o pairself snd)
22.272 in
22.273 if null new_facts andalso (not atp orelse null old_facts) then
22.274 @@ -691,15 +738,14 @@
22.275 else
22.276 let
22.277 val all_names =
22.278 - facts |> map snd
22.279 - |> filter_out is_likely_tautology_or_too_meta
22.280 - |> map (rpair () o nickname_of)
22.281 - |> Symtab.make
22.282 - val deps_of =
22.283 - if atp then
22.284 - atp_dependencies_of ctxt params prover auto_level facts all_names
22.285 + facts |> map snd |> map (rpair () o nickname_of) |> Symtab.make
22.286 + fun deps_of status th =
22.287 + if status = Non_Rec_Def orelse status = Rec_Def then
22.288 + SOME []
22.289 + else if atp then
22.290 + atp_dependencies_of ctxt params prover auto_level facts all_names th
22.291 else
22.292 - isar_dependencies_of all_names
22.293 + isar_dependencies_of all_names th
22.294 fun do_commit [] [] state = state
22.295 | do_commit adds reps {fact_G} =
22.296 let
22.297 @@ -727,13 +773,13 @@
22.298 else
22.299 ())
22.300 fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum
22.301 - | learn_new_fact ((_, stature), th)
22.302 + | learn_new_fact ((_, stature as (_, status)), th)
22.303 (adds, (parents, n, next_commit, _)) =
22.304 let
22.305 val name = nickname_of th
22.306 val feats =
22.307 features_of ctxt prover (theory_of_thm th) stature [prop_of th]
22.308 - val deps = deps_of th |> these
22.309 + val deps = deps_of status th |> these
22.310 val n = n |> not (null deps) ? Integer.add 1
22.311 val adds = (name, parents, feats, deps) :: adds
22.312 val (adds, next_commit) =
22.313 @@ -759,11 +805,12 @@
22.314 |> fold learn_new_fact new_facts
22.315 in commit true adds []; n end
22.316 fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
22.317 - | relearn_old_fact (_, th) (reps, (n, next_commit, _)) =
22.318 + | relearn_old_fact ((_, (_, status)), th)
22.319 + (reps, (n, next_commit, _)) =
22.320 let
22.321 val name = nickname_of th
22.322 val (n, reps) =
22.323 - case deps_of th of
22.324 + case deps_of status th of
22.325 SOME deps => (n + 1, (name, deps) :: reps)
22.326 | NONE => (n, reps)
22.327 val (reps, next_commit) =
22.328 @@ -774,7 +821,7 @@
22.329 val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
22.330 in (reps, (n, next_commit, timed_out)) end
22.331 val n =
22.332 - if null old_facts then
22.333 + if not atp orelse null old_facts then
22.334 n
22.335 else
22.336 let
23.1 --- a/src/Pure/General/file.ML Mon Jul 23 18:52:10 2012 +0200
23.2 +++ b/src/Pure/General/file.ML Mon Jul 23 19:07:01 2012 +0200
23.3 @@ -45,11 +45,7 @@
23.4
23.5 val platform_path = Path.implode o Path.expand;
23.6
23.7 -fun shell_quote s =
23.8 - if exists_string (fn c => c = "'") s then
23.9 - error ("Illegal single quote in path specification: " ^ quote s)
23.10 - else enclose "'" "'" s;
23.11 -
23.12 +val shell_quote = enclose "'" "'";
23.13 val shell_path = shell_quote o platform_path;
23.14
23.15
24.1 --- a/src/Pure/System/build.scala Mon Jul 23 18:52:10 2012 +0200
24.2 +++ b/src/Pure/System/build.scala Mon Jul 23 19:07:01 2012 +0200
24.3 @@ -340,20 +340,20 @@
24.4 def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
24.5 }
24.6
24.7 - private def start_job(save: Boolean, name: String, info: Session.Info): Job =
24.8 + private def start_job(name: String, info: Session.Info, output: Option[String]): Job =
24.9 {
24.10 val parent = info.parent.getOrElse("")
24.11
24.12 val cwd = info.dir.file
24.13 - val env = Map("INPUT" -> parent, "TARGET" -> name)
24.14 + val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output.getOrElse(""))
24.15 val script =
24.16 - if (is_pure(name)) "./build " + (if (save) "-b " else "") + name
24.17 + if (is_pure(name)) "./build " + name + " \"$OUTPUT\""
24.18 else {
24.19 """
24.20 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
24.21 """ +
24.22 - (if (save)
24.23 - """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$TARGET" """
24.24 + (if (output.isDefined)
24.25 + """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" """
24.26 else
24.27 """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
24.28 """
24.29 @@ -372,7 +372,7 @@
24.30 {
24.31 import XML.Encode._
24.32 pair(bool, pair(string, pair(string, list(string))))(
24.33 - save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
24.34 + output.isDefined, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
24.35 }
24.36 new Job(cwd, env, script, YXML.string_of_body(args_xml))
24.37 }
24.38 @@ -384,29 +384,31 @@
24.39 private def sleep(): Unit = Thread.sleep(500)
24.40
24.41 def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
24.42 - list_only: Boolean, verbose: Boolean,
24.43 + list_only: Boolean, system_mode: Boolean, verbose: Boolean,
24.44 more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
24.45 {
24.46 val options = (Options.init() /: more_options)(_.define_simple(_))
24.47 val queue = find_sessions(options, all_sessions, sessions, more_dirs)
24.48 val deps = dependencies(queue)
24.49
24.50 + val (output_dir, browser_info) =
24.51 + if (system_mode) (Path.explode("~~/heaps/$ML_IDENTIFIER"), Path.explode("~~/browser_info"))
24.52 + else (Path.explode("$ISABELLE_OUTPUT"), Path.explode("$ISABELLE_BROWSER_INFO"))
24.53
24.54 // prepare browser info dir
24.55 - if (options.bool("browser_info") &&
24.56 - !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
24.57 + if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile)
24.58 {
24.59 - Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
24.60 - File.copy(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif"),
24.61 - Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif"))
24.62 - File.write(Path.explode("$ISABELLE_BROWSER_INFO/index.html"),
24.63 - File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template")) +
24.64 - File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template")) +
24.65 - File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template")))
24.66 + browser_info.file.mkdirs()
24.67 + File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
24.68 + browser_info + Path.explode("isabelle.gif"))
24.69 + File.write(browser_info + Path.explode("index.html"),
24.70 + File.read(Path.explode("~~/lib/html/library_index_header.template")) +
24.71 + File.read(Path.explode("~~/lib/html/library_index_content.template")) +
24.72 + File.read(Path.explode("~~/lib/html/library_index_footer.template")))
24.73 }
24.74
24.75 // prepare log dir
24.76 - val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
24.77 + val log_dir = output_dir + Path.explode("log")
24.78 log_dir.file.mkdirs()
24.79
24.80 // scheduler loop
24.81 @@ -447,9 +449,12 @@
24.82 loop(pending - name, running, results + (name -> 0))
24.83 }
24.84 else if (info.parent.map(results(_)).forall(_ == 0)) {
24.85 - val save = build_images || queue.is_inner(name)
24.86 - echo((if (save) "Building " else "Running ") + name + " ...")
24.87 - val job = start_job(save, name, info)
24.88 + val output =
24.89 + if (build_images || queue.is_inner(name))
24.90 + Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
24.91 + else None
24.92 + echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
24.93 + val job = start_job(name, info, output)
24.94 loop(pending, running + (name -> job), results)
24.95 }
24.96 else {
24.97 @@ -477,10 +482,11 @@
24.98 Properties.Value.Boolean(build_images) ::
24.99 Properties.Value.Int(max_jobs) ::
24.100 Properties.Value.Boolean(list_only) ::
24.101 + Properties.Value.Boolean(system_mode) ::
24.102 Properties.Value.Boolean(verbose) ::
24.103 Command_Line.Chunks(more_dirs, options, sessions) =>
24.104 - build(all_sessions, build_images, max_jobs, list_only, verbose,
24.105 - more_dirs.map(Path.explode), options, sessions)
24.106 + build(all_sessions, build_images, max_jobs, list_only, system_mode,
24.107 + verbose, more_dirs.map(Path.explode), options, sessions)
24.108 case _ => error("Bad arguments:\n" + cat_lines(args))
24.109 }
24.110 }
25.1 --- a/src/Pure/System/session.ML Mon Jul 23 18:52:10 2012 +0200
25.2 +++ b/src/Pure/System/session.ML Mon Jul 23 19:07:01 2012 +0200
25.3 @@ -10,7 +10,7 @@
25.4 val name: unit -> string
25.5 val welcome: unit -> string
25.6 val init: bool -> string -> string -> unit
25.7 - val use_dir: string -> string -> bool -> string list -> bool -> bool ->
25.8 + val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
25.9 string -> bool -> string list -> string -> string -> bool * string ->
25.10 string -> int -> bool -> bool -> int -> int -> int -> int -> unit
25.11 val finish: unit -> unit
25.12 @@ -94,12 +94,12 @@
25.13 fun dumping (_, "") = NONE
25.14 | dumping (cp, path) = SOME (cp, Path.explode path);
25.15
25.16 -fun use_dir item root build modes reset info doc doc_graph doc_variants parent
25.17 +fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
25.18 name dump rpath level timing verbose max_threads trace_threads
25.19 parallel_proofs parallel_proofs_threshold =
25.20 ((fn () =>
25.21 (init reset parent name;
25.22 - Present.init build info doc doc_graph doc_variants (path ()) name
25.23 + Present.init build info info_path doc doc_graph doc_variants (path ()) name
25.24 (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
25.25 if timing then
25.26 let
26.1 --- a/src/Pure/Thy/present.ML Mon Jul 23 18:52:10 2012 +0200
26.2 +++ b/src/Pure/Thy/present.ML Mon Jul 23 19:07:01 2012 +0200
26.3 @@ -17,7 +17,7 @@
26.4 path: string, parents: string list} list -> Path.T -> unit
26.5 val display_graph: {name: string, ID: string, dir: string, unfold: bool,
26.6 path: string, parents: string list} list -> unit
26.7 - val init: bool -> bool -> string -> bool -> string list -> string list ->
26.8 + val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
26.9 string -> (bool * Path.T) option -> Url.T option * bool -> bool ->
26.10 theory list -> unit (*not thread-safe!*)
26.11 val finish: unit -> unit (*not thread-safe!*)
26.12 @@ -34,8 +34,6 @@
26.13
26.14 (** paths **)
26.15
26.16 -val output_path = Path.variable "ISABELLE_BROWSER_INFO";
26.17 -
26.18 val tex_ext = Path.ext "tex";
26.19 val tex_path = tex_ext o Path.basic;
26.20 val html_ext = Path.ext "html";
26.21 @@ -275,7 +273,7 @@
26.22
26.23 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
26.24
26.25 -fun init build info doc doc_graph doc_variants path name dump_prefix
26.26 +fun init build info info_path doc doc_graph doc_variants path name dump_prefix
26.27 (remote_path, first_time) verbose thys =
26.28 if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
26.29 (browser_info := empty_browser_info; session_info := NONE)
26.30 @@ -284,7 +282,7 @@
26.31 val parent_name = name_of_session (take (length path - 1) path);
26.32 val session_name = name_of_session path;
26.33 val sess_prefix = Path.make path;
26.34 - val html_prefix = Path.append (Path.expand output_path) sess_prefix;
26.35 + val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix;
26.36
26.37 val documents =
26.38 if doc = "" then []
27.1 --- a/src/Pure/build Mon Jul 23 18:52:10 2012 +0200
27.2 +++ b/src/Pure/build Mon Jul 23 19:07:01 2012 +0200
27.3 @@ -12,12 +12,7 @@
27.4 function usage()
27.5 {
27.6 echo
27.7 - echo "Usage: $PRG [OPTIONS] TARGET"
27.8 - echo
27.9 - echo " Options are:"
27.10 - echo " -b build target images"
27.11 - echo
27.12 - echo " Build Isabelle/ML TARGET: RAW or Pure"
27.13 + echo "Usage: $PRG TARGET OUTPUT"
27.14 echo
27.15 exit 1
27.16 }
27.17 @@ -33,32 +28,14 @@
27.18
27.19 ## process command line
27.20
27.21 -# options
27.22 -
27.23 -BUILD_IMAGES=false
27.24 -
27.25 -while getopts "b" OPT
27.26 -do
27.27 - case "$OPT" in
27.28 - b)
27.29 - BUILD_IMAGES="true"
27.30 - ;;
27.31 - \?)
27.32 - usage
27.33 - ;;
27.34 - esac
27.35 -done
27.36 -
27.37 -shift $(($OPTIND - 1))
27.38 -
27.39 -
27.40 # args
27.41
27.42 -TARGET="Pure"
27.43 -[ "$#" -ge 1 ] && { TARGET="$1"; shift; }
27.44 -[ "$TARGET" = RAW -o "$TARGET" = Pure ] || fail "Bad target: \"$TARGET\""
27.45 -
27.46 -[ "$#" -eq 0 ] || usage
27.47 +if [ "$#" -eq 2 ]; then
27.48 + TARGET="$1"; shift
27.49 + OUTPUT="$1"; shift
27.50 +else
27.51 + usage
27.52 +fi
27.53
27.54
27.55 ## main
27.56 @@ -79,7 +56,7 @@
27.57 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
27.58
27.59 if [ "$TARGET" = RAW ]; then
27.60 - if [ "$BUILD_IMAGES" = false ]; then
27.61 + if [ -z "$OUTPUT" ]; then
27.62 "$ISABELLE_PROCESS" \
27.63 -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
27.64 -q RAW_ML_SYSTEM
27.65 @@ -88,10 +65,10 @@
27.66 -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
27.67 -e "structure Isar = struct fun main () = () end;" \
27.68 -e "ml_prompts \"ML> \" \"ML# \";" \
27.69 - -q -w RAW_ML_SYSTEM RAW
27.70 + -q -w RAW_ML_SYSTEM "$OUTPUT"
27.71 fi
27.72 else
27.73 - if [ "$BUILD_IMAGES" = false ]; then
27.74 + if [ -z "$OUTPUT" ]; then
27.75 "$ISABELLE_PROCESS" \
27.76 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
27.77 -q RAW_ML_SYSTEM
27.78 @@ -99,7 +76,7 @@
27.79 "$ISABELLE_PROCESS" \
27.80 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
27.81 -e "ml_prompts \"ML> \" \"ML# \";" \
27.82 - -f -q -w RAW_ML_SYSTEM Pure
27.83 + -f -q -w RAW_ML_SYSTEM "$OUTPUT"
27.84 fi
27.85 fi
27.86