(executable
 (name doc_grammar)
 (libraries rocq-runtime.clib coqpp))

(env (_ (binaries doc_grammar.exe)))

(rule
 (alias check-gram)
 (deps
  (:input
   ; Main grammar
   (glob_files %{project_root}/parsing/*.mlg)
   (glob_files %{project_root}/toplevel/*.mlg)
   (glob_files %{project_root}/vernac/*.mlg)
   (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/ring/*.mlg)
   (glob_files %{project_root}/plugins/rtauto/*.mlg)
   (glob_files %{project_root}/plugins/ssr/*.mlg)
   (glob_files %{project_root}/plugins/ssrmatching/*.mlg)
   (glob_files %{project_root}/plugins/syntax/*.mlg)
   (glob_files %{project_root}/plugins/ltac2/*.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
  (progn
   (chdir %{project_root} (run doc_grammar -no-warn -check-cmds -no-update %{input}))
   (diff? fullGrammar fullGrammar.new)
   (diff? orderedGrammar orderedGrammar.new))))