Merge PR #10581: Remove the tactic wizard, as it has not worked for several years and no one complained (fixes #10580).

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

6 files changed, 2 insertions, 102 deletions

diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map
index 54a592a04d..6bcf3b438f 100644
--- a/ide/MacOS/default_accel_map
+++ b/ide/MacOS/default_accel_map
@@ -7,7 +7,6 @@
 ; (gtk_accel_path "<Actions>/Templates/Template Program Lemma" "")
 (gtk_accel_path "<Actions>/Templates/Lemma" "<Shift><Primary>l")
 ; (gtk_accel_path "<Actions>/Templates/Template Fact" "")
-(gtk_accel_path "<Actions>/Tactics/auto" "<Primary><Control>a")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic fold" "")
 ; (gtk_accel_path "<Actions>/Help/About Coq" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. " "")
@@ -19,7 +18,6 @@
 ; (gtk_accel_path "<Actions>/Tactics/Tactic inversion" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Write State" "")
 ; (gtk_accel_path "<Actions>/Export/Export to" "")
-(gtk_accel_path "<Actions>/Tactics/auto with *" "<Primary><Control>asterisk")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic inversion--clear" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Implicit Arguments" "")
 ; (gtk_accel_path "<Actions>/Edit/Copy" "<Primary>c")
@@ -50,7 +48,6 @@
 ; (gtk_accel_path "<Actions>/Tactics/Tactic fail" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic left" "")
 (gtk_accel_path "<Actions>/Edit/Undo" "<Primary>u")
-(gtk_accel_path "<Actions>/Tactics/eauto with *" "<Primary><Control>ampersand")
 ; (gtk_accel_path "<Actions>/Templates/Template Infix" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic functional induction" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic clear" "")
@@ -149,7 +146,6 @@
 (gtk_accel_path "<Actions>/Templates/Theorem" "<Shift><Primary>t")
 ; (gtk_accel_path "<Actions>/Templates/Template Derive Dependent Inversion--clear" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic unfold" "")
-; (gtk_accel_path "<Actions>/Tactics/Try Tactics" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic red in" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite <- -- in" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Hint Extern" "")
@@ -187,7 +183,6 @@
 ; (gtk_accel_path "<Actions>/Tactics/Tactic intro -- after" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic fold -- in" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Program Definition" "")
-(gtk_accel_path "<Actions>/Tactics/Wizard" "<Primary><Control>dollar")
 ; (gtk_accel_path "<Actions>/Templates/Template Hint Resolve" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Set Extraction Optimize" "")
 ; (gtk_accel_path "<Actions>/File/Revert all buffers" "")
@@ -228,7 +223,6 @@
 ; (gtk_accel_path "<Actions>/Export/Html" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Extraction Inline" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic absurd" "")
-(gtk_accel_path "<Actions>/Tactics/intuition" "<Primary><Control>i")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic simple induction" "")
 ; (gtk_accel_path "<Actions>/Queries/Queries" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite -- in" "")
@@ -289,7 +283,6 @@
 ; (gtk_accel_path "<Actions>/Templates/Template Add Field" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Require Export" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite <-" "")
-(gtk_accel_path "<Actions>/Tactics/omega" "<Primary><Control>o")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic split" "")
 ; (gtk_accel_path "<Actions>/File/Quit" "<Primary>q")
 (gtk_accel_path "<Actions>/View/Display existential variable instances" "<Shift><Control>e")
@@ -328,7 +321,6 @@
 ; (gtk_accel_path "<Actions>/Edit/Edit" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic firstorder" "")
 ; (gtk_accel_path "<Actions>/Templates/Template C" "")
-(gtk_accel_path "<Actions>/Tactics/simpl" "<Primary><Control>s")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic replace -- with" "")
 ; (gtk_accel_path "<Actions>/Templates/Template A" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Remove Printing Record" "")
@@ -360,13 +352,11 @@
 ; (gtk_accel_path "<Actions>/File/File" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic setoid--replace" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic generalize dependent" "")
-(gtk_accel_path "<Actions>/Tactics/trivial" "<Primary><Control>v")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic fix -- with" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic pose --:=--)" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic auto with" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Add Printing Record" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic inversion -- in" "")
-(gtk_accel_path "<Actions>/Tactics/eauto" "<Primary><Control>e")
 ; (gtk_accel_path "<Actions>/File/Open" "<Primary>o")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- using" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Hint" "")
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 566654218d..d52f038f1f 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -137,7 +137,6 @@ class type ops =
 object
   method go_to_insert : unit task
   method go_to_mark : GText.mark -> unit task
-  method tactic_wizard : string list -> unit task
   method process_next_phrase : unit task
   method process_until_end_or_error : unit task
   method handle_reset_initial : unit task
@@ -806,48 +805,6 @@ object(self)
     else Coq.seq (self#backtrack_to_iter ~move_insert:false point)
           (Coq.lift (fun () -> Sentence.tag_on_insert buffer)))
 
-  method tactic_wizard l =
-    let insert_phrase phrase tag =
-      let stop = self#get_start_of_input in
-      let phrase' = if stop#starts_line then phrase else "\n"^phrase in
-      buffer#insert ~iter:stop phrase';
-      Sentence.tag_on_insert buffer;
-      let start = self#get_start_of_input in
-      buffer#move_mark ~where:stop (`NAME "start_of_input");
-      buffer#apply_tag tag ~start ~stop;
-      if self#get_insert#compare stop <= 0 then
-        buffer#place_cursor ~where:stop;
-      let sentence =
-        mk_sentence
-          ~start:(`MARK (buffer#create_mark start))
-          ~stop:(`MARK (buffer#create_mark stop))
-          [] in
-      Doc.push document sentence;
-      messages#default_route#clear;
-      self#show_goals
-    in
-    let display_error (loc, s) =
-      messages#default_route#add (Ideutils.validate s) in
-    let try_phrase phrase stop more =
-      let action = log "Sending to coq now" in
-      let route_id = 0 in
-      let query = Coq.query (route_id,(phrase,Stateid.dummy)) in
-      let next = function
-      | Fail (_, l, str) -> (* FIXME: check *)
-        display_error (l, str);
-        messages#default_route#add (Pp.str ("Unsuccessfully tried: "^phrase));
-        more
-      | Good () -> stop Tags.Script.processed
-      in
-      Coq.bind (Coq.seq action query) next
-    in
-    let rec loop l = match l with
-      | [] -> Coq.return ()
-      | p :: l' ->
-        try_phrase ("progress "^p^".") (insert_phrase (p^".")) (loop l')
-    in
-    loop l
-
   method handle_reset_initial =
     let action () =
       (* clear the stack *)
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index 83ad8c15dc..1e8d87bb15 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -15,7 +15,6 @@ class type ops =
 object
   method go_to_insert : unit task
   method go_to_mark : GText.mark -> unit task
-  method tactic_wizard : string list -> unit task
   method process_next_phrase : unit task
   method process_until_end_or_error : unit task
   method handle_reset_initial : unit task
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 8d95dcee27..2c9f116cc3 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -603,9 +603,6 @@ module Nav = struct
   let join_document _ = send_to_coq (fun sn -> sn.coqops#join_document)
 end
 
-let tactic_wizard_callback l _ =
-  send_to_coq (fun sn -> sn.coqops#tactic_wizard l)
-
 let printopts_callback opts v =
   let b = v#get_active in
   let () = List.iter (fun o -> Coq.PrintOpt.set o b) opts in
@@ -1106,25 +1103,8 @@ let build_ui () =
     ("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f");
   ] end;
 
-  let tacitem s sc =
-    item s ~label:("_"^s)
-      ~accel:(modifier_for_tactics#get^sc)
-      ~callback:(tactic_wizard_callback [s])
-  in
   menu tactics_menu [
-    item "Try Tactics" ~label:"_Try Tactics";
-    item "Wizard" ~label:"<Proof Wizard>" ~stock:`DIALOG_INFO
-      ~tooltip:"Proof Wizard" ~accel:(modifier_for_tactics#get^"dollar")
-      ~callback:(tactic_wizard_callback automatic_tactics#get);
-    tacitem "auto" "a";
-    tacitem "auto with *" "asterisk";
-    tacitem "eauto" "e";
-    tacitem "eauto with *" "ampersand";
-    tacitem "intuition" "i";
-    tacitem "omega" "o";
-    tacitem "simpl" "s";
-    tacitem "tauto" "p";
-    tacitem "trivial" "v";
+    item "Tactics" ~label:"_Tactics";
   ];
   alpha_items tactics_menu "Tactic" Coq_commands.tactics;
 
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index d4a339f4f5..452808490d 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -100,18 +100,7 @@ let init () =
 \n    <menuitem action='Previous' />\
 \n    <menuitem action='Next' />\
 \n  </menu>\
-\n  <menu action='Try Tactics'>\
-\n    <menuitem action='auto' />\
-\n    <menuitem action='auto with *' />\
-\n    <menuitem action='eauto' />\
-\n    <menuitem action='eauto with *' />\
-\n    <menuitem action='intuition' />\
-\n    <menuitem action='omega' />\
-\n    <menuitem action='simpl' />\
-\n    <menuitem action='tauto' />\
-\n    <menuitem action='trivial' />\
-\n    <menuitem action='Wizard' />\
-\n    <separator />\
+\n  <menu action='Tactics'>\
 \n    %s\
 \n  </menu>\
 \n  <menu action='Templates'>\
@@ -173,7 +162,6 @@ let init () =
 \n  <toolitem action='Interrupt' />\
 \n  <toolitem action='Previous' />\
 \n  <toolitem action='Next' />\
-\n  <toolitem action='Wizard' />\
 \n</toolbar>\
 \n</ui>"
     (if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "")
diff --git a/ide/preferences.ml b/ide/preferences.ml
index ea0495bb19..bf9fe8922a 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -938,16 +938,6 @@ let configure ?(apply=(fun () -> ())) parent =
                    else cmd_browse#get])
       cmd_browse#get
   in
-(*
-  let automatic_tactics =
-    strings
-      ~f:automatic_tactics#set
-      ~add:(fun () -> ["<edit me>"])
-      "Wizard tactics to try in order"
-      automatic_tactics#get
-
-  in
-*)
 
   let contextual_menus_on_goal = pbool "Contextual menus on goal" contextual_menus_on_goal in
 
@@ -1008,10 +998,6 @@ let configure ?(apply=(fun () -> ())) parent =
      Section("Externals", None,
 	     [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
               cmd_print;cmd_editor;cmd_browse]);
-(*
-     Section("Tactics Wizard", None,
-	     [automatic_tactics]);
-*)
      Section("Shortcuts", Some `PREFERENCES,
 	     [modifiers_valid; modifier_for_tactics;
         modifier_for_templates; modifier_for_display; modifier_for_navigation;