# HG changeset patch
# User krauss
# Date 1335725635 -7200
# Node ID ddc7921701c56bfed3b04209c2a1b87db8f476d7
# Parent 471cc845430b3d959c80f34bd42c37641564e910# Parent 4e247a648a01d149eae69faa6dd8c13b99435f32
merged
diff -r 471cc845430b -r ddc7921701c5 Admin/CHECKLIST
--- a/Admin/CHECKLIST Sun Apr 29 20:39:34 2012 +0200
+++ b/Admin/CHECKLIST Sun Apr 29 20:53:55 2012 +0200
@@ -37,6 +37,9 @@
- test separate compilation of Isabelle/Scala PIDE sources:
Admin/build jars_test
+- test Isabelle/jEdit:
+ print buffer
+
- test contrib components:
x86_64-linux without 32bit C/C++ libraries
Mac OS X Leopard
diff -r 471cc845430b -r ddc7921701c5 Admin/makebundle
--- a/Admin/makebundle Sun Apr 29 20:39:34 2012 +0200
+++ b/Admin/makebundle Sun Apr 29 20:53:55 2012 +0200
@@ -81,6 +81,25 @@
cd "$ISABELLE_HOME/contrib/cygwin-1.7.9"
find usr/local/polyml-*/x86-cygwin | gzip > etc/setup/polyml.lst.gz
)
+
+ for NAME in ANNOUNCE README NEWS COPYRIGHT CONTRIBUTORS contrib/README
+ do
+ FILE="$ISABELLE_HOME/$NAME"
+ {
+ echo ''
+ echo ''
+ echo ''
+ echo ''
+ echo ''
+ echo "${NAME}"
+ echo ''
+ echo ''
+ echo ''
+ perl -w -p -e "s/&/&/g; s//>/g; s/'/'/g; s/\"/"/g;" "$FILE"
+ echo '
'
+ echo ''
+ } > "${FILE}.html"
+ done
fi
diff -r 471cc845430b -r ddc7921701c5 src/HOL/Library/Target_Numeral.thy
--- a/src/HOL/Library/Target_Numeral.thy Sun Apr 29 20:39:34 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thy Sun Apr 29 20:53:55 2012 +0200
@@ -632,6 +632,10 @@
hide_const (open) of_nat Nat
+lemma [code_unfold]:
+ "Int.nat (Target_Numeral.int_of k) = Target_Numeral.nat_of k"
+ by (simp add: nat_of_def)
+
lemma int_of_nat [simp]:
"Target_Numeral.int_of (Target_Numeral.of_nat n) = of_nat n"
by (simp add: of_nat_def)
diff -r 471cc845430b -r ddc7921701c5 src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy Sun Apr 29 20:39:34 2012 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy Sun Apr 29 20:53:55 2012 +0200
@@ -27,14 +27,14 @@
by (metis_exhaust inc_def plus_1_not_0)
lemma "inc = (\y. y + 1)"
-sledgehammer [expect = some] (inc_def)
+sledgehammer [expect = some]
by (metis_exhaust inc_def)
definition add_swap :: "nat \ nat \ nat" where
"add_swap = (\x y. y + x)"
lemma "add_swap m n = n + m"
-sledgehammer [expect = some] (add_swap_def)
+sledgehammer [expect = some]
by (metis_exhaust add_swap_def)
definition "A = {xs\'a list. True}"
diff -r 471cc845430b -r ddc7921701c5 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML Sun Apr 29 20:39:34 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Sun Apr 29 20:53:55 2012 +0200
@@ -10,7 +10,8 @@
val nitpick_tptp_file : theory -> int -> string -> unit
val refute_tptp_file : theory -> int -> string -> unit
val sledgehammer_tptp_file : theory -> int -> string -> unit
- val isabelle_tptp_file : theory -> int -> string -> unit
+ val isabelle_demo_tptp_file : theory -> int -> string -> unit
+ val isabelle_comp_tptp_file : theory -> int -> string -> unit
val translate_tptp_file : string -> string -> string -> unit
end;
@@ -175,33 +176,44 @@
{add = [(Facts.named (Thm.derivation_name ext), [])],
del = [], only = true}
-fun sledgehammer_tac ctxt timeout i =
+fun sledgehammer_tac demo ctxt timeout i =
let
- fun slice overload_params fraq prover =
- SOLVE_TIMEOUT (timeout div fraq) prover
- (atp_tac ctxt overload_params (timeout div fraq) prover i)
+ val frac = if demo then 6 else 4
+ fun slice prover =
+ SOLVE_TIMEOUT (timeout div frac) prover
+ (atp_tac ctxt [] (timeout div frac) prover i)
in
- slice [] 5 ATP_Systems.satallaxN
- ORELSE slice [] 5 ATP_Systems.leo2N
- ORELSE slice [] 5 ATP_Systems.spassN
- ORELSE slice [] 5 ATP_Systems.vampireN
- ORELSE slice [] 5 ATP_Systems.eN
+ (if demo then
+ slice ATP_Systems.satallaxN
+ ORELSE slice ATP_Systems.leo2N
+ else
+ no_tac)
+ ORELSE slice ATP_Systems.spassN
+ ORELSE slice ATP_Systems.vampireN
+ ORELSE slice ATP_Systems.eN
+ ORELSE slice ATP_Systems.z3_tptpN
end
+fun smt_solver_tac solver ctxt =
+ let
+ val ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver solver)
+ in SMT_Solver.smt_tac ctxt [] end
+
fun auto_etc_tac ctxt timeout i =
SOLVE_TIMEOUT (timeout div 20) "nitpick"
(nitpick_finite_oracle_tac ctxt (timeout div 20) i)
- ORELSE SOLVE_TIMEOUT (timeout div 10) "simp"
+ ORELSE SOLVE_TIMEOUT (timeout div 20) "simp"
(asm_full_simp_tac (simpset_of ctxt) i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
(auto_tac ctxt
THEN ALLGOALS (atp_tac ctxt [] (timeout div 5) ATP_Systems.spassN))
- ORELSE SOLVE_TIMEOUT (timeout div 5) "smt" (SMT_Solver.smt_tac ctxt [] i)
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "z3" (smt_solver_tac "z3" ctxt i)
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "cvc3" (smt_solver_tac "cvc3" ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "fast" (fast_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
- ORELSE SOLVE_TIMEOUT (timeout div 20) "arith" (Arith_Data.arith_tac ctxt i)
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac ctxt [] i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i)
fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
@@ -233,22 +245,27 @@
read_tptp_file thy (freeze_problem_consts thy) file_name
val conj = make_conj assms conjs
in
- can_tac ctxt (sledgehammer_tac ctxt timeout 1) conj
+ can_tac ctxt (sledgehammer_tac true ctxt timeout 1) conj
|> print_szs_from_success conjs
end
-fun isabelle_tptp_file thy timeout file_name =
+fun isabelle_tptp_file demo thy timeout file_name =
let
val (conjs, assms, ctxt) =
read_tptp_file thy (freeze_problem_consts thy) file_name
val conj = make_conj assms conjs
+ val last_hope = if demo then ATP_Systems.satallaxN else ATP_Systems.spassN
in
(can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
- can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
- can_tac ctxt (atp_tac ctxt [] timeout ATP_Systems.satallaxN 1) conj)
+ can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
+ can_tac ctxt (atp_tac ctxt [] timeout last_hope 1) conj)
|> print_szs_from_success conjs
end
+val isabelle_demo_tptp_file = isabelle_tptp_file true
+val isabelle_comp_tptp_file = isabelle_tptp_file false
+
+
(** Translator between TPTP(-like) file formats **)
fun translate_tptp_file format in_file_name out_file_name = ()
diff -r 471cc845430b -r ddc7921701c5 src/HOL/TPTP/lib/Tools/tptp_isabelle
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle Sun Apr 29 20:39:34 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Jasmin Blanchette
-#
-# DESCRIPTION: Isabelle tactics for TPTP
-
-
-PRG="$(basename "$0")"
-
-function usage() {
- echo
- echo "Usage: isabelle $PRG TIMEOUT FILES"
- echo
- echo " Runs a combination of Isabelle tactics on TPTP problems."
- echo " Each problem is allocated at most TIMEOUT seconds."
- echo
- exit 1
-}
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
-
-TIMEOUT=$1
-shift
-
-for FILE in "$@"
-do
- echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
- > /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
-done
diff -r 471cc845430b -r ddc7921701c5 src/HOL/TPTP/lib/Tools/tptp_isabelle_comp
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_comp Sun Apr 29 20:53:55 2012 +0200
@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+#
+# Author: Jasmin Blanchette
+#
+# DESCRIPTION: Isabelle tactics for TPTP competitive division
+
+
+PRG="$(basename "$0")"
+
+function usage() {
+ echo
+ echo "Usage: isabelle $PRG TIMEOUT FILES"
+ echo
+ echo " Runs a combination of Isabelle tactics on TPTP problems."
+ echo " Each problem is allocated at most TIMEOUT seconds."
+ echo
+ exit 1
+}
+
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
+SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
+
+TIMEOUT=$1
+shift
+
+for FILE in "$@"
+do
+ echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
+ML {* ATP_Problem_Import.isabelle_comp_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
+ > /tmp/$SCRATCH.thy
+ "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
+done
diff -r 471cc845430b -r ddc7921701c5 src/HOL/TPTP/lib/Tools/tptp_isabelle_demo
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_demo Sun Apr 29 20:53:55 2012 +0200
@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+#
+# Author: Jasmin Blanchette
+#
+# DESCRIPTION: Isabelle tactics for TPTP demo division
+
+
+PRG="$(basename "$0")"
+
+function usage() {
+ echo
+ echo "Usage: isabelle $PRG TIMEOUT FILES"
+ echo
+ echo " Runs a combination of Isabelle tactics on TPTP problems."
+ echo " Each problem is allocated at most TIMEOUT seconds."
+ echo
+ exit 1
+}
+
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
+SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
+
+TIMEOUT=$1
+shift
+
+for FILE in "$@"
+do
+ echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
+ML {* ATP_Problem_Import.isabelle_demo_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
+ > /tmp/$SCRATCH.thy
+ "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
+done