aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/changelog/03-notations/11859-warn-inexact-float.rst6
-rw-r--r--doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst7
-rw-r--r--doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst3
-rw-r--r--doc/sphinx/changes.rst4
-rw-r--r--doc/sphinx/language/coq-library.rst5
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst29
-rw-r--r--doc/tools/docgram/README.md3
-rw-r--r--doc/tools/docgram/common.edit_mlg4
-rw-r--r--doc/tools/docgram/doc_grammar.ml33
-rw-r--r--doc/tools/docgram/dune63
-rw-r--r--doc/tools/docgram/fullGrammar4
-rw-r--r--doc/tools/docgram/orderedGrammar4
12 files changed, 100 insertions, 65 deletions
diff --git a/doc/changelog/03-notations/11859-warn-inexact-float.rst b/doc/changelog/03-notations/11859-warn-inexact-float.rst
new file mode 100644
index 0000000000..224ffdbe9b
--- /dev/null
+++ b/doc/changelog/03-notations/11859-warn-inexact-float.rst
@@ -0,0 +1,6 @@
+- **Added:**
+ In primitive floats, print a warning when parsing a decimal value
+ that is not exactly a binary64 floating-point number.
+ For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
+ (`#11859 <https://github.com/coq/coq/pull/11859>`_,
+ by Pierre Roux).
diff --git a/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst b/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst
new file mode 100644
index 0000000000..d510416990
--- /dev/null
+++ b/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst
@@ -0,0 +1,7 @@
+- **Changed:** The :g:`auto with zarith` tactic and variations (including :tacn:`intuition`)
+ may now call the :tacn:`lia` tactic instead of :tacn:`omega`
+ (when the `Omega` module is loaded);
+ more goals may be automatically solved,
+ fewer section variables will be captured spuriously
+ (`#11018 <https://github.com/coq/coq/pull/11018>`_,
+ by Vincent Laporte).
diff --git a/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst b/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst
new file mode 100644
index 0000000000..e409c638bb
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst
@@ -0,0 +1,3 @@
+- **Removed:** Removed SearchAbout command that was deprecated in 8.5.
+ Use :cmd:`Search` instead.
+ (`#11944 <https://github.com/coq/coq/pull/11944>`_, by Jim Fehrle).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 5ca0d8b81f..7401aff48c 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -383,6 +383,10 @@ Changes in 8.11+beta1
<https://github.com/coq/coq/issues/3890>`_ and `#4638
<https://github.com/coq/coq/issues/4638>`_
by Maxime Dénès, review by Gaëtan Gilbert).
+- **Changed:**
+ :cmd:`Fail` does not catch critical errors (including "stack overflow")
+ anymore (`#10173 <https://github.com/coq/coq/pull/10173>`_,
+ by Gaëtan Gilbert).
- **Removed:**
Undocumented :n:`Instance : !@type` syntax
(`#10185 <https://github.com/coq/coq/pull/10185>`_, by Gaëtan Gilbert).
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 39f2ccec29..acdd4408ed 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -1062,6 +1062,11 @@ Floating-point constants are parsed and pretty-printed as (17-digit)
decimal constants. This ensures that the composition
:math:`\text{parse} \circ \text{print}` amounts to the identity.
+.. warn:: The constant @numeral is not a binary64 floating-point value. A closest value will be used and unambiguously printed @numeral. [inexact-float,parsing]
+
+ Not all decimal constants are floating-point values. This warning
+ is generated when parsing such a constant (for instance ``0.1``).
+
.. example::
.. coqtop:: all
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index c33d62532e..b22c5286fe 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -321,18 +321,6 @@ Requests to the environment
Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
- .. cmdv:: SearchAbout
- :name: SearchAbout
-
- .. deprecated:: 8.5
-
- Up to |Coq| version 8.4, :cmd:`Search` had the behavior of current
- :cmd:`SearchHead` and the behavior of current :cmd:`Search` was obtained with
- command :cmd:`SearchAbout`. For compatibility, the deprecated name
- :cmd:`SearchAbout` can still be used as a synonym of :cmd:`Search`. For
- compatibility, the list of objects to search when using :cmd:`SearchAbout`
- may also be enclosed by optional ``[ ]`` delimiters.
-
.. cmd:: SearchHead @term
@@ -929,16 +917,17 @@ Quitting and debugging
.. cmd:: Fail @command
- For debugging scripts, sometimes it is desirable to know
- whether a command or a tactic fails. If the given :n:`@command`
- fails, the ``Fail`` statement succeeds, without changing the proof
- state, and in interactive mode, the system
- prints a message confirming the failure.
- If the given :n:`@command` succeeds, the statement is an error, and
- it prints a message indicating that the failure did not occur.
+ For debugging scripts, sometimes it is desirable to know whether a
+ command or a tactic fails. If the given :n:`@command` fails, then
+ :n:`Fail @command` succeeds (excepts in the case of
+ critical errors, like a "stack overflow"), without changing the
+ proof state, and in interactive mode, the system prints a message
+ confirming the failure.
.. exn:: The command has not failed!
- :undocumented:
+
+ If the given :n:`@command` succeeds, then :n:`Fail @command`
+ fails with this error message.
.. _controlling-display:
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index 7ae98f4cd2..4cde3809f0 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -110,6 +110,9 @@ Other command line arguments:
* `-no-warn` suppresses printing of some warning messages
+* `-no-update` puts updates to `fullGrammar` and `orderedGrammar` into new files named
+ `*.new`, leaving the originals unmodified. For use in Dune.
+
* `-short` limits processing to updating/verifying only the `fullGrammar` file
* `-verbose` prints more messages about the grammar
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 88a5217652..60b845c4be 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1125,10 +1125,6 @@ query_command: [
| WITH "SearchRewrite" constr_pattern in_or_out_modules
| REPLACE "Search" searchabout_query searchabout_queries "."
| WITH "Search" searchabout_query searchabout_queries
-| REPLACE "SearchAbout" searchabout_query searchabout_queries "."
-| WITH "SearchAbout" searchabout_query searchabout_queries
-| REPLACE "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "."
-| WITH "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules
]
vernac_toplevel: [
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 0450aee2ec..eea1d5081d 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -32,6 +32,7 @@ type args = {
fullGrammar : bool;
check_tacs : bool;
check_cmds : bool;
+ no_update: bool;
show_warn : bool;
verbose : bool;
verify : bool;
@@ -43,6 +44,7 @@ let default_args = {
fullGrammar = false;
check_tacs = false;
check_cmds = false;
+ no_update = false;
show_warn = true;
verbose = false;
verify = false;
@@ -1574,7 +1576,7 @@ let reorder_grammar eg reordered_rules file =
g_reorder eg !og.map !og.order
-let finish_with_file old_file verify =
+let finish_with_file old_file args =
let files_eq f1 f2 =
let chunksize = 8192 in
(try
@@ -1605,18 +1607,18 @@ let finish_with_file old_file verify =
with Sys_error _ -> false)
in
- let temp_file = (old_file ^ "_temp") in
+ let temp_file = (old_file ^ ".new") in
if !exit_code <> 0 then
Sys.remove temp_file
- else if verify then begin
+ else if args.verify then begin
if not (files_eq old_file temp_file) then
error "%s is not current\n" old_file;
Sys.remove temp_file
- end else
+ end else if not args.no_update then
Sys.rename temp_file old_file
let open_temp_bin file =
- open_out_bin (sprintf "%s_temp" file)
+ open_out_bin (sprintf "%s.new" file)
let match_cmd_regex = Str.regexp "[a-zA-Z0-9_ ]+"
@@ -1829,7 +1831,7 @@ let process_rst g file args seen tac_prods cmd_prods =
with End_of_file -> ();
close_in old_rst;
close_out new_rst;
- finish_with_file file args.verify
+ finish_with_file file args
let report_omitted_prods entries seen label split =
let maybe_warn first last n =
@@ -1877,7 +1879,7 @@ let process_grammar args =
"DOC_GRAMMAR";
print_in_order out g `MLG !g.order StringSet.empty;
close_out out;
- finish_with_file (dir "fullGrammar") args.verify;
+ finish_with_file (dir "fullGrammar") args;
if args.verbose then
print_special_tokens g;
@@ -1896,7 +1898,7 @@ let process_grammar args =
"DOC_GRAMMAR";
print_in_order out g `MLG !g.order StringSet.empty;
close_out out;
- finish_with_file (dir "editedGrammar") args.verify;
+ finish_with_file (dir "editedGrammar") args;
report_bad_nts g "editedGrammar"
end;
@@ -1911,11 +1913,13 @@ let process_grammar args =
reorder_grammar g ordered_grammar "orderedGrammar";
print_in_order out g `MLG !g.order StringSet.empty;
close_out out;
- finish_with_file (dir "orderedGrammar") args.verify;
+ finish_with_file (dir "orderedGrammar") args;
check_singletons g
(* print_dominated g*)
end;
+ let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; tacvs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in
+ let args = { args with no_update = false } in (* always update rsts in place for now *)
if !exit_code = 0 then begin
let plist nt =
let list = (List.map (fun t -> String.trim (prod_to_prodn t))
@@ -1923,17 +1927,20 @@ let process_grammar args =
list, StringSet.of_list list in
let tac_list, tac_prods = plist "simple_tactic" in
let cmd_list, cmd_prods = plist "command" in
- let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; tacvs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in
List.iter (fun file -> process_rst g file args seen tac_prods cmd_prods) args.rst_files;
report_omitted_prods !g.order !seen.nts "Nonterminal" "";
let out = open_out (dir "updated_rsts") in
close_out out;
+ end;
+
(*
if args.check_tacs then
report_omitted_prods tac_list !seen.tacs "Tactic" "\n ";
if args.check_cmds then
report_omitted_prods cmd_list !seen.cmds "Command" "\n ";
*)
+
+ if !exit_code = 0 then begin
(* generate report on cmds or tacs *)
let cmdReport outfile cmdStr cmd_nts cmds cmdvs =
let rstCmds = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings cmds)) in
@@ -1942,7 +1949,7 @@ let process_grammar args =
StringSet.union set (StringSet.of_list (List.map (fun p -> String.trim (prod_to_prodn p)) (NTMap.find nt !prodn_gram.map)))
) StringSet.empty cmd_nts in
let allCmds = StringSet.union rstCmdvs (StringSet.union rstCmds gramCmds) in
- let out = open_out_bin (dir outfile) in
+ let out = open_temp_bin (dir outfile) in
StringSet.iter (fun c ->
let rsts = StringSet.mem c rstCmds in
let gram = StringSet.mem c gramCmds in
@@ -1956,6 +1963,7 @@ let process_grammar args =
fprintf out "%s%s %s\n" pfx var c)
allCmds;
close_out out;
+ finish_with_file (dir outfile) args;
Printf.printf "# %s in rsts, gram, total = %d %d %d\n" cmdStr (StringSet.cardinal gramCmds)
(StringSet.cardinal rstCmds) (StringSet.cardinal allCmds);
in
@@ -1973,7 +1981,7 @@ let process_grammar args =
let out = open_temp_bin (dir "prodnGrammar") in
print_in_order out prodn_gram `PRODN !prodn_gram.order StringSet.empty;
close_out out;
- finish_with_file (dir "prodnGrammar") args.verify
+ finish_with_file (dir "prodnGrammar") args
end
end
@@ -1985,6 +1993,7 @@ let parse_args () =
| "-check-cmds" -> { args with check_cmds = true }
| "-check-tacs" -> { args with check_tacs = true }
| "-no-warn" -> show_warn := false; { args with show_warn = true }
+ | "-no-update" -> { args with no_update = true }
| "-short" -> { args with fullGrammar = true }
| "-verbose" -> { args with verbose = true }
| "-verify" -> { args with verify = true }
diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune
index 3afa21f2cf..fba4856241 100644
--- a/doc/tools/docgram/dune
+++ b/doc/tools/docgram/dune
@@ -5,26 +5,47 @@
(env (_ (binaries doc_grammar.exe)))
(rule
- (targets fullGrammar)
+ (alias check-gram)
(deps
- ; Main grammar
- (glob_files %{project_root}/parsing/*.mlg)
- (glob_files %{project_root}/toplevel/*.mlg)
- (glob_files %{project_root}/vernac/*.mlg)
- ; All plugins except SSReflect for now (mimicking what is done in Makefile.doc)
- (glob_files %{project_root}/plugins/btauto/*.mlg)
- (glob_files %{project_root}/plugins/cc/*.mlg)
- (glob_files %{project_root}/plugins/derive/*.mlg)
- (glob_files %{project_root}/plugins/extraction/*.mlg)
- (glob_files %{project_root}/plugins/firstorder/*.mlg)
- (glob_files %{project_root}/plugins/funind/*.mlg)
- (glob_files %{project_root}/plugins/ltac/*.mlg)
- (glob_files %{project_root}/plugins/micromega/*.mlg)
- (glob_files %{project_root}/plugins/nsatz/*.mlg)
- (glob_files %{project_root}/plugins/omega/*.mlg)
- (glob_files %{project_root}/plugins/rtauto/*.mlg)
- (glob_files %{project_root}/plugins/setoid_ring/*.mlg)
- (glob_files %{project_root}/plugins/syntax/*.mlg))
+ (:input
+ ; Main grammar
+ (glob_files %{project_root}/parsing/*.mlg)
+ (glob_files %{project_root}/toplevel/*.mlg)
+ (glob_files %{project_root}/vernac/*.mlg)
+ ; All plugins except SSReflect and Ltac2 for now (mimicking what is done in Makefile.doc)
+ (glob_files %{project_root}/plugins/btauto/*.mlg)
+ (glob_files %{project_root}/plugins/cc/*.mlg)
+ (glob_files %{project_root}/plugins/derive/*.mlg)
+ (glob_files %{project_root}/plugins/extraction/*.mlg)
+ (glob_files %{project_root}/plugins/firstorder/*.mlg)
+ (glob_files %{project_root}/plugins/funind/*.mlg)
+ (glob_files %{project_root}/plugins/ltac/*.mlg)
+ (glob_files %{project_root}/plugins/micromega/*.mlg)
+ (glob_files %{project_root}/plugins/nsatz/*.mlg)
+ (glob_files %{project_root}/plugins/omega/*.mlg)
+ (glob_files %{project_root}/plugins/rtauto/*.mlg)
+ (glob_files %{project_root}/plugins/setoid_ring/*.mlg)
+ (glob_files %{project_root}/plugins/syntax/*.mlg)
+ ; Sphinx files
+ (glob_files %{project_root}/doc/sphinx/language/*.rst)
+ (glob_files %{project_root}/doc/sphinx/proof-engine/*.rst)
+ (glob_files %{project_root}/doc/sphinx/user-extensions/*.rst)
+ (glob_files %{project_root}/doc/sphinx/practical-tools/*.rst)
+ (glob_files %{project_root}/doc/sphinx/addendum/*.rst)
+ (glob_files %{project_root}/doc/sphinx/language/core/*.rst)
+ (glob_files %{project_root}/doc/sphinx/language/extensions/*.rst)
+ (glob_files %{project_root}/doc/sphinx/proofs/writing-proofs/*.rst)
+ (glob_files %{project_root}/doc/sphinx/proofs/automatic-tactics/*.rst)
+ (glob_files %{project_root}/doc/sphinx/proofs/creating-tactics/*.rst)
+ (glob_files %{project_root}/doc/sphinx/using/libraries/*.rst)
+ (glob_files %{project_root}/doc/sphinx/using/tools/*.rst))
+ common.edit_mlg
+ orderedGrammar)
(action
- (chdir %{project_root} (run doc_grammar -short -no-warn %{deps})))
- (mode promote))
+ (progn
+ (bash "for f in fullGrammar orderedGrammar; do cp ${f} ${f}.old; done")
+ (chdir %{project_root} (run doc_grammar -check-cmds %{input}))
+ (bash "for f in fullGrammar orderedGrammar; do cp ${f} ${f}.new; done")
+ (bash "for f in fullGrammar orderedGrammar; do cp ${f}.old ${f}; done")
+ (diff? fullGrammar fullGrammar.new)
+ (diff? orderedGrammar orderedGrammar.new))))
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 241cf48cf1..272d17bb35 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1244,8 +1244,6 @@ query_command: [
| "SearchPattern" constr_pattern in_or_out_modules "."
| "SearchRewrite" constr_pattern in_or_out_modules "."
| "Search" searchabout_query searchabout_queries "."
-| "SearchAbout" searchabout_query searchabout_queries "."
-| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "."
]
printable: [
@@ -2454,8 +2452,6 @@ as_or_and_ipat: [
eqn_ipat: [
| "eqn" ":" naming_intropattern
-| "_eqn" ":" naming_intropattern
-| "_eqn"
|
]
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 38e7b781df..0c9d7a853b 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -918,8 +918,6 @@ command: [
| "SearchPattern" one_term OPT ne_in_or_out_modules
| "SearchRewrite" one_term OPT ne_in_or_out_modules
| "Search" searchabout_query OPT searchabout_queries
-| "SearchAbout" searchabout_query OPT searchabout_queries
-| "SearchAbout" "[" LIST1 searchabout_query "]" OPT ne_in_or_out_modules
| "Time" command
| "Redirect" string command
| "Timeout" num command
@@ -1441,8 +1439,6 @@ as_or_and_ipat: [
eqn_ipat: [
| "eqn" ":" naming_intropattern
-| "_eqn" ":" naming_intropattern
-| "_eqn"
]
as_name: [
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 09:34:47 +0000