diff options
| author | Pierre-Marie Pédrot | 2020-01-11 14:51:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-01-11 14:51:42 +0100 |
| commit | 8a5e3cd84ab077f0bbe57bd13dca750cda043bf4 (patch) | |
| tree | 4cdd45e5a6f009747a27b179f5a97de7cfc41fbf | |
| parent | ba6ea757c79318a452bc1c044e140ebade6b224c (diff) | |
| parent | df452a678d4fcb82a35847a194408e1e59846ad0 (diff) | |
Merge PR #11349: [refman] [changelog] Announce omega replacement.
Ack-by: ejgallego
Reviewed-by: maximedenes
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 5 |
2 files changed, 26 insertions, 0 deletions
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 650a444a16..daca43e65e 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -5,6 +5,27 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic :Author: Pierre Crégut +.. warning:: + + The :tacn:`omega` tactic is about to be deprecated in favor of the + :tacn:`lia` tactic. The goal is to consolidate the arithmetic + solving capabilities of Coq into a single engine; moreover, + :tacn:`lia` is in general more powerful than :tacn:`omega` (it is a + complete Presburger arithmetic solver while :tacn:`omega` was known + to be incomplete). + + Work is in progress to make sure that there are no regressions + (including no performance regression) when switching from + :tacn:`omega` to :tacn:`lia` in existing projects. However, we + already recommend using :tacn:`lia` in new or refactored proof + scripts. We also ask that you report (in our `bug tracker + <https://github.com/coq/coq/issues>`_) any issue you encounter, + especially if the issue was not present in :tacn:`omega`. + + Note that replacing :tacn:`omega` with :tacn:`lia` can break + non-robust proof scripts which rely on incompleteness bugs of + :tacn:`omega` (e.g. using the pattern :g:`; try omega`). + Description of ``omega`` ------------------------ diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 33fc211fa5..21000889d3 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -50,6 +50,11 @@ __ 811RefineInstance_ __ 811SSRUnderOver_ __ 811Reals_ +Additionally, while the :tacn:`omega` tactic is not yet deprecated in +this version of Coq, it should soon be the case and we already +recommend users to switch to :tacn:`lia` in new proof scripts (see +also the warning message in the :ref:`corresponding chapter <omega>`). + The ``dev/doc/critical-bugs`` file documents the known critical bugs of |Coq| and affected releases. See the `Changes in 8.11+beta1`_ section for the detailed list of changes, including potentially breaking changes marked with |