diff options
| author | Jim Fehrle | 2019-01-09 15:32:52 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2019-07-19 09:50:31 -0700 |
| commit | cf868740c3d18ee9ce9a6b38dd617784625a3cae (patch) | |
| tree | 3786c67a8574ff6856f4ef53f7aaa9f263913a19 /Makefile.build | |
| parent | ba1bb7581a5ad0969d35911fffdf61f150e0536f (diff) | |
Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg files
and inserting it into the .rst files
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 33 |
1 files changed, 32 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index c6223a6dbd..d1ed9a6f96 100644 --- a/Makefile.build +++ b/Makefile.build @@ -355,13 +355,44 @@ kernel/copcodes.ml: kernel/genOpcodeFiles.exe COQPPCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex)) coqpp/coqpp_parse.cmi: coqpp/coqpp_ast.cmi +coqpp/coqpp_parser.cmo: coqpp_parser.cmi coqpp/coqpp_parse.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmi coqpp/coqpp_lex.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmo -$(COQPP): $(COQPPCMO) coqpp/coqpp_main.ml +$(COQPP): $(COQPPCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml coqpp/coqpp_main.ml $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) -I coqpp $^ -linkall -o $@ +DOC_GRAMCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex)) + +$(DOC_GRAM): $(DOC_GRAMCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml doc/tools/docgram/doc_grammar.ml + $(SHOW)'OCAMLC -a $@' + $(HIDE)$(OCAMLC) -I coqpp $^ -package str -linkall -linkpkg -o $@ + +DOC_MLGS := */*.mlg plugins/*/*.mlg +DOC_EDIT_MLGS := doc/tools/docgram/*_mlg +DOC_RSTS := doc/sphinx/*.rst doc/sphinx/*/*.rst + +doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS) + $(SHOW)'DOC_GRAM' + $(HIDE)$(DOC_GRAM) -short -no-warn $(DOC_MLGS) + +#todo: add a dependency of sphinx on orderedGrammar and of *.rst on orderedGrammar when we're ready +doc/tools/docgram/orderedGrammar: $(DOC_GRAM) $(DOC_EDIT_MLGS) + $(SHOW)'DOC_GRAM_RSTS' + $(HIDE)$(DOC_GRAM) $(DOC_MLGS) $(DOC_RSTS) + +.PHONY: doc_gram doc_gram_rsts doc_gram_verify + +doc_gram: doc/tools/docgram/fullGrammar + +doc_gram_verify: doc/tools/docgram/fullGrammar + $(SHOW)'DOC_GRAM_VERIFY' + $(HIDE)$(DOC_GRAM) -short -no-warn -verify $(DOC_MLGS) $(DOC_RSTS) + +#todo: add dependency on $(DOC_RSTS) very soon +doc_gram_rsts: doc/tools/docgram/orderedGrammar + ########################################################################### # Specific rules for Uint63 ########################################################################### |