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

7 files changed, 2 insertions, 132 deletions

diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index efb5df720a..7d6171285e 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -88,8 +88,6 @@ There are other buttons on the |CoqIDE| toolbar: a button to save the running
 buffer; a button to close the current buffer (an "X"); buttons to switch among
 buffers (left and right arrows); an "information" button; and a "gears" button.
 
-The "information" button is described in Section :ref:`try-tactics-automatically`.
-
 The "gears" button submits proof terms to the |Coq| kernel for type checking.
 When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`),
 proofs may have been completed without kernel-checking of generated proof terms.
@@ -100,27 +98,6 @@ processed color, though their preceding proofs have the processed color.
 Notice that for all these buttons, except for the "gears" button, their operations
 are also available in the menu, where their keyboard shortcuts are given.
 
-.. _try-tactics-automatically:
-
-Trying tactics automatically
-------------------------------
-
-The menu Try Tactics provides some features for automatically trying
-to solve the current goal using simple tactics. If such a tactic
-succeeds in solving the goal, then its text is automatically inserted
-into the script. There is finally a combination of these tactics,
-called the *proof wizard* which will try each of them in turn. This
-wizard is also available as a tool button (the "information" button). The set of
-tactics tried by the wizard is customizable in the preferences.
-
-These tactics are general ones, in particular they do not refer to
-particular hypotheses. You may also try specific tactics related to
-the goal or one of the hypotheses, by clicking with the right mouse
-button on the goal or the considered hypothesis. This is the
-“contextual menu on goals” feature, that may be disabled in the
-preferences if undesirable.
-
-
 Proof folding
 ------------------
 
@@ -202,13 +179,6 @@ compilation, printing, web browsing. In the browser command, you may
 use `%s` to denote the URL to open, for example:
 `firefox -remote "OpenURL(%s)"`.
 
-The `Tactics Wizard` section allows defining the set of tactics that
-should be tried, in sequence, to solve the current goal.
-
-The last section is for miscellaneous boolean settings, such as the
-“contextual menu on goals” feature presented in the section
-:ref:`Try tactics automatically <try-tactics-automatically>`.
-
 Notice that these settings are saved in the file `.coqiderc` of your
 home directory.
 
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;