1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
(executable
(name doc_grammar)
(libraries coq-core.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))))
|
