--- a/Admin/MacOS/App1/README Mon Jul 23 18:52:10 2012 +0200
+++ b/Admin/MacOS/App1/README Mon Jul 23 19:07:01 2012 +0200
@@ -5,5 +5,6 @@
* CocoaDialog 2.1.1 http://cocoadialog.sourceforge.net/
-* Platypus 4.0 http://www.sveinbjorn.org/platypus
+* Platypus 4.7 http://www.sveinbjorn.org/platypus
+ Preferences: Install command line tool
--- a/Admin/MacOS/App1/mk Mon Jul 23 18:52:10 2012 +0200
+++ b/Admin/MacOS/App1/mk Mon Jul 23 19:07:01 2012 +0200
@@ -4,15 +4,17 @@
THIS="$(cd "$(dirname "$0")"; pwd)"
-PLATYPUS_APP="/Applications/Platypus-4.0/Platypus.app"
COCOADIALOG_APP="/Applications/CocoaDialog.app"
-"$PLATYPUS_APP/Contents/Resources/platypus" \
+/usr/local/bin/platypus \
-a Isabelle -u Isabelle \
-I "de.tum.in.isabelle" \
-i "$THIS/../isabelle.icns" \
+ -D -X thy \
+ -Q "$THIS/../theory.icns" \
-p /bin/bash \
- -c "$THIS/script" \
+ -R \
-o None \
-f "$COCOADIALOG_APP" \
+ "$THIS/script" \
"$PWD/Isabelle.app"
--- a/Admin/init_components Mon Jul 23 18:52:10 2012 +0200
+++ b/Admin/init_components Mon Jul 23 19:07:01 2012 +0200
@@ -5,22 +5,11 @@
# init_components - bash source script to initialize components
# as specified in the Admin directory
-function init_component_liberal
-{
- local LOCATION="$1"
- if [[ -d "${LOCATION}" ]]
- then
- init_component "${LOCATION}"
- else
- echo "Warning: no component found in ${LOCATION}" >&2
- fi
-}
-
-while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
+while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
do
- case "${REPLY}" in
+ case "$REPLY" in
\#* | "") ;;
- /*) init_component_liberal "${REPLY}" ;;
- *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
+ /*) init_component "$REPLY" ;;
+ *) init_component "$COMPONENT/$REPLY" ;;
esac
-done < "${ISABELLE_HOME}/Admin/components"
+done < "$ISABELLE_HOME/Admin/components"
--- a/Admin/isatest/annomaly Mon Jul 23 18:52:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,98 +0,0 @@
-#!/bin/sh
-
-# Create AnnoMaLy documentation for Isabelle
-# See http://martin.von-gagern.net/projects/annomaly/
-# 2007 Martin von Gagern (martin@von-gagern.net)
-
-# Abort on any error
-set -e -o pipefail
-
-BUILD_DIR="$HOME/isabelle.annomaly"
-ISABELLE_HOME="$BUILD_DIR/Isabelle"
-ISABELLE_CVS="$HOME/isabelle.cvs"
-ADMIN_CVS="$ISABELLE_CVS/Admin"
-# ISABELLE_HOME="$ISABELLE_CVS/Distribution"
-ISABELLE_SRC="$ISABELLE_HOME/src"
-HTML_DIR="$HOME/html-data/isabelle-doc"
-export CVS_RSH=ssh
-export SMLNJ_HOME="$HOME/annomaly"
-export PATH="$SMLNJ_HOME/bin:$PATH"
-export SML_DOC_DIR="$HTML_DIR.tmp"
-# export SML_DOC_DEBUG="all"
-TARGET=HOL
-CVSUP=true
-
-# Parse command line
-for ARG in "$@"; do case "$ARG" in
- -p) TARGET=Pure ;;
- -n) CVSUP=false ;;
- -l) export SML_LOG_DIR="$HOME/logs" ;;
-esac; done
-
-# Update CVS
-cd "$ADMIN_CVS"
-if $CVSUP; then
- echo "Updating CVS"
- cvs -q up -d
-fi
-
-# Find nightly isabelle tarball
-ISABELLE_TAR=""
-for i in /home/html/isatest/Isabelle_[0-9]*-20[0-9][0-9].tar.gz; do
- if [[ -r "$i" ]]; then ISABELLE_TAR="$i"; fi
-done
-if [[ -z $ISABELLE_TAR ]]; then
- echo "No isabelle tarball found!" >&2
- exit 1
-fi
-
-# Create build environemnt
-mkdir -p "$BUILD_DIR"
-cd "$BUILD_DIR"
-if [[ -d Isabelle ]]; then
- rm -rf *
-fi
-tar xzf "$ISABELLE_TAR"
-cd "$ISABELLE_HOME"
-cp "$ADMIN_CVS"/isatest/annomaly.ML src/Pure/ML-Systems/annomaly.ML
-ln -s run-smlnj lib/scripts/run-annomaly
-
-# Create clean output directory
-rm -rf "$SML_DOC_DIR"
-mkdir "$SML_DOC_DIR"
-cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
-cat > "$SML_DOC_DIR/.htaccess" <<EOF
-DirectoryIndex index.html source.html
-<IfModule mod_deflate>
-SetOutputFilter DEFLATE
-</IfModule>
-AddType text/plain .dot
-EOF
-
-# Build isabelle
-ISABELLE_HOME="$(cd "$ISABELLE_HOME"; pwd -P)"
-cd "$ISABELLE_HOME"
-export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
-rm -rf heaps
-./build -b $TARGET
-cd "$BUILD_DIR"
-rm -rf *
-
-# Postprocess created files
-cd $SML_DOC_DIR
-dot -Tsvg depGraph.dot \
- | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
- > depGraph.svg
-dot -Tps2 depGraph.dot > depGraph.ps
-ps2pdf depGraph.ps depGraph.pdf
-grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
-
-# Install result by renaming, to be almost atomic
-rm -rf "$HTML_DIR.bac"
-if [[ -d $HTML_DIR ]]; then mv "$HTML_DIR" "$HTML_DIR.bac"; fi
-mv "$SML_DOC_DIR" "$HTML_DIR"
-rm -rf "$HTML_DIR.bac"
-
-# Done
-echo "Completed successfully"
-exit 0
--- a/Admin/isatest/annomaly.ML Mon Jul 23 18:52:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(* Title: Admin/isatest/annomaly.ML
- Author: Martin von Gagern <martin@von-gagern.net>
-*)
-
-use "ML-Systems/smlnj.ML";
-
-local
-
- val smlnj_use_text = use_text
-
- val smlnj_use_file = use_file
-
- val smlnj_forget_structure = forget_structure
-
- fun mkAbsolute path =
- OS.Path.mkAbsolute { path = path, relativeTo = OS.FileSys.getDir () }
-
- fun toArcs path = #arcs (OS.Path.fromString path)
-
- val isabelleHome =
- case OS.Process.getEnv "ISABELLE_HOME"
- of NONE => OS.FileSys.getDir ()
- | SOME home => mkAbsolute home
-
- fun noparent [] = []
- | noparent (n :: ns) =
- if n = OS.Path.parentArc then noparent ns else n :: noparent ns
-
- fun isabellePath [] = []
- | isabellePath ("src" :: name) = "Isabelle" :: name
- | isabellePath (name as (n :: ns)) =
- if n = OS.Path.parentArc then noparent ns else "Isabelle" :: name
-
- fun rewrite defPrefix name =
- let val abs = mkAbsolute name
- val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
- val exists = (OS.FileSys.access(abs, nil)
- handle OS.SysErr _ => false)
- in if exists andalso rel <> ""
- then isabellePath (toArcs rel)
- else defPrefix @ noparent (toArcs name)
- end handle OS.Path.Path => defPrefix @ noparent (toArcs name)
-
-in
-
- fun use_text tune str_of_pos name_space (line, name) p v t =
- let val name = case name of "" => "unnamed" | name => name
- val arcs = rewrite ["use_text"] name
- (* should we have different files for different line numbers? *
- val arcs = if line <= 1 then arcs
- else arcs @ [ "l." ^ Int.toString line ]
- *)
- val arcs = if t = "structure Isabelle =\nstruct\nend;"
- andalso name = "ML"
- then ["empty_Isabelle", "empty" ] else arcs
- val _ = AnnoMaLy.nameNextStream arcs
- in smlnj_use_text tune str_of_pos name_space (line, name) p v t end;
-
- fun use_file tune str_of_pos name_space output verbose name =
- let val arcs = rewrite ["use_file"] name
- val _ = AnnoMaLy.nameNextStream arcs
- in smlnj_use_file tune str_of_pos name_space output verbose name end;
-
- fun forget_structure name =
- let val arcs = [ "forget_structure", name ]
- val _ = AnnoMaLy.nameNextStream arcs
- in smlnj_forget_structure name end;
-
-end;
--- a/Admin/isatest/isatest-annomaly Mon Jul 23 18:52:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-#!/usr/bin/env bash
-#
-# Create AnnoMaLy documentation for Isabelle
-#
-# Based on http://martin.von-gagern.net/projects/annomaly/
-# 2007 Martin von Gagern (martin@von-gagern.net)
-
-## global settings
-. ~/admin/isatest/isatest-settings
-
-PRG="$(basename "$0")"
-
-export SMLNJ_HOME="/home/gagern/annomaly"
-export SML_DOC_DIR="$HOME/anno-html"
-
-ADMIN="$HOME/admin/isatest"
-LOGICS="HOL"
-
-# Abort on any error
-set -e -o pipefail
-
-function usage()
-{
- echo
- echo "Usage: $PRG"
- echo
- echo " Generate html documentation from .ML files"
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- log "FAILED, $1"
- exit 2
-}
-
-
-## main
-
-ISABELLE_HOME="$DISTPREFIX/Isabelle"
-ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
-
-[ -d $ISABELLE_HOME ] || fail "$ISABELLE_HOME is not a directory."
-
-
-# Create clean output directory
-rm -rf "$SML_DOC_DIR"
-mkdir "$SML_DOC_DIR"
-cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
-cat > "$SML_DOC_DIR/.htaccess" <<EOF
-DirectoryIndex index.html source.html
-<IfModule mod_deflate>
-SetOutputFilter DEFLATE
-</IfModule>
-AddType text/plain .dot
-EOF
-
-# Prepare build environemnt
-cd "$ISABELLE_HOME"
-cp "$ADMIN/annomaly.ML" src/Pure/ML-Systems/annomaly.ML
-ln -fs run-smlnj lib/scripts/run-annomaly
-
-cd "$ISABELLE_HOME"
-export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
-
-
-# Process image(s)
-for L in $LOGICS
-do
- ( cd "$ISABELLE_HOME/src/$L"; \
- cat ~/settings/annomaly >> $ISABELLE_HOME/etc/settings; \
- "$ISABELLE_TOOL" make || fail "isabelle make for $L failed." )
-done
-
-
-# Postprocess created files
-cd "$SML_DOC_DIR"
-dot -Tsvg depGraph.dot \
- | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
- > depGraph.svg
-dot -Tps2 depGraph.dot > depGraph.ps
-ps2pdf depGraph.ps depGraph.pdf
-
-# $ISABELLE_HOME does not seem to occur anywhere ??
-# grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
-
-
-log "annomaly docs generated successfully."
--- a/Admin/isatest/settings/annomaly Mon Jul 23 18:52:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-ML_SYSTEM=annomaly
-ML_HOME="$SMLNJ_HOME/bin"
-ML_OPTIONS="-m $SMLNJ_HOME/annomaly/annomaly.cm @SMLdebug=/dev/null"
-ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-
-
-ISABELLE_HOME_USER="$HOME/isabelle-annomaly"
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
-
--- a/Admin/mira.py Mon Jul 23 18:52:10 2012 +0200
+++ b/Admin/mira.py Mon Jul 23 19:07:01 2012 +0200
@@ -492,8 +492,8 @@
smlnj_settings = '''
ML_SYSTEM=smlnj
-ML_HOME="/home/smlnj/110.72/bin"
-ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
+ML_HOME="/home/smlnj/110.74/bin"
+ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
'''
--- a/etc/settings Mon Jul 23 18:52:10 2012 +0200
+++ b/etc/settings Mon Jul 23 19:07:01 2012 +0200
@@ -45,7 +45,7 @@
# Standard ML of New Jersey (slow!)
#ML_SYSTEM=smlnj-110
#ML_HOME="/usr/local/smlnj/bin"
-#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
+#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
#SMLNJ_CYGWIN_RUNTIME=1
@@ -93,7 +93,11 @@
###
# The place for user configuration, heap files, etc.
-ISABELLE_HOME_USER="$USER_HOME/.isabelle/${ISABELLE_IDENTIFIER:-.}"
+if [ -z "ISABELLE_IDENTIFIER" ]; then
+ ISABELLE_HOME_USER="$USER_HOME/.isabelle"
+else
+ ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER"
+fi
# Where to look for isabelle tools (multiple dirs separated by ':').
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
--- a/lib/Tools/build Mon Jul 23 18:52:10 2012 +0200
+++ b/lib/Tools/build Mon Jul 23 19:07:01 2012 +0200
@@ -21,6 +21,7 @@
echo " -j INT maximum number of jobs (default 1)"
echo " -l list sessions only"
echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)"
+ echo " -s system build mode: produce output in ISABELLE_HOME"
echo " -v verbose"
echo
echo " Build and manage Isabelle sessions, depending on implicit"
@@ -52,12 +53,13 @@
BUILD_IMAGES=false
MAX_JOBS=1
LIST_ONLY=false
+SYSTEM_MODE=false
VERBOSE=false
declare -a MORE_DIRS=()
eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
-while getopts "abd:j:lo:v" OPT
+while getopts "abd:j:lo:sv" OPT
do
case "$OPT" in
a)
@@ -79,6 +81,9 @@
o)
BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
;;
+ s)
+ SYSTEM_MODE="true"
+ ;;
v)
VERBOSE="true"
;;
@@ -96,5 +101,5 @@
[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
exec "$ISABELLE_TOOL" java isabelle.Build \
- "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$VERBOSE" \
+ "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$SYSTEM_MODE" "$VERBOSE" \
"${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
--- a/lib/Tools/usedir Mon Jul 23 18:52:10 2012 +0200
+++ b/lib/Tools/usedir Mon Jul 23 19:07:01 2012 +0200
@@ -241,7 +241,7 @@
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
- -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;" \
+ -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;" \
-q -w $LOGIC $NAME > "$LOG"
RC="$?"
else
@@ -250,7 +250,7 @@
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
- -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();" \
+ -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();" \
-r -q "$LOGIC" > "$LOG"
RC="$?"
cd ..
--- a/lib/scripts/getsettings Mon Jul 23 18:52:10 2012 +0200
+++ b/lib/scripts/getsettings Mon Jul 23 19:07:01 2012 +0200
@@ -163,8 +163,7 @@
esac
if [ ! -d "$COMPONENT" ]; then
- echo >&2 "Missing Isabelle component directory: \"$COMPONENT\""
- exit 2
+ echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
elif [ -z "$ISABELLE_COMPONENTS" ]; then
ISABELLE_COMPONENTS="$COMPONENT"
else
--- a/src/HOL/TPTP/MaSh_Export.thy Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy Mon Jul 23 19:07:01 2012 +0200
@@ -11,7 +11,7 @@
sledgehammer_params
[provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
- lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
+ lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize]
ML {*
open MaSh_Export
@@ -66,5 +66,4 @@
()
*}
-
end
--- a/src/HOL/TPTP/atp_theory_export.ML Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Mon Jul 23 19:07:01 2012 +0200
@@ -113,10 +113,6 @@
handle TYPE _ => @{prop True}
end
-fun all_non_tautological_facts_of thy css_table =
- Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
- |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd)
-
fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
let
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
@@ -126,7 +122,8 @@
val mono = not (is_type_enc_polymorphic type_enc)
val path = file_name |> Path.explode
val _ = File.write path ""
- val facts = all_non_tautological_facts_of thy css_table
+ val facts =
+ Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
val atp_problem =
facts
|> map (fn ((_, loc), th) =>
--- a/src/HOL/TPTP/mash_eval.ML Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Mon Jul 23 19:07:01 2012 +0200
@@ -26,9 +26,7 @@
val max_facts_slack = 2
-val all_names =
- filter_out is_likely_tautology_or_too_meta
- #> map (rpair () o nickname_of) #> Symtab.make
+val all_names = map (rpair () o nickname_of) #> Symtab.make
fun evaluate_mash_suggestions ctxt params thy file_name =
let
--- a/src/HOL/TPTP/mash_export.ML Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Mon Jul 23 19:07:01 2012 +0200
@@ -49,9 +49,7 @@
val thy_name_of_fact = hd o Long_Name.explode
fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact
-val all_names =
- filter_out is_likely_tautology_or_too_meta
- #> map (rpair () o nickname_of) #> Symtab.make
+val all_names = map (rpair () o nickname_of) #> Symtab.make
fun generate_accessibility thy include_thy file_name =
let
--- a/src/HOL/Tools/ATP/atp_problem.ML Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Mon Jul 23 19:07:01 2012 +0200
@@ -88,11 +88,13 @@
val isabelle_info : string -> int -> (string, 'a) ho_term list
val extract_isabelle_status : (string, 'a) ho_term list -> string option
val extract_isabelle_rank : (string, 'a) ho_term list -> int
+ val inductionN : string
val introN : string
val inductiveN : string
val elimN : string
val simpN : string
- val defN : string
+ val non_rec_defN : string
+ val rec_defN : string
val rankN : string
val minimum_rank : int
val default_rank : int
@@ -222,11 +224,14 @@
val isabelle_info_prefix = "isabelle_"
+val inductionN = "induction"
val introN = "intro"
val inductiveN = "inductive"
val elimN = "elim"
val simpN = "simp"
-val defN = "def"
+val non_rec_defN = "non_rec_def"
+val rec_defN = "rec_def"
+
val rankN = "rank"
val minimum_rank = 0
@@ -503,9 +508,13 @@
fun suffix_tag top_level s =
if top_level then
case extract_isabelle_status info of
- SOME s' => if s' = defN then s ^ ":lt"
- else if s' = simpN andalso gen_simp then s ^ ":lr"
- else s
+ SOME s' =>
+ if s' = non_rec_defN then
+ s ^ ":lt"
+ else if (s' = simpN orelse s' = rec_defN) andalso gen_simp then
+ s ^ ":lr"
+ else
+ s
| NONE => s
else
s
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jul 23 19:07:01 2012 +0200
@@ -18,7 +18,9 @@
datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
datatype scope = Global | Local | Assum | Chained
- datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
+ datatype status =
+ General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def |
+ Rec_Def
type stature = scope * status
datatype strictness = Strict | Non_Strict
@@ -103,6 +105,7 @@
val helper_table : ((string * bool) * (status * thm) list) list
val trans_lams_from_string :
Proof.context -> type_enc -> string -> term list -> term list * term list
+ val string_of_status : status -> string
val factsN : string
val prepare_atp_problem :
Proof.context -> atp_format -> formula_role -> type_enc -> mode -> string
@@ -123,7 +126,8 @@
datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
datatype scope = Global | Local | Assum | Chained
-datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
+datatype status =
+ General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
type stature = scope * status
datatype order =
@@ -1236,7 +1240,8 @@
|>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts
val lam_facts =
map2 (fn t => fn j =>
- ((lam_fact_prefix ^ Int.toString j, (Global, Def)), (Axiom, t)))
+ ((lam_fact_prefix ^ Int.toString j,
+ (Global, Non_Rec_Def)), (Axiom, t)))
lambda_ts (1 upto length lambda_ts)
in (facts, lam_facts) end
@@ -1293,7 +1298,7 @@
((name, stature as (_, status)), t) =
let
val role =
- if is_format_with_defs format andalso status = Def andalso
+ if is_format_with_defs format andalso status = Non_Rec_Def andalso
is_legitimate_tptp_def t then
Definition
else
@@ -1664,18 +1669,18 @@
(* The Boolean indicates that a fairly sound type encoding is needed. *)
val base_helper_table =
- [(("COMBI", false), [(Def, @{thm Meson.COMBI_def})]),
- (("COMBK", false), [(Def, @{thm Meson.COMBK_def})]),
- (("COMBB", false), [(Def, @{thm Meson.COMBB_def})]),
- (("COMBC", false), [(Def, @{thm Meson.COMBC_def})]),
- (("COMBS", false), [(Def, @{thm Meson.COMBS_def})]),
+ [(("COMBI", false), [(Non_Rec_Def, @{thm Meson.COMBI_def})]),
+ (("COMBK", false), [(Non_Rec_Def, @{thm Meson.COMBK_def})]),
+ (("COMBB", false), [(Non_Rec_Def, @{thm Meson.COMBB_def})]),
+ (("COMBC", false), [(Non_Rec_Def, @{thm Meson.COMBC_def})]),
+ (("COMBS", false), [(Non_Rec_Def, @{thm Meson.COMBS_def})]),
((predicator_name, false), [(General, not_ffalse), (General, ftrue)]),
(("fFalse", false), [(General, not_ffalse)]),
(("fFalse", true), [(General, @{thm True_or_False})]),
(("fTrue", false), [(General, ftrue)]),
(("fTrue", true), [(General, @{thm True_or_False})]),
(("If", true),
- [(Def, @{thm if_True}), (Def, @{thm if_False}),
+ [(Non_Rec_Def, @{thm if_True}), (Non_Rec_Def, @{thm if_False}),
(General, @{thm True_or_False})])]
val helper_table =
@@ -1683,7 +1688,7 @@
[(("fNot", false),
@{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
- |> map (pair Def)),
+ |> map (pair Non_Rec_Def)),
(("fconj", false),
@{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
by (unfold fconj_def) fast+}
@@ -1718,19 +1723,19 @@
((app_op_name, true),
[(General, @{lemma "EX x. ~ f x = g x | f = g" by blast})]),
(("fconj", false),
- @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Def)),
+ @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
(("fdisj", false),
- @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Def)),
+ @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
(("fimplies", false),
@{thms fimplies_table fconj_laws fdisj_laws fimplies_laws}
- |> map (pair Def)),
+ |> map (pair Non_Rec_Def)),
(("fequal", false),
- (@{thms fequal_table} |> map (pair Def)) @
+ (@{thms fequal_table} |> map (pair Non_Rec_Def)) @
(@{thms fequal_laws} |> map (pair General))),
(("fAll", false),
- @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Def)),
+ @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def)),
(("fEx", false),
- @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
+ @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def))]
|> map (apsnd (map (apsnd zero_var_indexes)))
fun bound_tvars type_enc sorts Ts =
@@ -2104,28 +2109,29 @@
| do_formula pos (AAtom tm) = AAtom (do_term pos tm)
in do_formula end
+fun string_of_status General = ""
+ | string_of_status Induction = inductionN
+ | string_of_status Intro = introN
+ | string_of_status Inductive = inductiveN
+ | string_of_status Elim = elimN
+ | string_of_status Simp = simpN
+ | string_of_status Non_Rec_Def = non_rec_defN
+ | string_of_status Rec_Def = rec_defN
+
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
of monomorphization). The TPTP explicitly forbids name clashes, and some of
the remote provers might care. *)
fun line_for_fact ctxt prefix encode freshen pos mono type_enc rank
- (j, {name, stature, role, iformula, atomic_types}) =
- (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, role,
- iformula
- |> formula_from_iformula ctxt mono type_enc should_guard_var_in_formula
- (if pos then SOME true else NONE)
- |> close_formula_universally
- |> bound_tvars type_enc true atomic_types,
- NONE,
- let val rank = rank j in
- case snd stature of
- Intro => isabelle_info introN rank
- | Inductive => isabelle_info inductiveN rank
- | Elim => isabelle_info elimN rank
- | Simp => isabelle_info simpN rank
- | Def => isabelle_info defN rank
- | _ => isabelle_info "" rank
- end)
- |> Formula
+ (j, {name, stature = (_, status), role, iformula, atomic_types}) =
+ Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
+ encode name,
+ role,
+ iformula
+ |> formula_from_iformula ctxt mono type_enc
+ should_guard_var_in_formula (if pos then SOME true else NONE)
+ |> close_formula_universally
+ |> bound_tvars type_enc true atomic_types,
+ NONE, isabelle_info (string_of_status status) (rank j))
fun lines_for_subclass type_enc sub super =
Formula (subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, Axiom,
@@ -2355,7 +2361,7 @@
Axiom,
eq_formula type_enc (atomic_types_of T) [] false
(tag_with_type ctxt mono type_enc NONE T x_var) x_var,
- NONE, isabelle_info defN helper_rank)
+ NONE, isabelle_info non_rec_defN helper_rank)
end
fun lines_for_mono_types ctxt mono type_enc Ts =
@@ -2438,7 +2444,7 @@
val tag_with = tag_with_type ctxt mono type_enc NONE
fun formula c =
[Formula (ident, role, eq (tag_with res_T c) c, NONE, isabelle_info
- defN helper_rank)]
+ non_rec_defN helper_rank)]
in
if pred_sym orelse not (should_encode_type ctxt mono level res_T) then
[]
@@ -2538,7 +2544,7 @@
in
([tm1, tm2],
[Formula (uncurried_alias_eq_prefix ^ s2, role, eq |> maybe_negate,
- NONE, isabelle_info defN helper_rank)])
+ NONE, isabelle_info non_rec_defN helper_rank)])
|> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
else pair_append (do_alias (ary - 1)))
end
@@ -2878,8 +2884,9 @@
fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
val graph =
Graph.empty
- |> fold (fold (add_eq_deps (has_status defN)) o snd) problem
- |> fold (fold (add_eq_deps (has_status simpN orf is_conj)) o snd) problem
+ |> fold (fold (add_eq_deps (has_status non_rec_defN)) o snd) problem
+ |> fold (fold (add_eq_deps (has_status rec_defN orf has_status simpN
+ orf is_conj)) o snd) problem
|> fold (fold (add_intro_deps (has_status inductiveN)) o snd) problem
|> fold (fold (add_intro_deps (has_status introN)) o snd) problem
fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jul 23 19:07:01 2012 +0200
@@ -200,10 +200,11 @@
else
isa_ext
-fun add_all_defs fact_names accum =
+fun add_non_rec_defs fact_names accum =
Vector.foldl
(fn (facts, facts') =>
- union (op =) (filter (fn (_, (_, status)) => status = Def) facts)
+ union (op =)
+ (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts)
facts')
accum fact_names
@@ -214,12 +215,12 @@
(* LEO 1.3.3 does not record definitions properly, leading to missing
dependencies in the TSTP proof. Remove the next line once this is
fixed. *)
- add_all_defs fact_names
+ add_non_rec_defs fact_names
else if rule = satallax_unsat_coreN then
(fn [] =>
(* Satallax doesn't include definitions in its unsatisfiable cores,
so we assume the worst and include them all here. *)
- [(ext_name ctxt, (Global, General))] |> add_all_defs fact_names
+ [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
| facts => facts)
else
I)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jul 23 19:07:01 2012 +0200
@@ -23,7 +23,6 @@
val fact_from_ref :
Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
-> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
- val is_likely_tautology_or_too_meta : thm -> bool
val backquote_thm : thm -> string
val clasimpset_rule_table_of : Proof.context -> status Termtab.table
val maybe_instantiate_inducts :
@@ -50,8 +49,6 @@
del : (Facts.ref * Attrib.src list) list,
only : bool}
-val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
-
(* experimental features *)
val ignore_no_atp =
Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
@@ -147,10 +144,11 @@
fun multi_base_blacklist ctxt ho_atp =
["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
"cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
- "weak_case_cong"]
+ "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps",
+ "nibble.distinct"]
|> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
append ["induct", "inducts"]
- |> map (prefix ".")
+ |> map (prefix Long_Name.separator)
val max_lambda_nesting = 3 (*only applies if not ho_atp*)
@@ -162,12 +160,11 @@
(* Don't count nested lambdas at the level of formulas, since they are
quantifiers. *)
-fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
- | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
- formula_has_too_many_lambdas false (T :: Ts) t
- | formula_has_too_many_lambdas _ Ts t =
+fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
+ formula_has_too_many_lambdas (T :: Ts) t
+ | formula_has_too_many_lambdas Ts t =
if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
- exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t))
+ exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
else
term_has_too_many_lambdas max_lambda_nesting t
@@ -180,11 +177,17 @@
| apply_depth _ = 0
fun is_formula_too_complex ho_atp t =
- apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
+ apply_depth t > max_apply_depth orelse
+ (not ho_atp andalso formula_has_too_many_lambdas [] t)
-(* FIXME: Extend to "Meson" and "Metis" *)
+(* These theories contain auxiliary facts that could positively confuse
+ Sledgehammer if they were included. *)
+val sledgehammer_prefixes =
+ ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator)
+
val exists_sledgehammer_const =
- exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
+ exists_Const (fn (s, _) =>
+ exists (fn pref => String.isPrefix pref s) sledgehammer_prefixes)
(* FIXME: make more reliable *)
val exists_low_level_class_const =
@@ -192,25 +195,11 @@
s = @{const_name equal_class.equal} orelse
String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
-fun is_metastrange_theorem th =
- case head_of (concl_of th) of
- Const (s, _) => (s <> @{const_name Trueprop} andalso
- s <> @{const_name "=="})
- | _ => false
-
fun is_that_fact th =
String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
| _ => false) (prop_of th)
-fun is_theorem_bad_for_atps ho_atp thm =
- is_metastrange_theorem thm orelse
- let val t = prop_of thm in
- is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
- exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
- is_that_fact thm
- end
-
fun is_likely_tautology_or_too_meta th =
let
val is_boring_const = member (op =) atp_widely_irrelevant_consts
@@ -229,6 +218,15 @@
is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
end
+fun is_theorem_bad_for_atps ho_atp th =
+ is_likely_tautology_or_too_meta th orelse
+ let val t = prop_of th in
+ is_formula_too_complex ho_atp t orelse
+ exists_type type_has_top_sort t orelse
+ exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
+ is_that_fact th
+ end
+
fun hackish_string_for_term thy t =
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
(print_mode_value ())) (Syntax.string_of_term_global thy) t
@@ -299,8 +297,8 @@
|> maps (snd o snd)
in
Termtab.empty |> add Simp [atomize] snd simps
- |> add Simp [] I rec_defs
- |> add Def [] I nonrec_defs
+ |> add Rec_Def [] I rec_defs
+ |> add Non_Rec_Def [] I nonrec_defs
(* Add once it is used:
|> add Elim [] I elims
*)
@@ -458,7 +456,6 @@
else
let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
all_facts ctxt ho_atp reserved add chained css
- |> filter_out (is_likely_tautology_or_too_meta o snd)
|> filter_out (member Thm.eq_thm_prop del o snd)
|> maybe_filter_no_atps ctxt
|> uniquify
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jul 23 19:07:01 2012 +0200
@@ -29,7 +29,7 @@
open Sledgehammer_MaSh
open Sledgehammer_Run
-val cvc3N = "cvc3"
+(* val cvc3N = "cvc3" *)
val yicesN = "yices"
val z3N = "z3"
@@ -226,7 +226,7 @@
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
timeout, it makes sense to put E first. *)
fun default_provers_param_value ctxt =
- [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN, cvc3N]
+ [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN]
|> map_filter (remotify_prover_if_not_installed ctxt)
|> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
max_default_remote_threads)
@@ -404,11 +404,11 @@
else
();
mash_learn ctxt (get_params Normal ctxt
- (("timeout",
- [string_of_real default_learn_atp_timeout]) ::
+ ([("timeout",
+ [string_of_real default_learn_atp_timeout]),
+ ("slice", ["false"])] @
override_params @
- [("slice", ["false"]),
- ("minimize", ["true"]),
+ [("minimize", ["true"]),
("preplay_timeout", ["0"])]))
fact_override (#facts (Proof.goal state))
(subcommand = learn_atpN orelse subcommand = relearn_atpN))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jul 23 19:07:01 2012 +0200
@@ -59,7 +59,7 @@
val mash_can_suggest_facts : Proof.context -> bool
val mash_suggested_facts :
Proof.context -> params -> string -> int -> term list -> term
- -> ('a * thm) list -> (('a * thm) * real) list * ('a * thm) list
+ -> fact list -> (fact * real) list * fact list
val mash_learn_proof :
Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
-> unit
@@ -106,7 +106,7 @@
getenv "ISABELLE_HOME_USER" ^ "/mash"
|> tap (Isabelle_System.mkdir o Path.explode)
val mash_state_dir = mash_model_dir
-fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
+fun mash_state_file () = mash_state_dir () ^ "/state"
(*** Isabelle helpers ***)
@@ -312,25 +312,44 @@
|> forall is_lambda_free ts ? cons "no_lams"
|> forall (not o exists_Const is_exists) ts ? cons "no_skos"
|> scope <> Global ? cons "local"
- |> (case status of
- General => I
- | Induction => cons "induction"
- | Intro => cons "intro"
- | Inductive => cons "inductive"
- | Elim => cons "elim"
- | Simp => cons "simp"
- | Def => cons "def")
+ |> (case string_of_status status of "" => I | s => cons s)
(* Too many dependencies is a sign that a decision procedure is at work. There
isn't much too learn from such proofs. *)
-val max_dependencies = 10
+val max_dependencies = 20
val atp_dependency_default_max_fact = 50
-fun trim_dependencies deps =
- if length deps <= max_dependencies then SOME deps else NONE
+(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
+val typedef_deps = [@{thm CollectI} |> nickname_of]
+
+(* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *)
+val typedef_ths =
+ @{thms type_definition.Abs_inverse type_definition.Rep_inverse
+ type_definition.Rep type_definition.Rep_inject
+ type_definition.Abs_inject type_definition.Rep_cases
+ type_definition.Abs_cases type_definition.Rep_induct
+ type_definition.Abs_induct type_definition.Rep_range
+ type_definition.Abs_image}
+ |> map nickname_of
-fun isar_dependencies_of all_names =
- thms_in_proof (SOME all_names) #> trim_dependencies
+fun is_size_def [dep] th =
+ (case first_field ".recs" dep of
+ SOME (pref, _) =>
+ (case first_field ".size" (nickname_of th) of
+ SOME (pref', _) => pref = pref'
+ | NONE => false)
+ | NONE => false)
+ | is_size_def _ _ = false
+
+fun trim_dependencies th deps =
+ if length deps > max_dependencies orelse deps = typedef_deps orelse
+ exists (member (op =) typedef_ths) deps orelse is_size_def deps th then
+ NONE
+ else
+ SOME deps
+
+fun isar_dependencies_of all_names th =
+ th |> thms_in_proof (SOME all_names) |> trim_dependencies th
fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
auto_level facts all_names th =
@@ -376,7 +395,7 @@
end
else
();
- used_facts |> map fst |> trim_dependencies)
+ used_facts |> map fst |> trim_dependencies th)
| _ => NONE
end
@@ -385,11 +404,11 @@
(* more friendly than "try o File.rm" for those who keep the files open in their
text editor *)
-fun wipe_out file = File.write file ""
+fun wipe_out_file file = File.write (Path.explode file) ""
-fun write_file (xs, f) file =
+fun write_file heading (xs, f) file =
let val path = Path.explode file in
- wipe_out path;
+ File.write path heading;
xs |> chunk_list 500
|> List.app (File.append path o space_implode "" o map f)
end
@@ -411,8 +430,8 @@
mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^
" --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file
in
- write_file ([], K "") sugg_file;
- write_file write_cmds cmd_file;
+ write_file "" ([], K "") sugg_file;
+ write_file "" write_cmds cmd_file;
trace_msg ctxt (fn () => "Running " ^ command);
Isabelle_System.bash command;
read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these)
@@ -422,8 +441,7 @@
| SOME "" => "Done"
| SOME s => "Error: " ^ elide_string 1000 s))
|> not overlord
- ? tap (fn _ => List.app (wipe_out o Path.explode)
- [err_file, sugg_file, cmd_file])
+ ? tap (fn _ => List.app wipe_out_file [err_file, sugg_file, cmd_file])
end
fun str_of_add (name, parents, feats, deps) =
@@ -506,7 +524,7 @@
fun load _ (state as (true, _)) = state
| load ctxt _ =
- let val path = mash_state_path () in
+ let val path = mash_state_file () |> Path.explode in
(true,
case try File.read_lines path of
SOME (version' :: node_lines) =>
@@ -531,15 +549,13 @@
fun save ctxt {fact_G} =
let
- val path = mash_state_path ()
- fun fact_line_for name parents =
- escape_meta name ^ ": " ^ escape_metas parents
- val append_fact = File.append path o suffix "\n" oo fact_line_for
- fun append_entry (name, ((), (parents, _))) () =
- append_fact name (Graph.Keys.dest parents)
+ fun str_of_entry (name, parents) =
+ escape_meta name ^ ": " ^ escape_metas parents ^ "\n"
+ fun append_entry (name, ((), (parents, _))) =
+ cons (name, Graph.Keys.dest parents)
+ val entries = [] |> Graph.fold append_entry fact_G
in
- File.write path (version ^ "\n");
- Graph.fold append_entry fact_G ();
+ write_file (version ^ "\n") (entries, str_of_entry) (mash_state_file ());
trace_msg ctxt (fn () => "Saved fact graph (" ^ graph_info fact_G ^ ")")
end
@@ -551,12 +567,17 @@
fun mash_map ctxt f =
Synchronized.change global_state (load ctxt ##> (f #> tap (save ctxt)))
+fun mash_peek ctxt f =
+ Synchronized.change_result global_state (load ctxt #> `snd #>> f)
+
fun mash_get ctxt =
Synchronized.change_result global_state (load ctxt #> `snd)
fun mash_unlearn ctxt =
Synchronized.change global_state (fn _ =>
- (mash_CLEAR ctxt; wipe_out (mash_state_path ()); (true, empty_state)))
+ (mash_CLEAR ctxt;
+ wipe_out_file (mash_state_file ());
+ (true, empty_state)))
end
@@ -598,28 +619,43 @@
(* Generate more suggestions than requested, because some might be thrown out
later for various reasons and "meshing" gives better results with some
slack. *)
-fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
+fun max_suggs_of max_facts = max_facts + Int.min (50, max_facts)
fun is_fact_in_graph fact_G (_, th) =
can (Graph.get_node fact_G) (nickname_of th)
+fun interleave 0 _ _ = []
+ | interleave n [] ys = take n ys
+ | interleave n xs [] = take n xs
+ | interleave 1 (x :: _) _ = [x]
+ | interleave n (x :: xs) (y :: ys) = x :: y :: interleave (n - 2) xs ys
+
fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
- val fact_G = #fact_G (mash_get ctxt)
- val parents = maximal_in_graph fact_G facts
- val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
- val suggs =
- if Graph.is_empty fact_G then []
- else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
- val selected =
+ val (fact_G, suggs) =
+ mash_peek ctxt (fn {fact_G} =>
+ if Graph.is_empty fact_G then
+ (fact_G, [])
+ else
+ let
+ val parents = maximal_in_graph fact_G facts
+ val feats =
+ features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
+ in
+ (fact_G, mash_QUERY ctxt overlord (max_suggs_of max_facts)
+ (parents, feats))
+ end)
+ val sels =
facts |> suggested_facts suggs
(* The weights currently returned by "mash.py" are too extreme to
make any sense. *)
- |> map fst |> weight_mepo_facts
- val unknown = facts |> filter_out (is_fact_in_graph fact_G)
- in (selected, unknown) end
+ |> map fst
+ val (unk_global, unk_local) =
+ facts |> filter_out (is_fact_in_graph fact_G)
+ |> List.partition (fn ((_, (scope, _)), _) => scope = Global)
+ in (interleave max_facts unk_local sels |> weight_mepo_facts, unk_global) end
fun add_to_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
let
@@ -638,7 +674,7 @@
val hard_timeout = time_mult learn_timeout_slack timeout
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, hard_timeout)
- val desc = ("machine learner for Sledgehammer", "")
+ val desc = ("Machine learner for Sledgehammer", "")
in Async_Manager.launch MaShN birth_time death_time desc task end
fun freshish_name () =
@@ -656,12 +692,22 @@
val name = freshish_name ()
val feats = features_of ctxt prover thy (Local, General) [t]
val deps = used_ths |> map nickname_of
- val {fact_G} = mash_get ctxt
- val parents = maximal_in_graph fact_G facts
in
- mash_ADD ctxt overlord [(name, parents, feats, deps)]; (true, "")
+ mash_peek ctxt (fn {fact_G} =>
+ let val parents = maximal_in_graph fact_G facts in
+ mash_ADD ctxt overlord [(name, parents, feats, deps)]
+ end);
+ (true, "")
end)
+val evil_theories =
+ ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick",
+ "New_DSequence", "New_Random_Sequence", "Quickcheck",
+ "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"]
+
+fun fact_has_evil_theory (_, th) =
+ member (op =) evil_theories (Context.theory_name (theory_of_thm th))
+
fun sendback sub =
Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
@@ -676,7 +722,8 @@
Time.+ (Timer.checkRealTimer timer, commit_timeout)
val {fact_G} = mash_get ctxt
val (old_facts, new_facts) =
- facts |> List.partition (is_fact_in_graph fact_G)
+ facts |> filter_out fact_has_evil_theory
+ |> List.partition (is_fact_in_graph fact_G)
||> sort (thm_ord o pairself snd)
in
if null new_facts andalso (not atp orelse null old_facts) then
@@ -691,15 +738,14 @@
else
let
val all_names =
- facts |> map snd
- |> filter_out is_likely_tautology_or_too_meta
- |> map (rpair () o nickname_of)
- |> Symtab.make
- val deps_of =
- if atp then
- atp_dependencies_of ctxt params prover auto_level facts all_names
+ facts |> map snd |> map (rpair () o nickname_of) |> Symtab.make
+ fun deps_of status th =
+ if status = Non_Rec_Def orelse status = Rec_Def then
+ SOME []
+ else if atp then
+ atp_dependencies_of ctxt params prover auto_level facts all_names th
else
- isar_dependencies_of all_names
+ isar_dependencies_of all_names th
fun do_commit [] [] state = state
| do_commit adds reps {fact_G} =
let
@@ -727,13 +773,13 @@
else
())
fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum
- | learn_new_fact ((_, stature), th)
+ | learn_new_fact ((_, stature as (_, status)), th)
(adds, (parents, n, next_commit, _)) =
let
val name = nickname_of th
val feats =
features_of ctxt prover (theory_of_thm th) stature [prop_of th]
- val deps = deps_of th |> these
+ val deps = deps_of status th |> these
val n = n |> not (null deps) ? Integer.add 1
val adds = (name, parents, feats, deps) :: adds
val (adds, next_commit) =
@@ -759,11 +805,12 @@
|> fold learn_new_fact new_facts
in commit true adds []; n end
fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
- | relearn_old_fact (_, th) (reps, (n, next_commit, _)) =
+ | relearn_old_fact ((_, (_, status)), th)
+ (reps, (n, next_commit, _)) =
let
val name = nickname_of th
val (n, reps) =
- case deps_of th of
+ case deps_of status th of
SOME deps => (n + 1, (name, deps) :: reps)
| NONE => (n, reps)
val (reps, next_commit) =
@@ -774,7 +821,7 @@
val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
in (reps, (n, next_commit, timed_out)) end
val n =
- if null old_facts then
+ if not atp orelse null old_facts then
n
else
let
--- a/src/Pure/General/file.ML Mon Jul 23 18:52:10 2012 +0200
+++ b/src/Pure/General/file.ML Mon Jul 23 19:07:01 2012 +0200
@@ -45,11 +45,7 @@
val platform_path = Path.implode o Path.expand;
-fun shell_quote s =
- if exists_string (fn c => c = "'") s then
- error ("Illegal single quote in path specification: " ^ quote s)
- else enclose "'" "'" s;
-
+val shell_quote = enclose "'" "'";
val shell_path = shell_quote o platform_path;
--- a/src/Pure/System/build.scala Mon Jul 23 18:52:10 2012 +0200
+++ b/src/Pure/System/build.scala Mon Jul 23 19:07:01 2012 +0200
@@ -340,20 +340,20 @@
def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
}
- private def start_job(save: Boolean, name: String, info: Session.Info): Job =
+ private def start_job(name: String, info: Session.Info, output: Option[String]): Job =
{
val parent = info.parent.getOrElse("")
val cwd = info.dir.file
- val env = Map("INPUT" -> parent, "TARGET" -> name)
+ val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output.getOrElse(""))
val script =
- if (is_pure(name)) "./build " + (if (save) "-b " else "") + name
+ if (is_pure(name)) "./build " + name + " \"$OUTPUT\""
else {
"""
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
""" +
- (if (save)
- """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$TARGET" """
+ (if (output.isDefined)
+ """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" """
else
""" "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
"""
@@ -372,7 +372,7 @@
{
import XML.Encode._
pair(bool, pair(string, pair(string, list(string))))(
- save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
+ output.isDefined, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
}
new Job(cwd, env, script, YXML.string_of_body(args_xml))
}
@@ -384,29 +384,31 @@
private def sleep(): Unit = Thread.sleep(500)
def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
- list_only: Boolean, verbose: Boolean,
+ list_only: Boolean, system_mode: Boolean, verbose: Boolean,
more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
{
val options = (Options.init() /: more_options)(_.define_simple(_))
val queue = find_sessions(options, all_sessions, sessions, more_dirs)
val deps = dependencies(queue)
+ val (output_dir, browser_info) =
+ if (system_mode) (Path.explode("~~/heaps/$ML_IDENTIFIER"), Path.explode("~~/browser_info"))
+ else (Path.explode("$ISABELLE_OUTPUT"), Path.explode("$ISABELLE_BROWSER_INFO"))
// prepare browser info dir
- if (options.bool("browser_info") &&
- !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
+ if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile)
{
- Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
- File.copy(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif"),
- Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif"))
- File.write(Path.explode("$ISABELLE_BROWSER_INFO/index.html"),
- File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template")) +
- File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template")) +
- File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template")))
+ browser_info.file.mkdirs()
+ File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
+ browser_info + Path.explode("isabelle.gif"))
+ File.write(browser_info + Path.explode("index.html"),
+ File.read(Path.explode("~~/lib/html/library_index_header.template")) +
+ File.read(Path.explode("~~/lib/html/library_index_content.template")) +
+ File.read(Path.explode("~~/lib/html/library_index_footer.template")))
}
// prepare log dir
- val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
+ val log_dir = output_dir + Path.explode("log")
log_dir.file.mkdirs()
// scheduler loop
@@ -447,9 +449,12 @@
loop(pending - name, running, results + (name -> 0))
}
else if (info.parent.map(results(_)).forall(_ == 0)) {
- val save = build_images || queue.is_inner(name)
- echo((if (save) "Building " else "Running ") + name + " ...")
- val job = start_job(save, name, info)
+ val output =
+ if (build_images || queue.is_inner(name))
+ Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
+ else None
+ echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
+ val job = start_job(name, info, output)
loop(pending, running + (name -> job), results)
}
else {
@@ -477,10 +482,11 @@
Properties.Value.Boolean(build_images) ::
Properties.Value.Int(max_jobs) ::
Properties.Value.Boolean(list_only) ::
+ Properties.Value.Boolean(system_mode) ::
Properties.Value.Boolean(verbose) ::
Command_Line.Chunks(more_dirs, options, sessions) =>
- build(all_sessions, build_images, max_jobs, list_only, verbose,
- more_dirs.map(Path.explode), options, sessions)
+ build(all_sessions, build_images, max_jobs, list_only, system_mode,
+ verbose, more_dirs.map(Path.explode), options, sessions)
case _ => error("Bad arguments:\n" + cat_lines(args))
}
}
--- a/src/Pure/System/session.ML Mon Jul 23 18:52:10 2012 +0200
+++ b/src/Pure/System/session.ML Mon Jul 23 19:07:01 2012 +0200
@@ -10,7 +10,7 @@
val name: unit -> string
val welcome: unit -> string
val init: bool -> string -> string -> unit
- val use_dir: string -> string -> bool -> string list -> bool -> bool ->
+ val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
string -> bool -> string list -> string -> string -> bool * string ->
string -> int -> bool -> bool -> int -> int -> int -> int -> unit
val finish: unit -> unit
@@ -94,12 +94,12 @@
fun dumping (_, "") = NONE
| dumping (cp, path) = SOME (cp, Path.explode path);
-fun use_dir item root build modes reset info doc doc_graph doc_variants parent
+fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
name dump rpath level timing verbose max_threads trace_threads
parallel_proofs parallel_proofs_threshold =
((fn () =>
(init reset parent name;
- Present.init build info doc doc_graph doc_variants (path ()) name
+ Present.init build info info_path doc doc_graph doc_variants (path ()) name
(dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
if timing then
let
--- a/src/Pure/Thy/present.ML Mon Jul 23 18:52:10 2012 +0200
+++ b/src/Pure/Thy/present.ML Mon Jul 23 19:07:01 2012 +0200
@@ -17,7 +17,7 @@
path: string, parents: string list} list -> Path.T -> unit
val display_graph: {name: string, ID: string, dir: string, unfold: bool,
path: string, parents: string list} list -> unit
- val init: bool -> bool -> string -> bool -> string list -> string list ->
+ val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
string -> (bool * Path.T) option -> Url.T option * bool -> bool ->
theory list -> unit (*not thread-safe!*)
val finish: unit -> unit (*not thread-safe!*)
@@ -34,8 +34,6 @@
(** paths **)
-val output_path = Path.variable "ISABELLE_BROWSER_INFO";
-
val tex_ext = Path.ext "tex";
val tex_path = tex_ext o Path.basic;
val html_ext = Path.ext "html";
@@ -275,7 +273,7 @@
fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
-fun init build info doc doc_graph doc_variants path name dump_prefix
+fun init build info info_path doc doc_graph doc_variants path name dump_prefix
(remote_path, first_time) verbose thys =
if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
(browser_info := empty_browser_info; session_info := NONE)
@@ -284,7 +282,7 @@
val parent_name = name_of_session (take (length path - 1) path);
val session_name = name_of_session path;
val sess_prefix = Path.make path;
- val html_prefix = Path.append (Path.expand output_path) sess_prefix;
+ val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix;
val documents =
if doc = "" then []
--- a/src/Pure/build Mon Jul 23 18:52:10 2012 +0200
+++ b/src/Pure/build Mon Jul 23 19:07:01 2012 +0200
@@ -12,12 +12,7 @@
function usage()
{
echo
- echo "Usage: $PRG [OPTIONS] TARGET"
- echo
- echo " Options are:"
- echo " -b build target images"
- echo
- echo " Build Isabelle/ML TARGET: RAW or Pure"
+ echo "Usage: $PRG TARGET OUTPUT"
echo
exit 1
}
@@ -33,32 +28,14 @@
## process command line
-# options
-
-BUILD_IMAGES=false
-
-while getopts "b" OPT
-do
- case "$OPT" in
- b)
- BUILD_IMAGES="true"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
# args
-TARGET="Pure"
-[ "$#" -ge 1 ] && { TARGET="$1"; shift; }
-[ "$TARGET" = RAW -o "$TARGET" = Pure ] || fail "Bad target: \"$TARGET\""
-
-[ "$#" -eq 0 ] || usage
+if [ "$#" -eq 2 ]; then
+ TARGET="$1"; shift
+ OUTPUT="$1"; shift
+else
+ usage
+fi
## main
@@ -79,7 +56,7 @@
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
if [ "$TARGET" = RAW ]; then
- if [ "$BUILD_IMAGES" = false ]; then
+ if [ -z "$OUTPUT" ]; then
"$ISABELLE_PROCESS" \
-e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
-q RAW_ML_SYSTEM
@@ -88,10 +65,10 @@
-e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
-e "structure Isar = struct fun main () = () end;" \
-e "ml_prompts \"ML> \" \"ML# \";" \
- -q -w RAW_ML_SYSTEM RAW
+ -q -w RAW_ML_SYSTEM "$OUTPUT"
fi
else
- if [ "$BUILD_IMAGES" = false ]; then
+ if [ -z "$OUTPUT" ]; then
"$ISABELLE_PROCESS" \
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
-q RAW_ML_SYSTEM
@@ -99,7 +76,7 @@
"$ISABELLE_PROCESS" \
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
-e "ml_prompts \"ML> \" \"ML# \";" \
- -f -q -w RAW_ML_SYSTEM Pure
+ -f -q -w RAW_ML_SYSTEM "$OUTPUT"
fi
fi