proper option quick_and_dirty;
authorwenzelm
Fri May 17 20:41:45 2013 +0200 (2013-05-17)
changeset 520592f970c7f722b
parent 52058 387dc978422b
child 52060 179236c82c2a
proper option quick_and_dirty;
NEWS
src/Doc/IsarRef/Proof.thy
src/Doc/ProgProve/Isar.thy
src/HOL/BNF/Tools/bnf_comp.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Mirabelle/lib/scripts/mirabelle.pl
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/ex/SAT_Examples.thy
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
src/Pure/ROOT.ML
src/Pure/Tools/build.ML
src/Pure/Tools/proof_general_pure.ML
src/Pure/goal.ML
src/Tools/Code/lib/Tools/codegen
     1.1 --- a/NEWS	Fri May 17 20:30:04 2013 +0200
     1.2 +++ b/NEWS	Fri May 17 20:41:45 2013 +0200
     1.3 @@ -6,6 +6,12 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Uniform management of "quick_and_dirty" as system option (see also
     1.8 +"isabelle options"), configuration option within the context (see also
     1.9 +Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor
    1.10 +INCOMPATIBILITY, need to use more official Isabelle means to access
    1.11 +quick_and_dirty, instead of historical poking into mutable reference.
    1.12 +
    1.13  * Sessions may be organized via 'chapter' specifications in the ROOT
    1.14  file, which determines a two-level hierarchy of browser info.  The old
    1.15  tree-like organization via implicit sub-session relation, with its
     2.1 --- a/src/Doc/IsarRef/Proof.thy	Fri May 17 20:30:04 2013 +0200
     2.2 +++ b/src/Doc/IsarRef/Proof.thy	Fri May 17 20:41:45 2013 +0200
     2.3 @@ -668,8 +668,8 @@
     2.4    
     2.5    \item @{command "sorry"} is a \emph{fake proof}\index{proof!fake}
     2.6    pretending to solve the pending claim without further ado.  This
     2.7 -  only works in interactive development, or if the @{ML
     2.8 -  quick_and_dirty} flag is enabled (in ML).  Facts emerging from fake
     2.9 +  only works in interactive development, or if the @{attribute
    2.10 +  quick_and_dirty} is enabled.  Facts emerging from fake
    2.11    proofs are not the real thing.  Internally, the derivation object is
    2.12    tainted by an oracle invocation, which may be inspected via the
    2.13    theorem status \cite{isabelle-implementation}.
     3.1 --- a/src/Doc/ProgProve/Isar.thy	Fri May 17 20:30:04 2013 +0200
     3.2 +++ b/src/Doc/ProgProve/Isar.thy	Fri May 17 20:41:45 2013 +0200
     3.3 @@ -2,7 +2,7 @@
     3.4  theory Isar
     3.5  imports LaTeXsugar
     3.6  begin
     3.7 -ML{* quick_and_dirty := true *}
     3.8 +declare [[quick_and_dirty]]
     3.9  (*>*)
    3.10  text{*
    3.11  Apply-scripts are unreadable and hard to maintain. The language of choice
     4.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Fri May 17 20:30:04 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Fri May 17 20:41:45 2013 +0200
     4.3 @@ -168,7 +168,7 @@
     4.4        mk_comp_bd_cinfinite_tac (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer);
     4.5  
     4.6      val set_alt_thms =
     4.7 -      if ! quick_and_dirty then
     4.8 +      if Config.get lthy quick_and_dirty then
     4.9          []
    4.10        else
    4.11          map (fn goal =>
    4.12 @@ -182,7 +182,7 @@
    4.13        mk_comp_map_cong0_tac set_alt_thms (map_cong0_of_bnf outer) (map map_cong0_of_bnf inners);
    4.14  
    4.15      val set_bd_tacs =
    4.16 -      if ! quick_and_dirty then
    4.17 +      if Config.get lthy quick_and_dirty then
    4.18          replicate ilive (K all_tac)
    4.19        else
    4.20          let
    4.21 @@ -402,7 +402,7 @@
    4.22      fun map_cong0_tac {context = ctxt, prems = _} =
    4.23        rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
    4.24      val set_map_tacs =
    4.25 -      if ! quick_and_dirty then
    4.26 +      if Config.get lthy quick_and_dirty then
    4.27          replicate (n + live) (K all_tac)
    4.28        else
    4.29          replicate n (K empty_natural_tac) @
    4.30 @@ -410,7 +410,7 @@
    4.31      fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
    4.32      fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
    4.33      val set_bd_tacs =
    4.34 -      if ! quick_and_dirty then
    4.35 +      if Config.get lthy quick_and_dirty then
    4.36          replicate (n + live) (K all_tac)
    4.37        else
    4.38          replicate n (K (mk_lift_set_bd_tac (bd_Card_order_of_bnf bnf))) @
     5.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Fri May 17 20:30:04 2013 +0200
     5.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri May 17 20:41:45 2013 +0200
     5.3 @@ -132,7 +132,7 @@
     5.4          Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     5.5      let val pth =
     5.6            (* If quick_and_dirty then run without proof generation as oracle*)
     5.7 -             if !quick_and_dirty
     5.8 +             if Config.get ctxt quick_and_dirty
     5.9               then mirfr_oracle (false, cterm_of thy (Pattern.eta_long [] t1))
    5.10               else mirfr_oracle (true, cterm_of thy (Pattern.eta_long [] t1))
    5.11      in 
     6.1 --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Fri May 17 20:30:04 2013 +0200
     6.2 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Fri May 17 20:41:45 2013 +0200
     6.3 @@ -158,7 +158,7 @@
     6.4  if ($output_log) { print "Mirabelle: $thy_file\n"; }
     6.5  
     6.6  my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
     6.7 -  "-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;
     6.8 +  "-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;
     6.9  
    6.10  if ($output_log) {
    6.11    my $outcome = ($result ? "failure" : "success");
     7.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri May 17 20:30:04 2013 +0200
     7.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri May 17 20:41:45 2013 +0200
     7.3 @@ -850,7 +850,7 @@
     7.4  fun core_tac ctxt = CSUBGOAL (fn (p, i) =>
     7.5     let
     7.6      val cpth = 
     7.7 -       if !quick_and_dirty 
     7.8 +       if Config.get ctxt quick_and_dirty
     7.9         then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
    7.10         else Conv.arg_conv (conv ctxt) p
    7.11      val p' = Thm.rhs_of cpth
     8.1 --- a/src/HOL/Tools/inductive.ML	Fri May 17 20:30:04 2013 +0200
     8.2 +++ b/src/HOL/Tools/inductive.ML	Fri May 17 20:41:45 2013 +0200
     8.3 @@ -116,7 +116,9 @@
     8.4  (** misc utilities **)
     8.5  
     8.6  fun message quiet_mode s = if quiet_mode then () else writeln s;
     8.7 -fun clean_message quiet_mode s = if ! quick_and_dirty then () else message quiet_mode s;
     8.8 +
     8.9 +fun clean_message ctxt quiet_mode s =
    8.10 +  if Config.get ctxt quick_and_dirty then () else message quiet_mode s;
    8.11  
    8.12  fun coind_prefix true = "co"
    8.13    | coind_prefix false = "";
    8.14 @@ -361,7 +363,7 @@
    8.15  (* prove monotonicity *)
    8.16  
    8.17  fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
    8.18 - (message (quiet_mode orelse skip_mono andalso ! quick_and_dirty)
    8.19 + (message (quiet_mode orelse skip_mono andalso Config.get ctxt quick_and_dirty)
    8.20      "  Proving monotonicity ...";
    8.21    (if skip_mono then Goal.prove_sorry else Goal.prove_future) ctxt
    8.22      [] []
    8.23 @@ -379,7 +381,7 @@
    8.24  
    8.25  fun prove_intrs quiet_mode coind mono fp_def k intr_ts rec_preds_defs ctxt ctxt' =
    8.26    let
    8.27 -    val _ = clean_message quiet_mode "  Proving the introduction rules ...";
    8.28 +    val _ = clean_message ctxt quiet_mode "  Proving the introduction rules ...";
    8.29  
    8.30      val unfold = funpow k (fn th => th RS fun_cong)
    8.31        (mono RS (fp_def RS
    8.32 @@ -404,7 +406,7 @@
    8.33  
    8.34  fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt ctxt''' =
    8.35    let
    8.36 -    val _ = clean_message quiet_mode "  Proving the elimination rules ...";
    8.37 +    val _ = clean_message ctxt quiet_mode "  Proving the elimination rules ...";
    8.38  
    8.39      val ([pname], ctxt') = Variable.variant_fixes ["P"] ctxt;
    8.40      val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
    8.41 @@ -453,7 +455,7 @@
    8.42  fun prove_eqs quiet_mode cs params intr_ts intrs
    8.43      (elims: (thm * bstring list * int) list) ctxt ctxt'' =  (* FIXME ctxt'' ?? *)
    8.44    let
    8.45 -    val _ = clean_message quiet_mode "  Proving the simplification rules ...";
    8.46 +    val _ = clean_message ctxt quiet_mode "  Proving the simplification rules ...";
    8.47  
    8.48      fun dest_intr r =
    8.49        (the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))),
    8.50 @@ -640,7 +642,7 @@
    8.51  fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
    8.52      fp_def rec_preds_defs ctxt ctxt''' =  (* FIXME ctxt''' ?? *)
    8.53    let
    8.54 -    val _ = clean_message quiet_mode "  Proving the induction rule ...";
    8.55 +    val _ = clean_message ctxt quiet_mode "  Proving the induction rule ...";
    8.56  
    8.57      (* predicates for induction rule *)
    8.58  
     9.1 --- a/src/HOL/Tools/sat_funcs.ML	Fri May 17 20:30:04 2013 +0200
     9.2 +++ b/src/HOL/Tools/sat_funcs.ML	Fri May 17 20:41:45 2013 +0200
     9.3 @@ -41,8 +41,8 @@
     9.4    dependent) configuration settings.  To replay SAT proofs in Isabelle, you
     9.5    must of course use a proof-producing SAT solver in the first place.
     9.6  
     9.7 -  Proofs are replayed only if "!quick_and_dirty" is false.  If
     9.8 -  "!quick_and_dirty" is true, the theorem (in case the SAT solver claims its
     9.9 +  Proofs are replayed only if "quick_and_dirty" is false.  If
    9.10 +  "quick_and_dirty" is true, the theorem (in case the SAT solver claims its
    9.11    negation to be unsatisfiable) is proved via an oracle.
    9.12  *)
    9.13  
    9.14 @@ -351,7 +351,7 @@
    9.15                (Inttab.dest clause_table) ^ "\n" ^
    9.16              "empty clause: " ^ string_of_int empty_id)
    9.17          else ();
    9.18 -        if !quick_and_dirty then
    9.19 +        if Config.get ctxt quick_and_dirty then
    9.20            make_quick_and_dirty_thm ()
    9.21          else
    9.22            let
    9.23 @@ -378,7 +378,7 @@
    9.24              Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
    9.25            end)
    9.26      | SatSolver.UNSATISFIABLE NONE =>
    9.27 -        if !quick_and_dirty then
    9.28 +        if Config.get ctxt quick_and_dirty then
    9.29           (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
    9.30            make_quick_and_dirty_thm ())
    9.31          else
    10.1 --- a/src/HOL/ex/SAT_Examples.thy	Fri May 17 20:30:04 2013 +0200
    10.2 +++ b/src/HOL/ex/SAT_Examples.thy	Fri May 17 20:41:45 2013 +0200
    10.3 @@ -11,7 +11,7 @@
    10.4  (* ML {* sat.solver := "zchaff_with_proofs"; *} *)
    10.5  (* ML {* sat.solver := "minisat_with_proofs"; *} *)
    10.6  ML {* sat.trace_sat := true; *}
    10.7 -ML {* quick_and_dirty := true; *}
    10.8 +declare [[quick_and_dirty]]
    10.9  
   10.10  lemma "True"
   10.11  by sat
   10.12 @@ -78,7 +78,7 @@
   10.13  by sat
   10.14  
   10.15  ML {* sat.trace_sat := false; *}
   10.16 -ML {* quick_and_dirty := false; *}
   10.17 +declare [[quick_and_dirty = false]]
   10.18  
   10.19  method_setup rawsat = {*
   10.20    Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac)
   10.21 @@ -522,8 +522,9 @@
   10.22  (* ML {*
   10.23  sat.solver := "zchaff_with_proofs";
   10.24  sat.trace_sat := false;
   10.25 -quick_and_dirty := false;
   10.26 -*} *)
   10.27 +*}
   10.28 +declare [[quick_and_dirty = false]]
   10.29 +*)
   10.30  
   10.31  ML {*
   10.32  fun benchmark dimacsfile =
    11.1 --- a/src/Pure/Isar/attrib.ML	Fri May 17 20:30:04 2013 +0200
    11.2 +++ b/src/Pure/Isar/attrib.ML	Fri May 17 20:41:45 2013 +0200
    11.3 @@ -553,7 +553,8 @@
    11.4  (* theory setup *)
    11.5  
    11.6  val _ = Context.>> (Context.map_theory
    11.7 - (register_config Ast.trace_raw #>
    11.8 + (register_config quick_and_dirty_raw #>
    11.9 +  register_config Ast.trace_raw #>
   11.10    register_config Ast.stats_raw #>
   11.11    register_config Printer.show_brackets_raw #>
   11.12    register_config Printer.show_sorts_raw #>
    12.1 --- a/src/Pure/Isar/method.ML	Fri May 17 20:30:04 2013 +0200
    12.2 +++ b/src/Pure/Isar/method.ML	Fri May 17 20:41:45 2013 +0200
    12.3 @@ -20,7 +20,7 @@
    12.4    val SIMPLE_METHOD: tactic -> method
    12.5    val SIMPLE_METHOD': (int -> tactic) -> method
    12.6    val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
    12.7 -  val cheating: bool -> method
    12.8 +  val cheating: Proof.context -> bool -> method
    12.9    val intro: thm list -> method
   12.10    val elim: thm list -> method
   12.11    val unfold: thm list -> Proof.context -> method
   12.12 @@ -127,8 +127,8 @@
   12.13  
   12.14  (* cheating *)
   12.15  
   12.16 -fun cheating int = METHOD (fn _ => fn st =>
   12.17 -  if int orelse ! quick_and_dirty then
   12.18 +fun cheating ctxt int = METHOD (fn _ => fn st =>
   12.19 +  if int orelse Config.get ctxt quick_and_dirty then
   12.20      ALLGOALS Skip_Proof.cheat_tac st
   12.21    else error "Cheating requires quick_and_dirty mode!");
   12.22  
   12.23 @@ -296,7 +296,7 @@
   12.24  val default_text = Source (Args.src (("default", []), Position.none));
   12.25  val this_text = Basic (K this);
   12.26  val done_text = Basic (K (SIMPLE_METHOD all_tac));
   12.27 -fun sorry_text int = Basic (K (cheating int));
   12.28 +fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
   12.29  
   12.30  fun finish_text (NONE, immed) = Basic (finish immed)
   12.31    | finish_text (SOME txt, immed) = Then [txt, Basic (finish immed)];
    13.1 --- a/src/Pure/ROOT.ML	Fri May 17 20:30:04 2013 +0200
    13.2 +++ b/src/Pure/ROOT.ML	Fri May 17 20:41:45 2013 +0200
    13.3 @@ -6,9 +6,6 @@
    13.4    val is_official = false;
    13.5  end;
    13.6  
    13.7 -(*if true then some tools will OMIT some proofs*)
    13.8 -val quick_and_dirty = Unsynchronized.ref false;
    13.9 -
   13.10  print_depth 10;
   13.11  
   13.12  
   13.13 @@ -118,6 +115,9 @@
   13.14  use "context_position.ML";
   13.15  use "config.ML";
   13.16  
   13.17 +val quick_and_dirty_raw = Config.declare_option "quick_and_dirty";
   13.18 +val quick_and_dirty = Config.bool quick_and_dirty_raw;
   13.19 +
   13.20  
   13.21  (* inner syntax *)
   13.22  
    14.1 --- a/src/Pure/Tools/build.ML	Fri May 17 20:30:04 2013 +0200
    14.2 +++ b/src/Pure/Tools/build.ML	Fri May 17 20:41:45 2013 +0200
    14.3 @@ -114,7 +114,6 @@
    14.4      |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    14.5      |> Unsynchronized.setmp Future.ML_statistics true
    14.6      |> no_document options ? Present.no_document
    14.7 -    |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
    14.8      |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
    14.9      |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
   14.10      |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    15.1 --- a/src/Pure/Tools/proof_general_pure.ML	Fri May 17 20:30:04 2013 +0200
    15.2 +++ b/src/Pure/Tools/proof_general_pure.ML	Fri May 17 20:41:45 2013 +0200
    15.3 @@ -131,9 +131,9 @@
    15.4  (* proof *)
    15.5  
    15.6  val _ =
    15.7 -  ProofGeneral.preference_bool ProofGeneral.category_proof
    15.8 +  ProofGeneral.preference_option ProofGeneral.category_proof
    15.9      (SOME "true")
   15.10 -    quick_and_dirty
   15.11 +    @{option quick_and_dirty}
   15.12      "quick-and-dirty"
   15.13      "Take a few short cuts";
   15.14  
    16.1 --- a/src/Pure/goal.ML	Fri May 17 20:30:04 2013 +0200
    16.2 +++ b/src/Pure/goal.ML	Fri May 17 20:41:45 2013 +0200
    16.3 @@ -337,7 +337,7 @@
    16.4    Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
    16.5  
    16.6  fun prove_sorry ctxt xs asms prop tac =
    16.7 -  if ! quick_and_dirty then
    16.8 +  if Config.get ctxt quick_and_dirty then
    16.9      prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac)
   16.10    else (if future_enabled () then prove_future else prove) ctxt xs asms prop tac;
   16.11  
    17.1 --- a/src/Tools/Code/lib/Tools/codegen	Fri May 17 20:30:04 2013 +0200
    17.2 +++ b/src/Tools/Code/lib/Tools/codegen	Fri May 17 20:41:45 2013 +0200
    17.3 @@ -55,9 +55,8 @@
    17.4    handle _ => exit 1;"
    17.5  
    17.6  ACTUAL_CMD="val thyname = \"$THYNAME\"; \
    17.7 -  val _ = quick_and_dirty := $QUICK_AND_DIRTY; \
    17.8    val cmd_expr = \"$CODE_EXPR\"; \
    17.9    val ml_cmd = \"Code_Target.codegen_tool thyname cmd_expr\"; \
   17.10    $FORMAL_CMD"
   17.11  
   17.12 -"$ISABELLE_PROCESS" -r -q -e "$ACTUAL_CMD" "$IMAGE" || exit 1
   17.13 +"$ISABELLE_PROCESS" -r -q -o "quick_and_dirty=$QUICK_AND_DIRTY" -e "$ACTUAL_CMD" "$IMAGE" || exit 1