--- a/NEWS Fri May 17 20:30:04 2013 +0200
+++ b/NEWS Fri May 17 20:41:45 2013 +0200
@@ -6,6 +6,12 @@
*** General ***
+* Uniform management of "quick_and_dirty" as system option (see also
+"isabelle options"), configuration option within the context (see also
+Config.get in Isabelle/ML), and attribute in Isabelle/Isar. Minor
+INCOMPATIBILITY, need to use more official Isabelle means to access
+quick_and_dirty, instead of historical poking into mutable reference.
+
* Sessions may be organized via 'chapter' specifications in the ROOT
file, which determines a two-level hierarchy of browser info. The old
tree-like organization via implicit sub-session relation, with its
--- a/src/Doc/IsarRef/Proof.thy Fri May 17 20:30:04 2013 +0200
+++ b/src/Doc/IsarRef/Proof.thy Fri May 17 20:41:45 2013 +0200
@@ -668,8 +668,8 @@
\item @{command "sorry"} is a \emph{fake proof}\index{proof!fake}
pretending to solve the pending claim without further ado. This
- only works in interactive development, or if the @{ML
- quick_and_dirty} flag is enabled (in ML). Facts emerging from fake
+ only works in interactive development, or if the @{attribute
+ quick_and_dirty} is enabled. Facts emerging from fake
proofs are not the real thing. Internally, the derivation object is
tainted by an oracle invocation, which may be inspected via the
theorem status \cite{isabelle-implementation}.
--- a/src/Doc/ProgProve/Isar.thy Fri May 17 20:30:04 2013 +0200
+++ b/src/Doc/ProgProve/Isar.thy Fri May 17 20:41:45 2013 +0200
@@ -2,7 +2,7 @@
theory Isar
imports LaTeXsugar
begin
-ML{* quick_and_dirty := true *}
+declare [[quick_and_dirty]]
(*>*)
text{*
Apply-scripts are unreadable and hard to maintain. The language of choice
--- a/src/HOL/BNF/Tools/bnf_comp.ML Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Fri May 17 20:41:45 2013 +0200
@@ -168,7 +168,7 @@
mk_comp_bd_cinfinite_tac (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer);
val set_alt_thms =
- if ! quick_and_dirty then
+ if Config.get lthy quick_and_dirty then
[]
else
map (fn goal =>
@@ -182,7 +182,7 @@
mk_comp_map_cong0_tac set_alt_thms (map_cong0_of_bnf outer) (map map_cong0_of_bnf inners);
val set_bd_tacs =
- if ! quick_and_dirty then
+ if Config.get lthy quick_and_dirty then
replicate ilive (K all_tac)
else
let
@@ -402,7 +402,7 @@
fun map_cong0_tac {context = ctxt, prems = _} =
rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
val set_map_tacs =
- if ! quick_and_dirty then
+ if Config.get lthy quick_and_dirty then
replicate (n + live) (K all_tac)
else
replicate n (K empty_natural_tac) @
@@ -410,7 +410,7 @@
fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
val set_bd_tacs =
- if ! quick_and_dirty then
+ if Config.get lthy quick_and_dirty then
replicate (n + live) (K all_tac)
else
replicate n (K (mk_lift_set_bd_tac (bd_Card_order_of_bnf bnf))) @
--- a/src/HOL/Decision_Procs/mir_tac.ML Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Fri May 17 20:41:45 2013 +0200
@@ -132,7 +132,7 @@
Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
let val pth =
(* If quick_and_dirty then run without proof generation as oracle*)
- if !quick_and_dirty
+ if Config.get ctxt quick_and_dirty
then mirfr_oracle (false, cterm_of thy (Pattern.eta_long [] t1))
else mirfr_oracle (true, cterm_of thy (Pattern.eta_long [] t1))
in
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Fri May 17 20:41:45 2013 +0200
@@ -158,7 +158,7 @@
if ($output_log) { print "Mirabelle: $thy_file\n"; }
my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
- "-e 'Unsynchronized.setmp Multithreading.max_threads 1 (Unsynchronized.setmp quick_and_dirty true use_thy) \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
+ "-o quick_and_dirty -e 'Unsynchronized.setmp Multithreading.max_threads 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
if ($output_log) {
my $outcome = ($result ? "failure" : "success");
--- a/src/HOL/Tools/Qelim/cooper.ML Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri May 17 20:41:45 2013 +0200
@@ -850,7 +850,7 @@
fun core_tac ctxt = CSUBGOAL (fn (p, i) =>
let
val cpth =
- if !quick_and_dirty
+ if Config.get ctxt quick_and_dirty
then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
else Conv.arg_conv (conv ctxt) p
val p' = Thm.rhs_of cpth
--- a/src/HOL/Tools/inductive.ML Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/Tools/inductive.ML Fri May 17 20:41:45 2013 +0200
@@ -116,7 +116,9 @@
(** misc utilities **)
fun message quiet_mode s = if quiet_mode then () else writeln s;
-fun clean_message quiet_mode s = if ! quick_and_dirty then () else message quiet_mode s;
+
+fun clean_message ctxt quiet_mode s =
+ if Config.get ctxt quick_and_dirty then () else message quiet_mode s;
fun coind_prefix true = "co"
| coind_prefix false = "";
@@ -361,7 +363,7 @@
(* prove monotonicity *)
fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
- (message (quiet_mode orelse skip_mono andalso ! quick_and_dirty)
+ (message (quiet_mode orelse skip_mono andalso Config.get ctxt quick_and_dirty)
" Proving monotonicity ...";
(if skip_mono then Goal.prove_sorry else Goal.prove_future) ctxt
[] []
@@ -379,7 +381,7 @@
fun prove_intrs quiet_mode coind mono fp_def k intr_ts rec_preds_defs ctxt ctxt' =
let
- val _ = clean_message quiet_mode " Proving the introduction rules ...";
+ val _ = clean_message ctxt quiet_mode " Proving the introduction rules ...";
val unfold = funpow k (fn th => th RS fun_cong)
(mono RS (fp_def RS
@@ -404,7 +406,7 @@
fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt ctxt''' =
let
- val _ = clean_message quiet_mode " Proving the elimination rules ...";
+ val _ = clean_message ctxt quiet_mode " Proving the elimination rules ...";
val ([pname], ctxt') = Variable.variant_fixes ["P"] ctxt;
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
@@ -453,7 +455,7 @@
fun prove_eqs quiet_mode cs params intr_ts intrs
(elims: (thm * bstring list * int) list) ctxt ctxt'' = (* FIXME ctxt'' ?? *)
let
- val _ = clean_message quiet_mode " Proving the simplification rules ...";
+ val _ = clean_message ctxt quiet_mode " Proving the simplification rules ...";
fun dest_intr r =
(the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))),
@@ -640,7 +642,7 @@
fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
fp_def rec_preds_defs ctxt ctxt''' = (* FIXME ctxt''' ?? *)
let
- val _ = clean_message quiet_mode " Proving the induction rule ...";
+ val _ = clean_message ctxt quiet_mode " Proving the induction rule ...";
(* predicates for induction rule *)
--- a/src/HOL/Tools/sat_funcs.ML Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Fri May 17 20:41:45 2013 +0200
@@ -41,8 +41,8 @@
dependent) configuration settings. To replay SAT proofs in Isabelle, you
must of course use a proof-producing SAT solver in the first place.
- Proofs are replayed only if "!quick_and_dirty" is false. If
- "!quick_and_dirty" is true, the theorem (in case the SAT solver claims its
+ Proofs are replayed only if "quick_and_dirty" is false. If
+ "quick_and_dirty" is true, the theorem (in case the SAT solver claims its
negation to be unsatisfiable) is proved via an oracle.
*)
@@ -351,7 +351,7 @@
(Inttab.dest clause_table) ^ "\n" ^
"empty clause: " ^ string_of_int empty_id)
else ();
- if !quick_and_dirty then
+ if Config.get ctxt quick_and_dirty then
make_quick_and_dirty_thm ()
else
let
@@ -378,7 +378,7 @@
Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
end)
| SatSolver.UNSATISFIABLE NONE =>
- if !quick_and_dirty then
+ if Config.get ctxt quick_and_dirty then
(warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
make_quick_and_dirty_thm ())
else
--- a/src/HOL/ex/SAT_Examples.thy Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/ex/SAT_Examples.thy Fri May 17 20:41:45 2013 +0200
@@ -11,7 +11,7 @@
(* ML {* sat.solver := "zchaff_with_proofs"; *} *)
(* ML {* sat.solver := "minisat_with_proofs"; *} *)
ML {* sat.trace_sat := true; *}
-ML {* quick_and_dirty := true; *}
+declare [[quick_and_dirty]]
lemma "True"
by sat
@@ -78,7 +78,7 @@
by sat
ML {* sat.trace_sat := false; *}
-ML {* quick_and_dirty := false; *}
+declare [[quick_and_dirty = false]]
method_setup rawsat = {*
Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac)
@@ -522,8 +522,9 @@
(* ML {*
sat.solver := "zchaff_with_proofs";
sat.trace_sat := false;
-quick_and_dirty := false;
-*} *)
+*}
+declare [[quick_and_dirty = false]]
+*)
ML {*
fun benchmark dimacsfile =
--- a/src/Pure/Isar/attrib.ML Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/Isar/attrib.ML Fri May 17 20:41:45 2013 +0200
@@ -553,7 +553,8 @@
(* theory setup *)
val _ = Context.>> (Context.map_theory
- (register_config Ast.trace_raw #>
+ (register_config quick_and_dirty_raw #>
+ register_config Ast.trace_raw #>
register_config Ast.stats_raw #>
register_config Printer.show_brackets_raw #>
register_config Printer.show_sorts_raw #>
--- a/src/Pure/Isar/method.ML Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/Isar/method.ML Fri May 17 20:41:45 2013 +0200
@@ -20,7 +20,7 @@
val SIMPLE_METHOD: tactic -> method
val SIMPLE_METHOD': (int -> tactic) -> method
val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
- val cheating: bool -> method
+ val cheating: Proof.context -> bool -> method
val intro: thm list -> method
val elim: thm list -> method
val unfold: thm list -> Proof.context -> method
@@ -127,8 +127,8 @@
(* cheating *)
-fun cheating int = METHOD (fn _ => fn st =>
- if int orelse ! quick_and_dirty then
+fun cheating ctxt int = METHOD (fn _ => fn st =>
+ if int orelse Config.get ctxt quick_and_dirty then
ALLGOALS Skip_Proof.cheat_tac st
else error "Cheating requires quick_and_dirty mode!");
@@ -296,7 +296,7 @@
val default_text = Source (Args.src (("default", []), Position.none));
val this_text = Basic (K this);
val done_text = Basic (K (SIMPLE_METHOD all_tac));
-fun sorry_text int = Basic (K (cheating int));
+fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
fun finish_text (NONE, immed) = Basic (finish immed)
| finish_text (SOME txt, immed) = Then [txt, Basic (finish immed)];
--- a/src/Pure/ROOT.ML Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/ROOT.ML Fri May 17 20:41:45 2013 +0200
@@ -6,9 +6,6 @@
val is_official = false;
end;
-(*if true then some tools will OMIT some proofs*)
-val quick_and_dirty = Unsynchronized.ref false;
-
print_depth 10;
@@ -118,6 +115,9 @@
use "context_position.ML";
use "config.ML";
+val quick_and_dirty_raw = Config.declare_option "quick_and_dirty";
+val quick_and_dirty = Config.bool quick_and_dirty_raw;
+
(* inner syntax *)
--- a/src/Pure/Tools/build.ML Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/Tools/build.ML Fri May 17 20:41:45 2013 +0200
@@ -114,7 +114,6 @@
|> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
|> Unsynchronized.setmp Future.ML_statistics true
|> no_document options ? Present.no_document
- |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
|> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
|> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
|> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
--- a/src/Pure/Tools/proof_general_pure.ML Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML Fri May 17 20:41:45 2013 +0200
@@ -131,9 +131,9 @@
(* proof *)
val _ =
- ProofGeneral.preference_bool ProofGeneral.category_proof
+ ProofGeneral.preference_option ProofGeneral.category_proof
(SOME "true")
- quick_and_dirty
+ @{option quick_and_dirty}
"quick-and-dirty"
"Take a few short cuts";
--- a/src/Pure/goal.ML Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/goal.ML Fri May 17 20:41:45 2013 +0200
@@ -337,7 +337,7 @@
Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
fun prove_sorry ctxt xs asms prop tac =
- if ! quick_and_dirty then
+ if Config.get ctxt quick_and_dirty then
prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac)
else (if future_enabled () then prove_future else prove) ctxt xs asms prop tac;
--- a/src/Tools/Code/lib/Tools/codegen Fri May 17 20:30:04 2013 +0200
+++ b/src/Tools/Code/lib/Tools/codegen Fri May 17 20:41:45 2013 +0200
@@ -55,9 +55,8 @@
handle _ => exit 1;"
ACTUAL_CMD="val thyname = \"$THYNAME\"; \
- val _ = quick_and_dirty := $QUICK_AND_DIRTY; \
val cmd_expr = \"$CODE_EXPR\"; \
val ml_cmd = \"Code_Target.codegen_tool thyname cmd_expr\"; \
$FORMAL_CMD"
-"$ISABELLE_PROCESS" -r -q -e "$ACTUAL_CMD" "$IMAGE" || exit 1
+"$ISABELLE_PROCESS" -r -q -o "quick_and_dirty=$QUICK_AND_DIRTY" -e "$ACTUAL_CMD" "$IMAGE" || exit 1