aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tools')
-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/dune60
-rw-r--r--doc/tools/docgram/fullGrammar4
-rw-r--r--doc/tools/docgram/orderedGrammar4
6 files changed, 63 insertions, 45 deletions
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..a533a6d367 100644
--- a/doc/tools/docgram/dune
+++ b/doc/tools/docgram/dune
@@ -5,26 +5,44 @@
(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
+ (chdir %{project_root} (run doc_grammar -check-cmds -no-update %{input}))
+ (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 02:55:08 +0000