From 89a2b709d254aeab2950764a89017cf8424ddfd1 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 27 Mar 2020 16:52:26 +0100
Subject: 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.
---
 doc/tools/docgram/dune | 63 +++++++++++++++++++++++++++++++++-----------------
 1 file changed, 42 insertions(+), 21 deletions(-)

(limited to 'doc/tools')

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))))
-- 
cgit v1.2.3