New target check-gram to check if fullGrammar and orderedGrammar are up-to-date.

Use `dune build @check-gram --auto-promote` to automatically update
these two files.  You will need to run it twice if the two files need
to be updated (which is the case most often) as Dune will stop after
the first diff failure.

The rst files are also updated but left in the `_build/` directory as
Dune wouldn't support targets outside the current directory.  You can
just `mv _build/default/doc/sphinx doc` to update them after running
the @check-gram target.

1 files changed, 42 insertions, 21 deletions

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))))