From 40c483a95f354e457e10d00951fd6a8eec08176d Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Mon, 5 Nov 2018 13:32:36 -0800 Subject: Document undocumented flags and options Also remove a few undocumented settings --- doc/sphinx/proof-engine/ltac.rst | 2 +- .../proof-engine/ssreflect-proof-language.rst | 36 +++++++++++++++++++--- doc/sphinx/proof-engine/tactics.rst | 25 +++++++++++++++ 3 files changed, 57 insertions(+), 6 deletions(-) (limited to 'doc/sphinx/proof-engine') diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 0ea8c7be2d..1071682ead 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1208,7 +1208,7 @@ Interactive debugger .. flag:: Ltac Debug - This option governs the step-by-step debugger that comes with the |Ltac| interpreter + This option governs the step-by-step debugger that comes with the |Ltac| interpreter. When the debugger is activated, it stops at every step of the evaluation of the current |Ltac| expression and prints information on what it is doing. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3ca0ffe678..e3089f0d09 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -157,14 +157,18 @@ compatible with the rest of |Coq|, up to a few discrepancies: (see :ref:`pattern_conditional_ssr`). To use the generalized form, turn off the |SSR| Boolean ``if`` notation using the command: ``Close Scope boolean_if_scope``. -+ The following two options can be unset to disable the incompatible - rewrite syntax and allow reserved identifiers to appear in scripts. ++ The following flags can be unset to make |SSR| more compatible with + parts of Coq: - .. coqtop:: in +.. flag:: SsrRewrite + + Controls whether the incompatible rewrite syntax is enabled (the default). + Disabling the flag makes the syntax compatible with other parts of Coq. - Unset SsrRewrite. - Unset SsrIdents. +.. flag:: SsrIdents + Controls whether reserved identifiers can appear in scripts. The default + is "on". "off" is compatible with other parts of Coq. |Gallina| extensions -------------------- @@ -3063,6 +3067,17 @@ An :token:`r_item` can be: rewrite -[f y x]/(y + _). +.. flag:: SsrOldRewriteGoalsOrder + + Controls the order in which generated subgoals (side conditions) + are added to the + proof context. "off", the default value, puts subgoals generated + by conditional rules first, followed by the main goal. "on" puts + the main goal first. If your proofs are organized to complete + proving the main goal before side conditions, "on" will save you + from having to add :tacn:`last first` tactics that would be needed + to keep the main goal as the currently focused goal. + Remarks and examples ~~~~~~~~~~~~~~~~~~~~ @@ -5428,6 +5443,17 @@ right hand side double , view hint declaration see :ref:`declaring_new_hints_ssr prenex implicits declaration see :ref:`parametric_polymorphism_ssr` +Settings +~~~~~~~~ + +.. flag:: Debug Ssreflect + + *Developer only.* Print debug information on reflect. + +.. flag:: Debug SsrMatching + + *Developer only.* Print debug information on SSR matching. + .. rubric:: Footnotes .. [#1] Unfortunately, even after a call to the Set Printing All command, diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 150aadc15a..6b48c3cc14 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4503,3 +4503,28 @@ user-defined tactics. significant changes in your theories to obtain the same result. As a drawback of the re-engineering of the code, this tactic has also been completely revised to get a very compact and readable version. + +Proof maintenance +----------------- + +*Experimental.* Many tactics, such as :tacn:`intros`, can automatically generate names, such +as "H0" or "H1" for a new hypothesis introduced from a goal. Subsequent proof steps +may explicitly refer to these names. However, future versions of Coq may not assign +names exactly the same way, which could cause the proof to fail because the +new names don't match the explicit references in the proof. + +The following "Mangle Names" settings let users find all the +places where proofs rely on automatically generated names, which can +then be named explicitly to avoid any incompatibility. These +settings cause Coq to generate different names, producing errors for +references to automatically generated names. + +.. flag:: Mangle Names + + When set, generated names use the prefix specified in the following + option instead of the default prefix. + +.. opt:: Mangle Names Prefix @string + :name: Mangle Names Prefix + + Specifies the prefix to use when generating names. -- cgit v1.2.3 From 9903f6a7f86661549def884a0050d0f4537d52d7 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Wed, 28 Nov 2018 10:35:27 -0800 Subject: Add undocumented options from mattam82 --- .../proof-engine/ssreflect-proof-language.rst | 18 +++++++---- doc/sphinx/proof-engine/tactics.rst | 36 ++++++++++++++++++++-- 2 files changed, 45 insertions(+), 9 deletions(-) (limited to 'doc/sphinx/proof-engine') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index e3089f0d09..9fbac95f0c 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -167,8 +167,14 @@ compatible with the rest of |Coq|, up to a few discrepancies: .. flag:: SsrIdents - Controls whether reserved identifiers can appear in scripts. The default - is "on". "off" is compatible with other parts of Coq. + Controls whether tactics can refer to |SSR|-generated variables that are + in the form _xxx_. Scripts with explicit references to such variables + are fragile; they are prone to failure if the proof is later modified or + if the details of variable name generation change in future releases of Coq. + + The default is on, which gives an error message when the user tries to + create such identifiers. Disabling the flag generates a warning instead, + increasing compatibility with other parts of Coq. |Gallina| extensions -------------------- @@ -3071,10 +3077,10 @@ An :token:`r_item` can be: Controls the order in which generated subgoals (side conditions) are added to the - proof context. "off", the default value, puts subgoals generated - by conditional rules first, followed by the main goal. "on" puts - the main goal first. If your proofs are organized to complete - proving the main goal before side conditions, "on" will save you + proof context. The flag is off by default, which puts subgoals generated + by conditional rules first, followed by the main goal. When it is on, + the main goal appears first. If your proofs are organized to complete + proving the main goal before side conditions, turning the flag on will save you from having to add :tacn:`last first` tactics that would be needed to keep the main goal as the currently focused goal. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 6b48c3cc14..ad80cb62e1 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -264,6 +264,11 @@ Applying theorems This tactic behaves like :tacn:`simple refine` except it performs type checking without resolution of typeclasses. + .. flag:: Debug Unification + + Enables printing traces of unification steps used during + elaboration/typechecking and the :tacn:`refine` tactic. + .. tacn:: apply @term :name: apply @@ -606,6 +611,10 @@ Applying theorems when the instantiation of a variable cannot be found (cf. :tacn:`eapply` and :tacn:`apply`). +.. flag:: Debug Tactic Unification + + Enables printing traces of unification steps in tactic unification. + Tactic unification is used in tactics such as :tacn:`apply` and :tacn:`rewrite`. .. _managingthelocalcontext: @@ -2096,9 +2105,9 @@ and an explanation of the underlying technique. Part of the behavior of the ``inversion`` tactic is to generate equalities between expressions that appeared in the hypothesis that is being processed. By default, no equalities are generated if they - relate two proofs (i.e. equalities between :n:`@terms` whose type is in sort - :g:`Prop`). This behavior can be turned off by using the option - :flag`Keep Proof Equalities`. + relate two proofs (i.e. equalities between :token:`term`\s whose type is in sort + :g:`Prop`). This behavior can be turned off by using the + :flag:`Keep Proof Equalities` setting. .. tacv:: inversion @num @@ -2534,6 +2543,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. unresolved bindings into existential variables, if any, instead of failing. It has the same variants as :tacn:`rewrite` has. + .. flag:: Keyed Unification + + Makes higher-order unification used by :tacn:`rewrite` rely on a set of keys to drive + unification. The subterms, considered as rewriting candidates, must start with + the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments + are then unified up to full reduction. + .. tacn:: replace @term with @term’ :name: replace @@ -4504,6 +4520,20 @@ user-defined tactics. drawback of the re-engineering of the code, this tactic has also been completely revised to get a very compact and readable version. +Delaying solving unification constraints +---------------------------------------- + +.. tacn:: solve_constraints + :name: solve_constraints + :undocumented: + +.. flag:: Solve Unification Constraints + + By default, after each tactic application, postponed typechecking unification + problems are resolved using heuristics. Unsetting this flag disables this + behavior, allowing tactics to leave unification constraints unsolved. Use the + :tacn:`solve_constraints` tactic at any point to solve the constraints. + Proof maintenance ----------------- -- cgit v1.2.3