diff options
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 135 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 6 | ||||
| -rw-r--r-- | test-suite/ssr/autoclean.v | 4 | ||||
| -rw-r--r-- | test-suite/stm/arg_filter_1.v | 4 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 35 |
6 files changed, 105 insertions, 85 deletions
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index e5b41be691..d15aacad44 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -37,7 +37,7 @@ In addition to these user-defined classes, we have two built-in classes: * ``Funclass``, the class of functions; its objects are all the terms with a functional type, i.e. of form :g:`forall x:A,B`. -Formally, the syntax of a classes is defined as: +Formally, the syntax of classes is defined as: .. productionlist:: class: `qualid` @@ -289,7 +289,7 @@ by extending the existing :cmd:`Record` macro. Its new syntax is: The first identifier :token:`ident` is the name of the defined record and :token:`sort` is its type. The optional identifier after ``:=`` is the name - of the constuctor (it will be :n:`Build_@ident` if not given). + of the constructor (it will be :n:`Build_@ident` if not given). The other identifiers are the names of the fields, and :token:`term` are their respective types. If ``:>`` is used instead of ``:`` in the declaration of a field, then the name of this field is automatically @@ -365,7 +365,7 @@ We first give an example of coercion between atomic inductive types .. warning:: - Note that ``Check true=O`` would fail. This is "normal" behavior of + Note that ``Check (true = O)`` would fail. This is "normal" behavior of coercions. To validate ``true=O``, the coercion is searched from ``nat`` to ``bool``. There is none. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 081fef07b9..66d510bc0e 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3406,129 +3406,140 @@ Automation This tactic implements a Prolog-like resolution procedure to solve the current goal. It first tries to solve the goal using the :tacn:`assumption` - tactic, then it reduces the goal to an atomic one using intros and + tactic, then it reduces the goal to an atomic one using :tacn:`intros` and introduces the newly generated hypotheses as hints. Then it looks at the list of tactics associated to the head symbol of the goal and tries to apply one of them (starting from the tactics with lower cost). This process is recursively applied to the generated subgoals. - By default, auto only uses the hypotheses of the current goal and the - hints of the database named core. + By default, :tacn:`auto` only uses the hypotheses of the current goal and + the hints of the database named ``core``. -.. tacv:: auto @num + .. warning:: - Forces the search depth to be :token:`num`. The maximal search depth - is 5 by default. + :tacn:`auto` uses a weaker version of :tacn:`apply` that is closer to + :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will + fail even if applying manually one of the hints would succeed. -.. tacv:: auto with {+ @ident} + .. tacv:: auto @num - Uses the hint databases :n:`{+ @ident}` in addition to the database core. + Forces the search depth to be :token:`num`. The maximal search depth + is 5 by default. + + .. tacv:: auto with {+ @ident} + + Uses the hint databases :n:`{+ @ident}` in addition to the database ``core``. + + .. note:: + + Use the fake database `nocore` if you want to *not* use the `core` + database. + + .. tacv:: auto with * + + Uses all existing hint databases. Using this variant is highly discouraged + in finished scripts since it is both slower and less robust than the variant + where the required databases are explicitly listed. .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of pre-defined databases and the way to create or extend a database. -.. tacv:: auto with * + .. tacv:: auto using {+ @ident__i} {? with {+ @ident } } - Uses all existing hint databases. + Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an + inductive type, it is the collection of its constructors which are added + as hints. - .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + .. note:: -.. tacv:: auto using {+ @ident__i} {? with {+ @ident } } + The hints passed through the `using` clause are used in the same + way as if they were passed through a hint database. Consequently, + they use a weaker version of :tacn:`apply` and :n:`auto using @ident` + may fail where :n:`apply @ident` succeeds. - Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an - inductive type, it is the collection of its constructors which are added - as hints. + Given that this can be seen as counter-intuitive, it could be useful + to have an option to use full-blown :tacn:`apply` for lemmas passed + through the `using` clause. Contributions welcome! -.. tacv:: info_auto + .. tacv:: info_auto - Behaves like auto but shows the tactics it uses to solve the goal. This - variant is very useful for getting a better understanding of automation, or - to know what lemmas/assumptions were used. + Behaves like :tacn:`auto` but shows the tactics it uses to solve the goal. This + variant is very useful for getting a better understanding of automation, or + to know what lemmas/assumptions were used. -.. tacv:: debug auto - :name: debug auto + .. tacv:: debug auto + :name: debug auto - Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, - including failing paths. + Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, + including failing paths. -.. tacv:: {? info_}auto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}auto {? @num} {? using {+ @lemma}} {? with {+ @ident}} - This is the most general form, combining the various options. + This is the most general form, combining the various options. .. tacv:: trivial :name: trivial - This tactic is a restriction of auto that is not recursive + This tactic is a restriction of :tacn:`auto` that is not recursive and tries only hints that cost `0`. Typically it solves trivial equalities like :g:`X=X`. -.. tacv:: trivial with {+ @ident} - :undocumented: - -.. tacv:: trivial with * - :undocumented: - -.. tacv:: trivial using {+ @lemma} - :undocumented: - -.. tacv:: debug trivial - :name: debug trivial - :undocumented: - -.. tacv:: info_trivial - :name: info_trivial - :undocumented: - -.. tacv:: {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} - :undocumented: + .. tacv:: trivial with {+ @ident} + trivial with * + trivial using {+ @lemma} + debug trivial + info_trivial + {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} + :name: _; _; _; debug trivial; info_trivial; _ + :undocumented: .. note:: - :tacn:`auto` either solves completely the goal or else leaves it - intact. :tacn:`auto` and :tacn:`trivial` never fail. - -The following options enable printing of informative or debug information for -the :tacn:`auto` and :tacn:`trivial` tactics: + :tacn:`auto` and :tacn:`trivial` either solve completely the goal or + else succeed without changing the goal. Use :g:`solve [ auto ]` and + :g:`solve [ trivial ]` if you would prefer these tactics to fail when + they do not manage to solve the goal. .. flag:: Info Auto Debug Auto Info Trivial Debug Trivial - :undocumented: -.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + These options enable printing of informative or debug information for + the :tacn:`auto` and :tacn:`trivial` tactics. .. tacn:: eauto :name: eauto This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try resolution hints which would leave existential variables in the goal, - :tacn:`eauto` does try them (informally speaking, it usessimple :tacn:`eapply` - where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto` + :tacn:`eauto` does try them (informally speaking, it internally uses a tactic + close to :tacn:`simple eapply` instead of a tactic close to :tacn:`simple apply` + in the case of :tacn:`auto`). As a consequence, :tacn:`eauto` can solve such a goal: .. example:: .. coqtop:: all - Hint Resolve ex_intro. + Hint Resolve ex_intro : core. Goal forall P:nat -> Prop, P 0 -> exists n, P n. eauto. Note that ``ex_intro`` should be declared as a hint. -.. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} - The various options for :tacn:`eauto` are the same as for :tacn:`auto`. + The various options for :tacn:`eauto` are the same as for :tacn:`auto`. -:tacn:`eauto` also obeys the following options: + :tacn:`eauto` also obeys the following options: -.. flag:: Info Eauto - Debug Eauto - :undocumented: + .. flag:: Info Eauto + Debug Eauto + :undocumented: -.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` .. tacn:: autounfold with {+ @ident} diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 3fb21e5ef6..2a2cd73df2 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -591,10 +591,8 @@ END GRAMMAR EXTEND Gram GLOBAL: ssrfwdview; ssrfwdview: [ - [ test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr -> - { [mk_ast_closure_term `None c] } - | test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrfwdview -> - { (mk_ast_closure_term `None c) :: w } ]]; + [ test_not_ssrslashnum; "/"; c = ast_closure_term -> { [c] } + | test_not_ssrslashnum; "/"; c = ast_closure_term; w = ssrfwdview -> { c :: w } ]]; END (* ipats *) diff --git a/test-suite/ssr/autoclean.v b/test-suite/ssr/autoclean.v new file mode 100644 index 0000000000..db80a62259 --- /dev/null +++ b/test-suite/ssr/autoclean.v @@ -0,0 +1,4 @@ +Require Import ssreflect. + +Lemma view_disappears A B (AB : A -> B) : A -> False. +Proof. move=> {}/(AB). have := AB. Abort. diff --git a/test-suite/stm/arg_filter_1.v b/test-suite/stm/arg_filter_1.v index 1cf66d6b43..ed87d67405 100644 --- a/test-suite/stm/arg_filter_1.v +++ b/test-suite/stm/arg_filter_1.v @@ -1,4 +1,4 @@ (* coq-prog-args: ("-async-proofs-tac-j" "1") *) -Lemma foo : True. -Proof. now auto. Qed. +Lemma foo (A B : Prop) n : n + 0 = n /\ (A -> B -> A). +Proof. split. par: now auto. Qed. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 1e1a74209f..c110f3831e 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -13,6 +13,9 @@ let fatal_error exn = let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in exit exit_code +let error_wrong_arg msg = + prerr_endline msg; exit 1 + let error_missing_arg s = prerr_endline ("Error: extra argument expected after option "^s); prerr_endline "See -help for the syntax of supported options"; @@ -169,7 +172,8 @@ let set_color opts = function | "yes" | "on" -> { opts with color = `ON } | "no" | "off" -> { opts with color = `OFF } | "auto" -> { opts with color = `AUTO } -| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1 +| _ -> + error_wrong_arg ("Error: on/off/auto expected after option color") let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" @@ -187,26 +191,26 @@ let exitcode opts = if opts.filter_opts then 2 else 0 let get_bool opt = function | "yes" | "on" -> true | "no" | "off" -> false - | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1 + | _ -> + error_wrong_arg ("Error: yes/no expected after option "^opt) let get_int opt n = try int_of_string n with Failure _ -> - prerr_endline ("Error: integer expected after option "^opt); exit 1 + error_wrong_arg ("Error: integer expected after option "^opt) let get_float opt n = try float_of_string n with Failure _ -> - prerr_endline ("Error: float expected after option "^opt); exit 1 + error_wrong_arg ("Error: float expected after option "^opt) let get_host_port opt s = match String.split_on_char ':' s with | [host; portr; portw] -> - Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) + Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) | ["stdfds"] -> Some Spawned.AnonPipe | _ -> - prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt); - exit 1 + error_wrong_arg ("Error: host:portr:portw or stdfds expected after option "^opt) let get_error_resilience opt = function | "on" | "all" | "yes" -> `All @@ -216,17 +220,20 @@ let get_error_resilience opt = function let get_priority opt s = try CoqworkmgrApi.priority_of_string s with Invalid_argument _ -> - prerr_endline ("Error: low/high expected after "^opt); exit 1 + error_wrong_arg ("Error: low/high expected after "^opt) let get_async_proofs_mode opt = let open Stm.AsyncOpts in function | "no" | "off" -> APoff | "yes" | "on" -> APon | "lazy" -> APonLazy - | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 + | _ -> + error_wrong_arg ("Error: on/off/lazy expected after "^opt) let get_cache opt = function | "force" -> Some Stm.AsyncOpts.Force - | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 + | _ -> + error_wrong_arg ("Error: force expected after "^opt) + let get_native_name s = (* We ignore even critical errors because this mode has to be super silent *) @@ -313,8 +320,7 @@ let parse_args ~help ~init arglist : t * string list = |"-async-proofs-tac-j" -> let j = get_int opt (next ()) in if j <= 0 then begin - prerr_endline ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1"); - exit 1; + error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1") end; { oval with stm_flags = { oval.stm_flags with Stm.AsyncOpts.async_proofs_n_tacworkers = j @@ -436,7 +442,8 @@ let parse_args ~help ~init arglist : t * string list = | ("yes" | "on") -> NativeOn {ondemand=false} | "ondemand" -> NativeOn {ondemand=true} | ("no" | "off") -> NativeOff - | _ -> prerr_endline ("Error: (yes|no|ondemand) expected after option -native-compiler"); exit 1 + | _ -> + error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in { oval with native_compiler } @@ -461,7 +468,7 @@ let parse_args ~help ~init arglist : t * string list = if List.exists (fun x -> opt = x) ["off"; "on"; "removed"] then Proof_diffs.write_diffs_option opt else - (prerr_endline ("Error: on|off|removed expected after -diffs"); exit 1); + error_wrong_arg "Error: on|off|removed expected after -diffs"; { oval with diffs_set = true } |"-stm-debug" -> Stm.stm_debug := true; oval |"-emacs" -> set_emacs oval |